Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Several Properties of Fields. Field Theory

**by****Jozef Bialas**- Received September 27, 1990
- MML identifier: REALSET3

- [ Mizar article, MML identifier index ]

environ vocabulary VECTSP_1, REALSET2, FUNCT_1, BOOLE, BINOP_1, REALSET3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, REALSET2, BINOP_1; constructors REALSET2, XBOOLE_0; clusters REALSET1, REALSET2, RELSET_1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Properties of fields theorem :: REALSET3:1 for F being Field holds compf(F).(ndf(F)) = ndf(F); theorem :: REALSET3:2 for F being Field holds revf(F).(nmf(F)) = nmf(F); theorem :: REALSET3:3 for F being Field holds for a,b being Element of suppf(F) holds compf(F).(odf(F).[a,compf(F).b]) = odf(F).[b,compf(F).a]; theorem :: REALSET3:4 for F being Field holds for a,b being Element of suppf(F)\{ndf(F)} holds revf(F).(omf(F).[a,revf(F).b]) = omf(F).[b,revf(F).a]; theorem :: REALSET3:5 for F being Field holds for a,b being Element of suppf(F) holds compf(F).(odf(F).[a,b]) = odf(F).[compf(F).a,compf(F).b]; theorem :: REALSET3:6 for F being Field, a,b being Element of suppf(F)\{ndf(F)} holds revf(F).(omf(F).[a,b]) = omf(F).[revf(F).a,revf(F).b]; theorem :: REALSET3:7 for F being Field holds for a,b,c,d being Element of suppf(F) holds odf(F).[a,compf(F).b] = odf(F).[c,compf(F).d] iff odf(F).[a,d] = odf(F).[b,c]; theorem :: REALSET3:8 for F being Field holds for a,c being Element of suppf(F) holds for b,d being Element of suppf(F)\{ndf(F)} holds omf(F).[a,revf(F).b] = omf(F).[c,revf(F).d] iff omf(F).[a,d] = omf(F).[b,c]; theorem :: REALSET3:9 for F being Field holds for a,b being Element of suppf(F) holds omf(F).[a,b] = ndf(F) iff (a = ndf(F) or b = ndf(F)); theorem :: REALSET3:10 for F being Field holds for a,b being Element of suppf(F) holds for c,d being Element of suppf(F)\{ndf(F)} holds omf(F).[omf(F).[a,revf(F).c],omf(F).[b,revf(F).d]] = omf(F).[omf(F).[a,b],revf(F).(omf(F).[c,d])]; theorem :: REALSET3:11 for F being Field holds for a,b being Element of suppf(F) holds for c,d being Element of suppf(F)\{ndf(F)} holds odf(F).[omf(F).[a,revf(F).c],omf(F).[b,revf(F).d]] = omf(F).[odf(F).[omf(F).[a,d],omf(F).[b,c]],revf(F).(omf(F).[c,d])]; definition ::subtraction let F be Field; func osf(F) -> BinOp of suppf(F) means :: REALSET3:def 1 for x,y being Element of suppf(F) holds it.[x,y] = odf(F).[x,compf(F).y]; end; canceled 2; theorem :: REALSET3:14 for F being Field holds for x being Element of suppf(F) holds osf(F).[x,x] = ndf(F); theorem :: REALSET3:15 for F being Field holds for a,b,c being Element of suppf(F) holds omf(F).[a,osf(F).[b,c]] = osf(F).[omf(F).[a,b],omf(F).[a,c]]; theorem :: REALSET3:16 for F being Field holds for a,b being Element of suppf(F) holds osf(F).[a,b] is Element of suppf(F); theorem :: REALSET3:17 for F being Field holds for a,b,c being Element of suppf(F) holds omf(F).[osf(F).[a,b],c] = osf(F).[omf(F).[a,c],omf(F).[b,c]]; theorem :: REALSET3:18 for F being Field holds for a,b being Element of suppf(F) holds osf(F).[a,b] = compf(F).(osf(F).[b,a]); theorem :: REALSET3:19 for F being Field holds for a,b being Element of suppf(F) holds osf(F).[compf(F).a,b] = compf(F).(odf(F).[a,b]); theorem :: REALSET3:20 for F being Field holds for a,b,c,d being Element of suppf(F) holds osf(F).[a,b] = osf(F).[c,d] iff odf(F).[a,d] = odf(F).[b,c]; theorem :: REALSET3:21 for F being Field holds for a being Element of suppf(F) holds osf(F).[ndf(F),a] = compf(F).a; theorem :: REALSET3:22 for F being Field holds for a being Element of suppf(F) holds osf(F).[a,ndf(F)] = a; theorem :: REALSET3:23 for F being Field holds for a,b,c being Element of suppf(F) holds odf(F).[a,b] = c iff osf(F).[c,a] = b; theorem :: REALSET3:24 for F being Field holds for a,b,c being Element of suppf(F) holds odf(F).[a,b] = c iff osf(F).[c,b] = a; theorem :: REALSET3:25 for F being Field holds for a,b,c being Element of suppf(F) holds osf(F).[a,osf(F).[b,c]] = odf(F).[osf(F).[a,b],c]; theorem :: REALSET3:26 for F being Field holds for a,b,c being Element of suppf(F) holds osf(F).[a,odf(F).[b,c]] = osf(F).[osf(F).[a,b],c]; definition ::division. let F be Field; func ovf(F) -> Function of [:suppf(F),suppf(F)\{ndf(F)}:],suppf(F) means :: REALSET3:def 2 for x being Element of suppf(F), y being Element of suppf(F)\{ndf(F)} holds it.[x,y] = omf(F).[x,revf(F).y]; end; canceled 2; theorem :: REALSET3:29 for F being Field holds for x being Element of suppf(F)\{ndf(F)} holds ovf(F).[x,x] = nmf(F); theorem :: REALSET3:30 for F being Field holds for a being Element of suppf(F) holds for b being Element of suppf(F)\{ndf(F)} holds ovf(F).[a,b] is Element of suppf(F); theorem :: REALSET3:31 for F being Field holds for a,b being Element of suppf(F) holds for c being Element of suppf(F)\{ndf(F)} holds omf(F).[a,ovf(F).[b,c]] = ovf(F).[omf(F).[a,b],c]; theorem :: REALSET3:32 for F being Field holds for a being Element of suppf(F)\{ndf(F)} holds omf(F).[a,ovf(F).[nmf(F),a]] = nmf(F) & omf(F).[ovf(F).[nmf(F),a],a] = nmf(F); canceled 2; theorem :: REALSET3:35 for F being Field holds for a,b being Element of suppf(F)\{ndf(F)} holds ovf(F).[a,b] = revf(F).(ovf(F).[b,a]); theorem :: REALSET3:36 for F being Field holds for a,b being Element of suppf(F)\{ndf(F)} holds ovf(F).[revf(F).a,b] = revf(F).(omf(F).[a,b]); theorem :: REALSET3:37 for F being Field holds for a,c being Element of suppf(F) holds for b,d being Element of suppf(F)\{ndf(F)} holds ovf(F).[a,b] = ovf(F).[c,d] iff omf(F).[a,d] = omf(F).[b,c]; theorem :: REALSET3:38 for F being Field holds for a being Element of suppf(F)\{ndf(F)} holds ovf(F).[nmf(F),a] = revf(F).a; theorem :: REALSET3:39 for F being Field holds for a being Element of suppf(F) holds ovf(F).[a,nmf(F)] = a; theorem :: REALSET3:40 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] = c iff ovf(F).[c,a] = b; theorem :: REALSET3:41 for F being Field holds for a,c being Element of suppf(F) holds for b being Element of suppf(F)\{ndf(F)} holds omf(F).[a,b] = c iff ovf(F).[c,b] = a; theorem :: REALSET3:42 for F being Field holds for a being Element of suppf(F) holds for b,c being Element of suppf(F)\{ndf(F)} holds ovf(F).[a,ovf(F).[b,c]] = omf(F).[ovf(F).[a,b],c]; theorem :: REALSET3:43 for F being Field holds for a being Element of suppf(F) holds for b,c being Element of suppf(F)\{ndf(F)} holds ovf(F).[a,omf(F).[b,c]] = ovf(F).[ovf(F).[a,b],c];

Back to top