:: Group and Field Definitions
:: by J\'ozef Bia{\l}as
::
:: Received October 27, 1989
:: Copyright (c) 1990-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, ZFMISC_1, XBOOLE_0, RELAT_1, TARSKI, BINOP_1, SUBSET_1,
MCART_1, REALSET1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
BINOP_1, DOMAIN_1, FUNCOP_1, FUNCT_3;
constructors BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, RELSET_1, SETFAM_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, ZFMISC_1, FUNCT_2;
requirements SUBSET, BOOLE;
equalities BINOP_1;
theorems FUNCT_1, FUNCT_2, FUNCT_3, ZFMISC_1, RELAT_1, PARTFUN1;
begin
theorem Th1:
for X,x being set holds for F being Function of [:X,X:],X holds x
in [:X,X:] implies F.x in X
proof
let X,x be set;
let F be Function of [:X,X:],X;
A1: dom F = [:X,X:] by PARTFUN1:def 2;
assume x in [:X,X:];
then rng F c= X & F.x in rng F by A1,FUNCT_1:def 3,RELAT_1:def 19;
hence thesis;
end;
definition
let X be set;
let F be BinOp of X;
mode Preserv of F -> Subset of X means
:Def1:
for x being set holds x in [: it,it:] implies F.x in it;
existence
proof
X c= X;
then reconsider Z = X as Subset of X;
take Z;
thus thesis by Th1;
end;
end;
definition
let R be Relation;
let A be set;
func R||A -> set equals
R | [:A,A:];
coherence;
end;
registration
let R be Relation;
let A be set;
cluster R||A -> Relation-like;
coherence;
end;
registration
let R be Function;
let A be set;
cluster R||A -> Function-like;
coherence;
end;
theorem Th2:
for X being set, F being BinOp of X, A being Preserv of F holds F
||A is BinOp of A
proof
let X be set, F be BinOp of X, A be Preserv of F;
dom F = [:X,X:] by PARTFUN1:def 2;
then
A1: dom (F||A) = [:A,A:] by RELAT_1:62,ZFMISC_1:96;
for x being object holds x in [:A,A:] implies F||A.x in A
proof
let x be object;
assume
A2: x in [:A,A:];
then F||A.x=F.x by A1,FUNCT_1:47;
hence thesis by A2,Def1;
end;
hence thesis by A1,FUNCT_2:3;
end;
definition
let X be set;
let F be BinOp of X;
let A be Preserv of F;
redefine func F||A -> BinOp of A;
coherence by Th2;
end;
definition
let X be non trivial set;
let F be BinOp of X;
let x be Element of X;
pred F is_Bin_Op_Preserv x means
X\{x} is Preserv of F & F||X\{x} is BinOp of X\{x};
correctness;
end;
::$CT 2
theorem Th3:
for X being set holds for A being Subset of X holds ex F being
BinOp of X st for x being set holds x in [:A,A:] implies F.x in A
proof
let X be set;
let A be Subset of X;
set S = pr1(X,X);
take S;
for x being set holds x in [:A,A:] implies S.x in A
proof
let x be set;
assume x in [:A,A:];
then consider p,q being object such that
A1: p in A & q in A and
A2: x = [p,q] by ZFMISC_1:def 2;
S.x = S.(p,q) by A2;
hence thesis by A1,FUNCT_3:def 4;
end;
hence thesis;
end;
definition
let X be set;
let A be Subset of X;
mode Presv of X,A -> BinOp of X means
:Def4:
for x being set holds x in [:A, A:] implies it.x in A;
existence by Th3;
end;
theorem Th4:
for X being set, A being Subset of X, F being Presv of X,A holds
F||A is BinOp of A
proof
let X be set;
let A be Subset of X;
let F be Presv of X,A;
dom F = [:X,X:] by PARTFUN1:def 2;
then
A1: dom (F||A) = [:A,A:] by RELAT_1:62,ZFMISC_1:96;
for x being object holds x in [:A,A:] implies F||A.x in A
proof
let x be object;
assume
A2: x in [:A,A:];
then F||A.x=F.x by A1,FUNCT_1:47;
hence thesis by A2,Def4;
end;
hence thesis by A1,FUNCT_2:3;
end;
definition
let X be set;
let A be Subset of X;
let F be Presv of X,A;
func F|||A -> BinOp of A equals
F||A;
coherence by Th4;
end;
definition
let A be set;
let x be Element of A;
mode DnT of x,A -> BinOp of A means
:Def6:
for y being set holds y in [:A\{x },A\{x}:] implies it.y in A\{x};
existence by Th3;
end;
theorem Th5:
for A being non trivial set holds for x being Element of A holds
for F being DnT of x,A holds F||(A\{x}) is BinOp of A\{x}
proof
let A be non trivial set;
let x be Element of A;
let F be DnT of x,A;
dom F = [:A,A:] by FUNCT_2:def 1;
then
A1: dom(F||(A\{x})) = [:A\{x},A\{x}:] by RELAT_1:62,ZFMISC_1:96;
for y being object holds y in [:A\{x},A\{x}:] implies F||(A\{x}).y in A\{x}
proof
let y be object;
assume
A2: y in [:A\{x},A\{x}:];
then F||(A\{x}).y=F.y by A1,FUNCT_1:47;
hence thesis by A2,Def6;
end;
hence thesis by A1,FUNCT_2:3;
end;
definition
let A be non trivial set;
let x be Element of A;
let F be DnT of x,A;
func F!(A,x) -> BinOp of A\{x} equals
F||(A\{x});
coherence by Th5;
end;