:: Properties of Fields
:: by J\'ozef Bia{\l}as
::
:: Received June 20, 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 BINOP_1, CARD_1, FUNCOP_1, FUNCT_4, RELAT_1, XBOOLE_0, ZFMISC_1,
TARSKI, FUNCT_7, SUBSET_1, FUNCT_1, ALGSTR_0, ARYTM_3, SUPINF_2,
REALSET1, VECTSP_1, STRUCT_0, MESFUNC1, RLVECT_1, LATTICES, ARYTM_1,
REALSET2, MEMBERED;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
ORDINAL1, NUMBERS, REALSET1, FUNCOP_1, FUNCT_2, BINOP_1, FUNCT_4,
FUNCT_7, MEMBERED, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1;
constructors RLVECT_1, BINOP_1, FUNCT_4, REALSET1, FUNCT_7, VECTSP_1,
RELSET_1, MEMBERED, GROUP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, STRUCT_0, RLVECT_1,
VECTSP_1, ORDINAL1, ALGSTR_0, ZFMISC_1, CARD_1;
requirements SUBSET, BOOLE, NUMERALS;
begin
definition
func add_2 -> BinOp of 2 equals
:: REALSET2:def 1
((0,0) .--> 0) +* ((0,1).-->1) +* ((1,0).-->1) +* ((1,1).-->0);
func mult_2 -> BinOp of 2 equals
:: REALSET2:def 2
((0,0).-->0) +* ((0,1).-->0) +* ((1,0).-->0) +* ((1,1).-->1);
end;
reserve x,y for set;
definition
func dL-Z_2 -> doubleLoopStr equals
:: REALSET2:def 3
doubleLoopStr(#2,add_2,mult_2,In(1,2),In(0,2)#);
end;
registration
cluster dL-Z_2 -> strict non empty non degenerated;
end;
registration
cluster dL-Z_2 -> add-associative distributive;
end;
registration
cluster add-associative for non trivial strict doubleLoopStr;
end;
registration
cluster the carrier of dL-Z_2 -> natural-membered;
end;
registration
cluster empty for Element of dL-Z_2;
cluster non empty for Element of dL-Z_2;
end;
definition
let L be doubleLoopStr;
attr L is Field-like means
:: REALSET2:def 4
the multF of L is ((the carrier of L)\{0.L})-subsetpreserving &
for B being non empty set, P being BinOp of B, e being Element of B
holds B = NonZero L & e = 1.L & P = (the multF of L)||NonZero L implies
addLoopStr(#B,P,e#) is AbGroup;
end;
registration
let A be non empty set, od be BinOp of A, nd be Element of A,
om be BinOp of A, nm be Element of A;
cluster doubleLoopStr(#A,od,om,nm,nd#) -> non empty;
end;
registration
cluster strict Field-like Abelian distributive add-associative right_zeroed
right_complementable for non degenerated doubleLoopStr;
end;
registration
cluster add-associative right_zeroed right_complementable Abelian
commutative associative well-unital distributive almost_left_invertible ->
Field-like for non degenerated doubleLoopStr;
end;
definition
let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr;
func omf(F) -> ((the carrier of F) \ {0.F})-subsetpreserving BinOp of F
equals
:: REALSET2:def 5
the multF of F;
end;
theorem :: REALSET2:1
for F being Field holds the addLoopStr of F is AbGroup;
theorem :: REALSET2:2
for F being Field, a being Element of F holds a+0.F = a & 0.F+a = a;
theorem :: REALSET2:3
for F being AbGroup, a being Element of F
ex b being Element of F st a+b = 0.F & b+a = 0.F;
theorem :: REALSET2:4
for F being Field-like Abelian distributive add-associative
right_zeroed right_complementable non degenerated doubleLoopStr,
a,b,c being Element of NonZero F holds (a*b)*c = a*(b*c);
theorem :: REALSET2:5
for F being Field-like Abelian distributive add-associative
right_zeroed right_complementable non degenerated doubleLoopStr, a,b being
Element of NonZero F holds a*b = b*a;
theorem :: REALSET2:6
for F being Field-like Abelian distributive add-associative
right_zeroed right_complementable non degenerated doubleLoopStr, a being
Element of NonZero F holds a*1.F = a & 1.F*a = a;
theorem :: REALSET2:7
for F being Field-like Abelian distributive add-associative
right_zeroed right_complementable non degenerated doubleLoopStr, a being
Element of NonZero F ex b being Element of NonZero F st a*b = 1.F & b*a = 1.F
;
theorem :: REALSET2:8
for F being Field, x,y being Element of F holds x+y = 0.F implies
y = (comp F).x;
theorem :: REALSET2:9
for F being Field, x being Element of F holds x = (comp F).((comp F).x );
theorem :: REALSET2:10
for F being Field, a,b being Element of (the carrier of F)holds (the
addF of F).(a,b) is Element of (the carrier of F)& omf(F).(a,b) is Element of (
the carrier of F)& (comp F).a is Element of the carrier of F;
theorem :: REALSET2:11
for F being Field, a,b,c being Element of F holds a*(b-c) = a*b-a*c;
theorem :: REALSET2:12
for F being Field, a,b,c being Element of F holds (a-b)*c = a*c-b*c;
theorem :: REALSET2:13
for F being Field, a being Element of F holds a*0.F = 0.F;
theorem :: REALSET2:14
for F being Field, a being Element of F holds 0.F*a = 0.F;
theorem :: REALSET2:15
for F being Field, a,b being Element of F holds -(a*b) = a*-b;
theorem :: REALSET2:16
for F being Field holds 1.F*0.F = 0.F;
theorem :: REALSET2:17
for F being Field holds 0.F*1.F = 0.F;
theorem :: REALSET2:18
for F being Field, a,b being Element of (the carrier of F)holds omf(F)
.(a,b) is Element of the carrier of F;
theorem :: REALSET2:19
for F being Field-like Abelian distributive add-associative
right_zeroed right_complementable non degenerated doubleLoopStr, a,b,c being
Element of F holds (a*b)*c = a*(b*c);
theorem :: REALSET2:20
for F being Field-like Abelian distributive add-associative
right_zeroed right_complementable non degenerated doubleLoopStr, a,b being
Element of F holds a*b = b*a;
theorem :: REALSET2:21
for F being Field-like Abelian distributive add-associative
right_zeroed right_complementable non degenerated doubleLoopStr, a being
Element of F holds a*1.F = a & 1.F*a = a;
definition
let F be Field;
func revf(F) -> UnOp of NonZero F means
:: REALSET2:def 6
for x being Element of NonZero F holds omf(F).(x,it.x) = 1.F;
end;
theorem :: REALSET2:22
for F being Field, x,y being Element of NonZero F holds x*y = 1.F
implies y = revf(F).x;
theorem :: REALSET2:23
for F being Field, x being Element of NonZero F holds x =revf(F).(revf (F).x)
;
theorem :: REALSET2:24
for F being Field, a,b being Element of NonZero F holds
omf(F).(a,b) is Element of NonZero F & revf(F).a is Element of NonZero F;
theorem :: REALSET2:25
for F being Field, a,b,c being Element of F holds a+b = a+c implies
b = c;
theorem :: REALSET2:26
for F being Field, a being Element of NonZero F,
b,c being Element of F holds a*b = a*c implies b = c;
registration
cluster Field-like Abelian distributive add-associative right_zeroed
right_complementable -> commutative associative well-unital
almost_left_invertible for non degenerated doubleLoopStr;
end;