:: Several Properties of Fields. Field Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies VECTSP_1, REALSET2, FUNCT_1, MESFUNC1, SUBSET_1, STRUCT_0,
RELAT_1, ARYTM_1, ARYTM_3, SUPINF_2, ALGSTR_0, BINOP_1, ZFMISC_1,
REALSET3;
notations TARSKI, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, BINOP_1, STRUCT_0,
ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, REALSET2;
constructors BINOP_1, REALSET2, RELSET_1;
registrations RELSET_1, STRUCT_0, REALSET2;
requirements SUBSET, BOOLE;
begin
:: Properties of fields
theorem :: REALSET3:1
for F being Field holds revf(F).1.F = 1.F;
theorem :: REALSET3:2
for F being Field holds for a,b being Element of NonZero F holds
revf(F).(omf(F).(a,revf(F).b)) = omf(F).(b,revf(F).a);
theorem :: REALSET3:3
for F being Field, a,b being Element of NonZero F holds revf(F).(
omf(F).(a,b)) = omf(F).(revf(F).a,revf(F).b);
theorem :: REALSET3:4
for F being Field holds for a,b,c,d being Element
of F holds a-b = c-d iff a+d = b+c;
theorem :: REALSET3:5
for F being Field holds for a,c being Element of F
holds for b,d being Element of NonZero 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:6
for F being Field holds for a,b being Element of F
holds for c,d being Element of NonZero 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:7
for F being Field holds for a,b being Element of F
holds for c,d being Element of NonZero F holds (the addF of F).(omf(F).(a,revf(
F).c),omf(F).(b,revf(F).d)) = omf(F).((the addF of 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 the carrier of F means
:: REALSET3:def 1
for x,y being Element of F holds it.(x,y) = (the addF of F).(x,(comp F).y);
end;
theorem :: REALSET3:8
for F being Field holds for x being Element of F holds osf(F).(x,x) = 0.F;
theorem :: REALSET3:9
for F being Field holds for a,b,c being Element
of F holds omf(F).(a,osf(F).(b,c)) = osf(F).(omf(F).(a,b),omf(F).(a,c));
theorem :: REALSET3:10
for F being Field holds for a,b,c being Element of F
holds omf(F).(osf(F).(a,b),c) = osf(F).(omf(F).(a,c),omf(F).(b,c));
theorem :: REALSET3:11
for F being Field holds for a,b being Element of F
holds osf(F).(a,b) = (comp F).(osf(F).(b,a));
theorem :: REALSET3:12
for F being Field holds for a,b being Element of F
holds osf(F).((comp F).a,b) = (comp F).((the addF of F).(a,b));
theorem :: REALSET3:13
for F being Field holds for a,b,c,d being Element
of F holds osf(F).(a,b) = osf(F).(c,d) iff a+d = b+c;
theorem :: REALSET3:14
for F being Field holds for a being Element of F holds
osf(F).(0.F,a) = (comp F).a;
theorem :: REALSET3:15
for F being Field holds for a being Element of F holds osf(F).(a,0.F) = a;
theorem :: REALSET3:16
for F being Field holds for a,b,c being Element of F
holds a+b = c iff osf(F).(c,a) = b;
theorem :: REALSET3:17
for F being Field holds for a,b,c being Element of F
holds a+b = c iff osf(F).(c,b) = a;
theorem :: REALSET3:18
for F being Field holds for a,b,c being Element of F
holds osf(F).(a,osf(F).(b,c)) = (the addF of F).(osf(F).(a,b),c);
theorem :: REALSET3:19
for F being Field holds for a,b,c being Element of F
holds osf(F).(a,(the addF of F).(b,c)) = osf(F).(osf(F).(a,b),c);
definition ::division.
let F be Field;
func ovf(F) -> Function of [:the carrier of F, NonZero F:],the carrier of F
means
:: REALSET3:def 2
for x being Element of F, y being Element of
NonZero F holds it.(x,y) = omf(F).(x,revf(F).y);
end;
theorem :: REALSET3:20
for F being Field holds for x being Element of NonZero F holds
ovf(F).(x,x) = 1.F;
theorem :: REALSET3:21
for F being Field holds for a,b being Element of
F holds for c being Element of NonZero F holds omf(F).(a,ovf(F).(b,c)) = ovf(F)
.(omf(F).(a,b),c);
theorem :: REALSET3:22
for F being Field holds for a being Element of NonZero F holds omf(F).
(a,ovf(F).(1.F,a)) = 1.F & omf(F).(ovf(F).(1.F,a),a) = 1.F;
theorem :: REALSET3:23
for F being Field holds for a,b being Element of NonZero F holds ovf(F
).(a,b) = revf(F).(ovf(F).(b,a));
theorem :: REALSET3:24
for F being Field holds for a,b being Element of NonZero F holds ovf(F
).(revf(F).a,b) = revf(F).(omf(F).(a,b));
theorem :: REALSET3:25
for F being Field holds for a,c being Element of
F holds for b,d being Element of NonZero F holds ovf(F).(a,b) = ovf(F).(c,d)
iff omf(F).(a,d) = omf(F).(b,c);
theorem :: REALSET3:26
for F being Field holds for a being Element of NonZero F holds ovf(F).
(1.F,a) = revf(F).a;
theorem :: REALSET3:27
for F being Field holds for a being Element of F holds ovf(F).(a,1.F) = a;
theorem :: REALSET3:28
for F being Field holds for a being Element of NonZero F holds for b,c
being Element of F holds omf(F).(a,b) = c iff ovf(F).(c,a) = b;
theorem :: REALSET3:29
for F being Field holds for a,c being Element of F
holds for b being Element of NonZero F holds omf(F).(a,b) = c iff ovf(F).(c,b)
= a;
theorem :: REALSET3:30
for F being Field holds for a being Element of F holds
for b,c being Element of NonZero F holds ovf(F).(a,ovf(F).(b,c)) = omf(F).(ovf(
F).(a,b),c);
theorem :: REALSET3:31
for F being Field holds for a being Element of F holds
for b,c being Element of NonZero F holds ovf(F).(a,omf(F).(b,c)) = ovf(F).(ovf(
F).(a,b),c);