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

### Several Properties of Fields. Field Theory

by
Jozef Bialas

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