Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Properties of Fields

**by****Jozef Bialas**- Received June 20, 1990
- MML identifier: REALSET2

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, REALSET1, FUNCT_1, RELAT_1, BINOP_1, RLVECT_1, QC_LANG1, VECTSP_1, REALSET2; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, STRUCT_0, RLVECT_1, VECTSP_1, REALSET1; constructors ENUMSET1, REALSET1, MEMBERED, XBOOLE_0; clusters REALSET1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin definition let IT be doubleLoopStr; attr IT is Field-like means :: REALSET2:def 1 ex A being non trivial set, od being BinOp of A, nd being Element of A, om being DnT of nd,A, nm being Element of A\{nd} st (IT = field(A,od,om,nd,nm) & LoopStr(#A,od,nd#) is Group & (for B being non empty set, P being BinOp of B, e being Element of B holds (B = A\{nd} & e = nm & P = om!(A,nd) implies LoopStr(#B,P,e#) is Group)) & for x,y,z being Element of A holds om.[x,od.[y,z]] = od.[om.[x,y],om.[x,z]] & om.[od.[x,y],z] = od.[om.[x,z],om.[y,z]]); end; definition cluster strict Field-like doubleLoopStr; end; definition ::field mode Field is Field-like doubleLoopStr; end; definition ::supp projection let F be Field; func suppf(F) -> non trivial set means :: REALSET2:def 2 ex od being BinOp of it, nd being Element of it, om being DnT of nd,it, nm being Element of it\{nd} st F = field(it,od,om,nd,nm); end; definition ::add projection let F be Field; func odf(F) -> BinOp of suppf(F) means :: REALSET2:def 3 ex nd being Element of suppf(F), om being DnT of nd, suppf(F), nm being Element of suppf(F)\{nd} st F = field(suppf(F),it,om,nd,nm); end; definition ::nadd projection let F be Field; func ndf(F) -> Element of suppf(F) means :: REALSET2:def 4 ex om being DnT of it,suppf(F), nm being Element of suppf(F)\{it} st F = field(suppf(F),odf(F),om,it,nm); end; definition ::mply projection let F be Field; func omf(F) -> DnT of ndf(F),suppf(F) means :: REALSET2:def 5 ex nm being Element of suppf(F)\{ndf(F)} st F = field(suppf(F),odf(F),it,ndf(F),nm); end; definition ::nom projection let F be Field; func nmf(F) -> Element of suppf(F)\{ndf(F)} means :: REALSET2:def 6 F = field(suppf(F),odf(F),omf(F),ndf(F),it); end; canceled 7; theorem :: REALSET2:8 for F being Field holds LoopStr(#suppf(F),odf(F),ndf(F)#) is Group; theorem :: REALSET2:9 for F being Field, B being non empty set, P being BinOp of B, e being Element of B st B = suppf(F)\{ndf(F)} & e = nmf(F) & P = omf(F)!(suppf(F),ndf(F)) holds LoopStr(#B,P,e#) is Group; theorem :: REALSET2:10 for F being Field, x,y,z being Element of suppf(F) holds (omf(F).[x,odf(F).[y,z]] = odf(F).[omf(F).[x,y],omf(F).[x,z]] & omf(F).[odf(F).[x,y],z] = odf(F).[omf(F).[x,z],omf(F).[y,z]] ); theorem :: REALSET2:11 for F being Field, a,b,c being Element of suppf(F) holds odf(F).[odf(F).[a,b],c] = odf(F).[a,odf(F).[b,c]]; theorem :: REALSET2:12 for F being Field, a,b being Element of suppf(F) holds odf(F).[a,b] = odf(F).[b,a]; theorem :: REALSET2:13 for F being Field, a being Element of suppf(F) holds odf(F).[a,ndf(F)] = a & odf(F).[ndf(F),a] = a; theorem :: REALSET2:14 for F being Field holds for a being Element of suppf(F) ex b being Element of suppf(F) st odf(F).[a,b] = ndf(F) & odf(F).[b,a] = ndf(F); definition let F be non trivial set; mode OnePoint of F -> set means :: REALSET2:def 7 ex x being Element of F st it = {x}; end; theorem :: REALSET2:15 for F being non trivial set holds for A being OnePoint of F holds F\A is non empty set; definition let F be non trivial set; let A be OnePoint of F; cluster F\A -> non empty; end; definition let F be non trivial set; cluster non empty OnePoint of F; end; definition let F be non trivial set; let x be Element of F; redefine func {x} -> OnePoint of F; end; canceled 4; theorem :: REALSET2:20 for F being Field holds for a,b,c being Element of suppf(F)\{ndf(F)} holds omf(F).[omf(F).[a,b],c] = omf(F).[a,omf(F).[b,c]]; theorem :: REALSET2:21 for F being Field holds for a,b being Element of suppf(F)\{ndf(F)} holds omf(F).[a,b] = omf(F).[b,a]; theorem :: REALSET2:22 for F being Field holds for a being Element of suppf(F)\{ndf(F)} holds omf(F).[a,nmf(F)] = a & omf(F).[nmf(F),a] = a; theorem :: REALSET2:23 for F being Field holds for a being Element of suppf(F)\{ndf(F)} ex b being Element of suppf(F)\{ndf(F)} st omf(F).[a,b] = nmf(F) & omf(F).[b,a] = nmf(F); definition ::complement element let F be Field; func compf(F) -> Function of suppf(F),suppf(F) means :: REALSET2:def 8 for x being Element of suppf(F) holds odf(F).[x,it.x] = ndf(F); end; canceled 2; theorem :: REALSET2:26 for F being Field holds for x,y being Element of suppf(F) holds odf(F).[x,y] = ndf(F) implies y = compf(F).x; theorem :: REALSET2:27 for F being Field holds for x being Element of suppf(F) holds x = compf(F).(compf(F).x); theorem :: REALSET2:28 for F being Field holds for a,b being Element of suppf(F) holds (odf(F).[a,b] is Element of suppf(F) & omf(F).[a,b] is Element of suppf(F) & compf(F).a is Element of suppf(F)); theorem :: REALSET2:29 for F being Field holds for a,b,c being Element of suppf(F) holds omf(F).[a,odf(F).[b,compf(F).c]] = odf(F).[omf(F).[a,b],compf(F).(omf(F).[a,c])]; theorem :: REALSET2:30 for F being Field holds for a,b,c being Element of suppf(F) holds omf(F).[odf(F).[a,compf(F).b],c] = odf(F).[omf(F).[a,c],compf(F).(omf(F).[b,c])]; theorem :: REALSET2:31 for F being Field holds for a being Element of suppf(F) holds omf(F).[a,ndf(F)] = ndf(F); theorem :: REALSET2:32 for F being Field holds for a being Element of suppf(F) holds omf(F).[ndf(F),a] = ndf(F); theorem :: REALSET2:33 for F being Field, a,b being Element of suppf(F) holds compf(F).(omf(F).[a,b]) = omf(F).[a,compf(F).b]; theorem :: REALSET2:34 for F being Field holds omf(F).[nmf(F),ndf(F)] = ndf(F); theorem :: REALSET2:35 for F being Field holds omf(F).[ndf(F),nmf(F)] = ndf(F); theorem :: REALSET2:36 for F being Field, a,b being Element of suppf(F) holds omf(F).[a,b] is Element of suppf(F); theorem :: REALSET2:37 for F being Field, a,b,c being Element of suppf(F) holds omf(F).[omf(F).[a,b],c] = omf(F).[a,omf(F).[b,c]]; theorem :: REALSET2:38 for F being Field, a,b being Element of suppf(F) holds omf(F).[a,b] = omf(F).[b,a]; theorem :: REALSET2:39 for F being Field, a being Element of suppf(F) holds omf(F).[a,nmf(F)] = a & omf(F).[nmf(F),a] = a; definition :: reverse element let F be Field; func revf(F) -> Function of suppf(F)\{ndf(F)},suppf(F)\{ndf(F)} means :: REALSET2:def 9 for x being Element of suppf(F)\{ndf(F)} holds omf(F).[x,it.x] = nmf(F); end; canceled 2; theorem :: REALSET2:42 for F being Field holds for x,y being Element of suppf(F)\{ndf(F)} holds omf(F).[x,y] = nmf(F) implies y = revf(F).x; theorem :: REALSET2:43 for F being Field holds for x being Element of suppf(F)\{ndf(F)} holds x =revf(F).(revf(F).x); theorem :: REALSET2:44 for F being Field holds for a,b being Element of suppf(F)\{ndf(F)} holds omf(F).[a,b] is Element of suppf(F)\{ndf(F)} & revf(F).a is Element of suppf(F)\{ndf(F)}; theorem :: REALSET2:45 for F being Field holds for a,b,c being Element of suppf(F) holds odf(F).[a,b] = odf(F).[a,c] implies b = c; theorem :: REALSET2:46 for F being Field holds for a being Element of suppf(F)\{ndf(F)} holds for b,c being Element of suppf(F) holds omf(F).[a,b] = omf(F).[a,c] implies b = c;

Back to top