### The Mizar article:

### Group and Field Definitions

**by****Jozef Bialas**

- Received October 27, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: REALSET1
- [ 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; definitions RLVECT_1, STRUCT_0, TARSKI, XBOOLE_0; theorems TARSKI, FUNCT_1, FUNCT_2, FUNCT_3, ZFMISC_1, VECTSP_1, RLVECT_1, BINOP_1, RELSET_1, SUBSET_1, XBOOLE_0, XBOOLE_1, RELAT_1; begin canceled 9; theorem Th10: 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:] & rng F c= X proof X={} implies [:X,X:]={} by ZFMISC_1:113; hence thesis by FUNCT_2:def 1,RELSET_1:12; end; assume x in [:X,X:]; then F.x in rng F by A1,FUNCT_1:def 5; hence thesis by A1; end; theorem Th11: 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 proof let X be set, F be BinOp of X; X c= X; then reconsider Z = X as Subset of X; take Z; thus thesis by Th10; end; definition let X be set; let F be BinOp of X; let A be Subset of X; pred F is_in A means 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 :Def2:for x being set holds x in [:it,it:] implies F.x in it; existence by Th11; end; canceled 2; theorem Th14: for X being set, F being BinOp of X, A being Preserv of F holds F|([:A,A:]) is BinOp of A proof let X be set, F be BinOp of X, A be Preserv of F; X={} implies [:X,X:]={} by ZFMISC_1:113; then A1: dom F = [:X,X:] & rng F c= X by FUNCT_2:def 1,RELSET_1:12; [:A,A:] c= [:X,X:] by ZFMISC_1:119; then A2: dom (F|([:A,A:])) = [:A,A:] by A1,RELAT_1:91; for x being set holds x in [:A,A:] implies F|([:A,A:]).x in A proof let x be set; assume A3:x in [:A,A:]; then F|([:A,A:]).x=F.x by A2,FUNCT_1:70; hence thesis by A3,Def2; end; hence thesis by A2,FUNCT_2:5; end; definition let X be set; let F be BinOp of X; let A be Preserv of F; func F||A -> BinOp of A equals F | [:A,A:]; coherence by Th14; end; Lm1: now consider x being set; set B = {x}; A1: x in B by TARSKI:def 1; consider og being BinOp of B; A2: og.[x,x] = x proof A3:dom og = [:B,B:] & rng og c= B by FUNCT_2:def 1,RELSET_1:12; [x,x] in [:B,B:] by A1,ZFMISC_1:def 2; then og.[x,x] in rng og by A3,FUNCT_1:def 5; hence thesis by A3,TARSKI:def 1; end; reconsider ng = x as Element of B by TARSKI:def 1; A4: for a,b,c being Element of B holds og.[og.[a,b],c] = og.[a,og.[b,c]] proof let a,b,c be Element of B; a = x & b = x & c = x by TARSKI:def 1; hence thesis by A2; end; A5: for a being Element of B holds og.[a,ng] = a & og.[ng,a] = a proof let a be Element of B; a = x by TARSKI:def 1; hence thesis by A2; end; A6: for a being Element of B ex b being Element of B st og.[a,b] = ng & og.[b,a] = ng proof let a be Element of B; take ng; thus thesis by A2,TARSKI:def 1; end; for a,b being Element of B holds og.[a,b] = og.[b,a] proof let a,b be Element of B; a = x & b = x by TARSKI:def 1; hence thesis; end; hence ex A being non empty set st ex og being BinOp of A st ex ng being Element of A st (for a,b,c being Element of A holds og.[og.[a,b],c] = og.[a,og.[b,c]]) & (for a being Element of A holds og.[a,ng] = a & og.[ng,a] = a) & (for a being Element of A ex b being Element of A st og.[a,b] = ng & og.[b,a] = ng) & (for a,b being Element of A holds og.[a,b] = og.[b,a]) by A4,A5,A6; end; Lm2: for L being non empty LoopStr for a,b being Element of L holds (the add of L).[a,b] = a + b proof let L be non empty LoopStr, a,b be Element of L; thus (the add of L).[a,b] = (the add of L).(a,b) by BINOP_1:def 1 .= a + b by RLVECT_1:5; end; definition ::group let IT be LoopStr; canceled; attr IT is zeroed means :Def5: 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 :Def6: 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 :Def7: 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]]; compatibility proof hereby assume A1: L is add-associative; let a,b,c be Element of L; A2: a + b = (the add of L).[a,b] by Lm2; A3: b + c = (the add of L).[b,c] by Lm2; thus (the add of L).[(the add of L).[a,b],c] = a + b + c by A2,Lm2 .= a + (b + c) by A1,RLVECT_1:def 6 .= (the add of L).[a,(the add of L).[b,c]] by A3,Lm2; end; assume that A4: 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]]; let u,v,w be Element of L; A5: u + v = (the add of L).[u,v] by Lm2; A6: v + w = (the add of L).[v,w] by Lm2; thus (u + v) + w = (the add of L).[(the add of L).[u,v],w] by A5,Lm2 .= (the add of L).[u,(the add of L).[v,w]] by A4 .= u + (v + w) by A6,Lm2; end; redefine attr L is Abelian means :Def8: for a,b being Element of L holds (the add of L).[a,b] = (the add of L).[b,a]; compatibility proof hereby assume A7: L is Abelian; let a,b be Element of L; thus (the add of L).[a,b] = a + b by Lm2 .= b + a by A7,RLVECT_1:def 5 .= (the add of L).[b,a] by Lm2; end; assume A8: for a,b being Element of L holds (the add of L).[a,b] = (the add of L).[b,a]; let a,b be Element of L; thus a + b = (the add of L).[a,b] by Lm2 .= (the add of L).[b,a] by A8 .= b + a by Lm2; end; 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; coherence proof thus the carrier of LoopStr(#X,a,Z#) is non empty; end; end; definition cluster strict Abelian add-associative zeroed complementable (non empty LoopStr); existence proof consider A being non empty set, og being BinOp of A, ng being Element of A such that A1: (for a,b,c being Element of A holds og.[og.[a,b],c] = og.[a,og.[b,c]]) & (for a being Element of A holds og.[a,ng] = a & og.[ng,a] = a) & (for a being Element of A ex b being Element of A st og.[a,b] = ng & og.[b,a] = ng) & (for a,b being Element of A holds og.[a,b] = og.[b,a]) by Lm1; LoopStr(#A,og,ng#) is Abelian add-associative zeroed complementable by A1,Def5,Def6,Def7,Def8; hence thesis; end; 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 :Def12: IT is empty or ex x being set st IT = {x}; end; definition cluster trivial non empty set; existence proof take {0}; thus thesis by Def12; end; cluster non trivial non empty set; existence proof take {0,1}; not ex x being set st {0,1} = {x} by ZFMISC_1:9; hence thesis by Def12; end; cluster non trivial -> non empty set; coherence proof let IT be set; assume not(IT is empty or ex x being set st IT = {x}); hence thesis; end; end; canceled 17; theorem Th32: for X being non empty set holds X is non trivial iff for x being set holds X\{x} is non empty set proof let X be non empty set; hereby assume A1: X is non trivial; let x be set; X <> {x} by A1,Def12; then consider y being set such that A2: y in X and A3: x <> y by ZFMISC_1:41; not y in {x} by A3,TARSKI:def 1; hence X\{x} is non empty set by A2,XBOOLE_0:def 4; end; assume A4: for x being set holds X\{x} is non empty set; thus X is non empty; given x being set such that A5: X = {x}; X\{x} is empty by A5,XBOOLE_1:37; hence contradiction by A4; end; theorem ex A being non empty set st for z being Element of A holds A \ {z} is non empty set proof consider x,y being set such that A1: x<>y by VECTSP_1:78; set B = {x,y}; A2: for z being Element of B holds B\{z} is non empty set proof let z be Element of B; A3:y in B by TARSKI:def 2; not y in {x} by A1,TARSKI:def 1; then A4:B\{x} is non empty set by A3,XBOOLE_0:def 4; A5:x in B by TARSKI:def 2; not x in {y} by A1,TARSKI:def 1; then B\{y} is non empty set by A5,XBOOLE_0:def 4; hence thesis by A4,TARSKI:def 2; end; take B; thus thesis by A2; end; theorem Th34: 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 proof let X be non empty set; assume A1: for x being Element of X holds X\{x} is non empty set; thus X is non empty; given x being set such that A2: X = {x}; A3: x in X by A2,TARSKI:def 1; X\{x} is empty by A2,XBOOLE_1:37; hence contradiction by A1,A3; end; definition let IT be 1-sorted; attr IT is trivial means the carrier of IT is trivial; end; Lm3: for S being 1-sorted holds S is trivial iff for x,y being Element of S holds x = y proof let S be 1-sorted; set I = the carrier of S; per cases; suppose A1:I is non empty; thus S is trivial implies for x,y being Element of I holds x = y proof assume A2: I is trivial; per cases by A2,Def12; suppose I is empty; hence thesis by A1; suppose ex a being set st I = {a}; then consider a being set such that A3: I = {a}; let x, y be Element of I; thus x = a by A3,TARSKI:def 1 .= y by A3,TARSKI:def 1; end; assume A4: for x,y being Element of I holds x = y; consider a being set such that A5: a in I by A1,XBOOLE_0:def 1; I = {a} proof hereby let i be set; assume i in I; then a = i by A4,A5; hence i in {a} by TARSKI:def 1; end; let i be set; assume i in {a}; hence i in I by A5,TARSKI:def 1; end; hence I is empty or ex x being set st I = {x}; suppose A6:I is empty; thus S is trivial implies for x,y being Element of I holds x = y proof assume I is trivial; let x, y be Element of I; thus x = {} by A6,SUBSET_1:def 2 .= y by A6,SUBSET_1:def 2; end; assume for x,y being Element of I holds x = y; thus I is empty or ex x being set st I = {x} by A6; end; definition cluster trivial 1-sorted; existence proof take O = 1-sorted(#{0}#); now let x,y be Element of O; thus x = 0 by TARSKI:def 1 .= y by TARSKI:def 1; end; hence thesis by Lm3; end; end; theorem 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 by Th34; Lm4: now 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}; let nm0 be Element of A; assume A1: nm0=nm; set F = doubleLoopStr(#A,od,om,nm0,nd#); thus F is non trivial proof now take nd,nm0; A\{nd} is non empty set by Th32; then not nm in {nd} by XBOOLE_0:def 4; hence nd <> nm0 by A1,TARSKI:def 1; end; hence thesis by Lm3; end; thus F is strict; end; definition cluster non trivial strict doubleLoopStr; existence proof consider A be non trivial set, od,om be BinOp of A, nd be Element of A, nm be Element of A\{nd}; A\{nd} is non empty set by Th32; then reconsider nm0=nm as Element of A by XBOOLE_0:def 4; take doubleLoopStr(#A,od,om,nm0,nd#); thus thesis by Lm4; end; 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 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; existence proof A\{nd} is non empty set by Th32; then reconsider nm0=nm as Element of A by XBOOLE_0:def 4; reconsider F = doubleLoopStr(#A,od,om,nm0,nd#) as non trivial strict doubleLoopStr by Lm4; take F; thus thesis; end; uniqueness; 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},X\{x}:] is BinOp of X\{x}; correctness; end; canceled 3; theorem Th39: 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); A1: 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 set such that A2: p in A & q in A & x = [p,q] by ZFMISC_1:def 2; thus thesis by A2,FUNCT_3:def 5; end; take S; thus thesis by A1; end; definition let X be set; let A be Subset of X; mode Presv of X,A -> BinOp of X means :Def16:for x being set holds x in [:A,A:] implies it.x in A; existence by Th39; end; canceled; theorem Th41: for X being set, A being Subset of X, F being Presv of X,A holds F|([:A,A:]) is BinOp of A proof let X be set; let A be Subset of X; let F be Presv of X,A; X={} implies [:X,X:]={} by ZFMISC_1:113; then A1: dom F = [:X,X:] & rng F c= X by FUNCT_2:def 1,RELSET_1:12; [:A,A:] c= [:X,X:] by ZFMISC_1:119; then A2: dom (F|([:A,A:])) = [:A,A:] by A1,RELAT_1:91; for x being set holds x in [:A,A:] implies F|([:A,A:]).x in A proof let x be set; assume A3:x in [:A,A:]; then F|([:A,A:]).x=F.x by A2,FUNCT_1:70; hence thesis by A3,Def16; end; hence thesis by A2,FUNCT_2:5; 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,A:]; coherence by Th41; end; canceled; theorem Th43: 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} proof let A be non trivial set; let x be Element of A; set B = A\{x}; B is Subset of A by XBOOLE_1:36; then consider F1 being BinOp of A such that A1: for y being set holds y in [:B,B:] implies F1.y in B by Th39; take F1; thus thesis by A1; end; definition let A be non trivial set; let x be Element of A; mode DnT of x,A -> BinOp of A means :Def18: for y being set holds y in [:A\{x},A\{x}:] implies it.y in A\{x}; existence by Th43; end; canceled; theorem Th45: 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} proof let A be non trivial set; let x be Element of A; let F be DnT of x,A; A1: dom F = [:A,A:] & rng F c= A by FUNCT_2:def 1,RELSET_1:12; A\{x} is Subset of A by XBOOLE_1:36; then [:A\{x},A\{x}:] c= [:A,A:] by ZFMISC_1:119; then A2: dom(F|[:A\{x},A\{x}:]) = [:A\{x},A\{x}:] by A1,RELAT_1:91; for y being set holds y in [:A\{x},A\{x}:] implies F|[:A\{x},A\{x}:].y in A\{x} proof let y be set; assume A3:y in [:A\{x},A\{x}:]; then F|[:A\{x},A\{x}:].y=F.y by A2,FUNCT_1:70; hence thesis by A3,Def18; end; hence thesis by A2,FUNCT_2:5; 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},A\{x}:]; coherence by Th45; end; definition let IT be 1-sorted; redefine attr IT is trivial means for x,y being Element of IT holds x = y; compatibility by Lm3; end;

Back to top