Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Group and Field Definitions

**by****Jozef Bialas**- Received October 27, 1989
- MML identifier: REALSET1

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, BOOLE, BINOP_1, RLVECT_1, VECTSP_1, FUNCT_3, QC_LANG1, REALSET1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, FUNCT_3, STRUCT_0, RLVECT_1, VECTSP_1; constructors BINOP_1, FUNCT_3, VECTSP_1, MEMBERED, XBOOLE_0; clusters FUNCT_1, RLVECT_1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin canceled 9; theorem :: REALSET1:10 for X,x being set holds for F being Function of [:X,X:],X holds x in [:X,X:] implies F.x in X; theorem :: REALSET1:11 for X being set, F being BinOp of X ex A being Subset of X st for x being set holds x in [:A,A:] implies F.x in A; definition let X be set; let F be BinOp of X; let A be Subset of X; pred F is_in A means :: REALSET1:def 1 for x being set holds x in [:A,A:] implies F.x in A; end; definition let X be set; let F be BinOp of X; mode Preserv of F -> Subset of X means :: REALSET1:def 2 for x being set holds x in [:it,it:] implies F.x in it; end; canceled 2; theorem :: REALSET1:14 for X being set, F being BinOp of X, A being Preserv of F holds F|([:A,A:]) is BinOp of A; definition let X be set; let F be BinOp of X; let A be Preserv of F; func F||A -> BinOp of A equals :: REALSET1:def 3 F | [:A,A:]; end; definition ::group let IT be LoopStr; canceled; attr IT is zeroed means :: REALSET1:def 5 for a being Element of IT holds (the add of IT).[a,the Zero of IT] = a & (the add of IT).[the Zero of IT,a] = a; attr IT is complementable means :: REALSET1:def 6 for a being Element of IT ex b being Element of IT st (the add of IT).[a,b] = the Zero of IT & (the add of IT).[b,a] = the Zero of IT; end; definition let L be non empty LoopStr; redefine attr L is add-associative means :: REALSET1:def 7 for a,b,c being Element of L holds (the add of L).[(the add of L).[a,b],c] = (the add of L).[a,(the add of L).[b,c]]; redefine attr L is Abelian means :: REALSET1:def 8 for a,b being Element of L holds (the add of L).[a,b] = (the add of L).[b,a]; end; definition let X be non empty set, a be BinOp of X, Z be Element of X; cluster LoopStr(#X,a,Z#) -> non empty; end; definition cluster strict Abelian add-associative zeroed complementable (non empty LoopStr); end; definition ::group mode Group is Abelian add-associative zeroed complementable (non empty LoopStr); end; definition let IT be set; canceled 3; attr IT is trivial means :: REALSET1:def 12 IT is empty or ex x being set st IT = {x}; end; definition cluster trivial non empty set; cluster non trivial non empty set; cluster non trivial -> non empty set; end; canceled 17; theorem :: REALSET1:32 for X being non empty set holds X is non trivial iff for x being set holds X\{x} is non empty set; theorem :: REALSET1:33 ex A being non empty set st for z being Element of A holds A \ {z} is non empty set; theorem :: REALSET1:34 for X being non empty set st for x being Element of X holds X\{x} is non empty set holds X is non trivial; definition let IT be 1-sorted; attr IT is trivial means :: REALSET1:def 13 the carrier of IT is trivial; end; definition cluster trivial 1-sorted; end; theorem :: REALSET1:35 for A being non empty set st (for x being Element of A holds A\{x} is non empty set) holds A is non trivial set; definition cluster non trivial strict doubleLoopStr; end; definition ::field operator let A be non trivial set; let od,om be BinOp of A; let nd be Element of A; let nm be Element of A\{nd}; func field(A,od,om,nd,nm) -> non trivial strict doubleLoopStr means :: REALSET1:def 14 A = the carrier of it & od = the add of it & om = the mult of it & nd = the Zero of it & nm = the unity of it; 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 :: REALSET1:def 15 (X\{x} is Preserv of F) & F|[:X\{x},X\{x}:] is BinOp of X\{x}; end; canceled 3; theorem :: REALSET1:39 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; definition let X be set; let A be Subset of X; mode Presv of X,A -> BinOp of X means :: REALSET1:def 16 for x being set holds x in [:A,A:] implies it.x in A; end; canceled; theorem :: REALSET1:41 for X being set, A being Subset of X, F being Presv of X,A holds F|([:A,A:]) is BinOp of A; 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 :: REALSET1:def 17 F | [:A,A:]; end; canceled; theorem :: REALSET1:43 for A being non trivial set holds for x being Element of A holds ex F being BinOp of A st for y being set holds y in [:A\{x},A\{x}:] implies F.y in A\{x}; definition let A be non trivial set; let x be Element of A; mode DnT of x,A -> BinOp of A means :: REALSET1:def 18 for y being set holds y in [:A\{x},A\{x}:] implies it.y in A\{x}; end; canceled; theorem :: REALSET1:45 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},A\{x}:] is BinOp of A\{x}; 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 :: REALSET1:def 19 F | [:A\{x},A\{x}:]; end; definition let IT be 1-sorted; redefine attr IT is trivial means :: REALSET1:def 20 for x,y being Element of IT holds x = y; end;

Back to top