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];