Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Properties of Fields

by
Jozef Bialas

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;

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;

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