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;