:: Properties of Fields
:: by J\'ozef Bia{\l}as
::
:: Received June 20, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
func add_2  ->  BinOp of 2 equals :: REALSET2:def 1
((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0);
coherence
 ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0) is BinOp of 2
proofend;
func mult_2  ->  BinOp of 2 equals :: REALSET2:def 2
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1);
coherence
 ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1) is BinOp of 2
proofend;
end;

:: deftheorem  defines add_2 REALSET2:def_1_:_
 add_2 = ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0);

:: deftheorem  defines mult_2 REALSET2:def_2_:_
 mult_2 = ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1);

set x = In (0,2);

set y = In (1,2);

Lm1:  1 in 2
by CARD_1:50, TARSKI:def_2;

Lm2:  0 in 2
by CARD_1:50, TARSKI:def_2;

then Lm3:  In (0,2) = 0
by FUNCT_7:def_1;

Lm4:  In (1,2) = 1
by Lm1, FUNCT_7:def_1;

set Z = 2;

reconsider A = 2 as non trivial set by Lm1, Lm2, ZFMISC_1:def_10;

reconsider nd = In (0,2) as Element of A ;

Lm5:  dom ((1,1) .--> 0) = {[1,1]}
by FUNCOP_1:13;

Lm6:  dom ((1,0) .--> 1) = {[1,0]}
by FUNCOP_1:13;

Lm7:  dom ((0,1) .--> 1) = {[0,1]}
by FUNCOP_1:13;

Lm8:  add_2 . ((In (0,2)),(In (0,2))) = In (0,2)
proofend;

Lm9:  add_2 . ((In (0,2)),(In (1,2))) = In (1,2)
proofend;

Lm10:  add_2 . ((In (1,2)),(In (0,2))) = In (1,2)
proofend;

Lm11:  add_2 . ((In (1,2)),(In (1,2))) = In (0,2)
proofend;

Lm12:  dom ((1,1) .--> 1) = {[1,1]}
by FUNCOP_1:13;

Lm13:  dom ((1,0) .--> 0) = {[1,0]}
by FUNCOP_1:13;

Lm14:  dom ((0,1) .--> 0) = {[0,1]}
by FUNCOP_1:13;

Lm15:  mult_2 . ((In (0,2)),(In (0,2))) = In (0,2)
proofend;

Lm16:  mult_2 . ((In (0,2)),(In (1,2))) = In (0,2)
proofend;

Lm17:  mult_2 . ((In (1,2)),(In (0,2))) = In (0,2)
proofend;

Lm18:  mult_2 . ((In (1,2)),(In (1,2))) = In (1,2)
proofend;

set om = mult_2 ;

Lm19:  A \ {(In (0,2))} = {(In (1,2))}
by Lm3, Lm4, CARD_1:50, ZFMISC_1:17;

then Lm20:  [:(A \ {(In (0,2))}),(A \ {(In (0,2))}):] = {[(In (1,2)),(In (1,2))]}
by ZFMISC_1:29;

Lm21:  for t being set st t in [:(A \ {(In (0,2))}),(A \ {(In (0,2))}):] holds
mult_2 . t in A \ {(In (0,2))}
proofend;

reconsider nm = In (1,2) as Element of A \ {nd} by Lm19, TARSKI:def_1;

reconsider od0 = add_2 as BinOp of A ;

reconsider om0 = mult_2 as BinOp of A ;

Lm22:  for a, b, d being Element of A holds add_2 . ((add_2 . (a,b)),d) = add_2 . (a,(add_2 . (b,d)))
proofend;

reconsider dL = doubleLoopStr(# A,od0,om0,nm,nd #) as non empty doubleLoopStr ;

Lm23:  for a being Element of dL holds a + (0. dL) = a
proofend;

Lm24:  for a, b, c being Element of dL holds (a + b) + c = a + (b + c)
by Lm22;

Lm25:  for a, b being Element of dL holds a + b = b + a
proofend;

reconsider om1 = mult_2 as DnT of nd,A by Lm21, REALSET1:def_6;

Lm26:  for B being non empty set
for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm holds
addLoopStr(# B,P,e #) is AbGroup
proofend;

Lm27:  for a, b, d being Element of dL holds
( a * (b + d) = (a * b) + (a * d) & (b + d) * a = (b * a) + (d * a) )
proofend;

definition
func dL-Z_2  ->  doubleLoopStr  equals :: REALSET2:def 3
 doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #);
coherence
 doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #) is doubleLoopStr ;
end;

:: deftheorem  defines dL-Z_2 REALSET2:def_3_:_
 dL-Z_2 = doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #);

registration
cluster dL-Z_2  ->  non empty non degenerated strict ;
coherence
 ( dL-Z_2 is strict & not dL-Z_2 is empty & not dL-Z_2 is degenerated )
proofend;
end;

registration
cluster dL-Z_2  ->  add-associative distributive ;
coherence
 ( dL-Z_2 is add-associative & dL-Z_2 is distributive )
proofend;
end;

registration
cluster non empty non trivial strict add-associative for doubleLoopStr ;
existence
 ex b1 being non trivial strict doubleLoopStr st b1 is add-associative
proofend;
end;

registration
cluster the carrier of dL-Z_2 ->  natural-membered ;
coherence
 the carrier of dL-Z_2 is natural-membered
proofend;
end;

registration
cluster empty for Element of the carrier of dL-Z_2;
existence
 ex b1 being Element of dL-Z_2 st b1 is empty
proofend;
cluster non empty for Element of the carrier of dL-Z_2;
existence
 not for b1 being Element of dL-Z_2 holds b1 is empty
proofend;
end;

definition
let L be doubleLoopStr ;
attrL is Field-like  means :Def4: :: REALSET2:def 4
( the multF of L is DnT of 0. L, the carrier of L & ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup ) );
end;

:: deftheorem Def4 defines Field-like REALSET2:def_4_:_
 for L being doubleLoopStr holds
( L is Field-like iff ( the multF of L is DnT of 0. L, the carrier of L & ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup ) ) );

registration
let A be non empty set ;
let od be BinOp of A;
let nd be Element of A;
let om be BinOp of A;
let nm be Element of A;
cluster doubleLoopStr(# A,od,om,nm,nd #) ->  non empty ;
coherence
 not doubleLoopStr(# A,od,om,nm,nd #) is empty ;
end;

Lm28:  for B being non empty set
for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm & P = om1 ! (A,nd) holds
addLoopStr(# B,P,e #) is AbGroup
by Lm26;

registration
cluster non empty non degenerated non trivial right_complementable strict Abelian add-associative right_zeroed distributive Field-like for doubleLoopStr ;
existence
 ex b1 being non degenerated doubleLoopStr st
( b1 is strict & b1 is Field-like & b1 is Abelian & b1 is distributive & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable )
proofend;
end;

registration
cluster non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive  ->  non degenerated Field-like for doubleLoopStr ;
coherence
 for b1 being non degenerated doubleLoopStr st b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is well-unital & b1 is distributive & b1 is almost_left_invertible holds
b1 is Field-like
proofend;
end;

deffunc H1( non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ) ->  set = the carrier of $1;

definition
let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ;
func omf F ->  DnT of 0. F, the carrier of F equals :: REALSET2:def 5
 the multF of F;
coherence
 the multF of F is DnT of 0. F, the carrier of F by Def4;
end;

:: deftheorem  defines omf REALSET2:def_5_:_
 for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr holds omf F = the multF of F;

theorem :: REALSET2:1
for F being Field holds addLoopStr(# the carrier of F, the addF of F, the ZeroF of F #) is AbGroup
proofend;

theorem :: REALSET2:2
for F being Field
for a being Element of F holds
( a + (0. F) = a & (0. F) + a = a ) by RLVECT_1:def_13;

theorem Th3: :: REALSET2:3
for F being AbGroup
for a being Element of F ex b being Element of F st
( a + b = 0. F & b + a = 0. F )
proofend;

theorem Th4: :: REALSET2:4
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b, c being Element of NonZero F holds (a * b) * c = a * (b * c)
proofend;

theorem Th5: :: REALSET2:5
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b being Element of NonZero F holds a * b = b * a
proofend;

theorem Th6: :: REALSET2:6
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a being Element of NonZero F holds
( a * (1. F) = a & (1. F) * a = a )
proofend;

theorem Th7: :: REALSET2:7
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a being Element of NonZero F ex b being Element of NonZero F st
( a * b = 1. F & b * a = 1. F )
proofend;

theorem :: REALSET2:8
for F being Field
for x, y being Element of F st x + y = 0. F holds
y = (comp F) . x
proofend;

theorem :: REALSET2:9
for F being Field
for x being Element of F holds x = (comp F) . ((comp F) . x)
proofend;

theorem :: REALSET2:10
for F being Field
for 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
for a, b, c being Element of F holds a * (b - c) = (a * b) - (a * c) by VECTSP_1:11;

theorem :: REALSET2:12
for F being Field
for a, b, c being Element of F holds (a - b) * c = (a * c) - (b * c) by VECTSP_1:13;

theorem :: REALSET2:13
for F being Field
for a being Element of F holds a * (0. F) = 0. F by VECTSP_1:6;

theorem :: REALSET2:14
for F being Field
for a being Element of F holds (0. F) * a = 0. F by VECTSP_1:7;

theorem :: REALSET2:15
for F being Field
for a, b being Element of F holds - (a * b) = a * (- b) by VECTSP_1:8;

theorem :: REALSET2:16
for F being Field holds (1. F) * (0. F) = 0. F by VECTSP_1:6;

theorem :: REALSET2:17
for F being Field holds (0. F) * (1. F) = 0. F by VECTSP_1:7;

theorem :: REALSET2:18
for F being Field
for a, b being Element of the carrier of F holds (omf F) . (a,b) is Element of the carrier of F ;

theorem Th19: :: REALSET2:19
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b, c being Element of F holds (a * b) * c = a * (b * c)
proofend;

theorem Th20: :: REALSET2:20
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b being Element of F holds a * b = b * a
proofend;

theorem Th21: :: REALSET2:21
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a being Element of F holds
( a * (1. F) = a & (1. F) * a = a )
proofend;

definition
let F be Field;
func revf F ->  UnOp of (NonZero F) means :Def6: :: REALSET2:def 6
 for x being Element of NonZero F holds (omf F) . (x,(it . x)) = 1. F;
existence
 ex b1 being UnOp of (NonZero F) st
for x being Element of NonZero F holds (omf F) . (x,(b1 . x)) = 1. F
proofend;
uniqueness
 for b1, b2 being UnOp of (NonZero F) st ( for x being Element of NonZero F holds (omf F) . (x,(b1 . x)) = 1. F ) & ( for x being Element of NonZero F holds (omf F) . (x,(b2 . x)) = 1. F ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines revf REALSET2:def_6_:_
 for F being Field
for b2 being UnOp of (NonZero F) holds
( b2 = revf F iff for x being Element of NonZero F holds (omf F) . (x,(b2 . x)) = 1. F );

theorem :: REALSET2:22
for F being Field
for x, y being Element of NonZero F st x * y = 1. F holds
y = (revf F) . x
proofend;

theorem :: REALSET2:23
for F being Field
for x being Element of NonZero F holds x = (revf F) . ((revf F) . x)
proofend;

theorem :: REALSET2:24
for F being Field
for 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 )
proofend;

theorem :: REALSET2:25
for F being Field
for a, b, c being Element of F st a + b = a + c holds
b = c by RLVECT_1:8;

theorem :: REALSET2:26
for F being Field
for a being Element of NonZero F
for b, c being Element of the carrier of F st a * b = a * c holds
b = c
proofend;

registration
cluster non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like  ->  non degenerated almost_left_invertible associative commutative well-unital for doubleLoopStr ;
coherence
 for b1 being non degenerated doubleLoopStr st b1 is Field-like & b1 is Abelian & b1 is distributive & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable holds
( b1 is commutative & b1 is associative & b1 is well-unital & b1 is almost_left_invertible )
proofend;
end;