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

definition

canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
func add_2 -> BinOp of 2 equals :: REALSET2:def 8
(((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

proof end;

func mult_2 -> BinOp of 2 equals :: REALSET2:def 9
(((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

proof end;

end;

:: deftheorem REALSET2:def 1 :

canceled;

:: deftheorem REALSET2:def 2 :

canceled;

:: deftheorem REALSET2:def 3 :

canceled;

:: deftheorem REALSET2:def 4 :

canceled;

:: deftheorem REALSET2:def 5 :

canceled;

:: deftheorem REALSET2:def 6 :

canceled;

:: deftheorem REALSET2:def 7 :

canceled;

:: deftheorem defines add_2 REALSET2:def 8 :

add_2 = (((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1)) +* (1,1 .--> 0 );

:: deftheorem defines mult_2 REALSET2:def 9 :

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 & 0 in 2 )
by CARD_1:88, TARSKI:def 2;

then Lm2: ( In 0 ,2 = 0 & In 1,2 = 1 )
by FUNCT_7:def 1;

set Z = 2;

reconsider A = 2 as non trivial set by Lm1, REALSET1:14;

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

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

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

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

Lm6: add_2 . (In 0 ,2),(In 0 ,2) = In 0 ,2

proof end;

Lm7: add_2 . (In 0 ,2),(In 1,2) = In 1,2

proof end;

Lm8: add_2 . (In 1,2),(In 0 ,2) = In 1,2

proof end;

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

proof end;

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

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

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

Lm13: mult_2 . (In 0 ,2),(In 0 ,2) = In 0 ,2

proof end;

Lm14: mult_2 . (In 0 ,2),(In 1,2) = In 0 ,2

proof end;

Lm15: mult_2 . (In 1,2),(In 0 ,2) = In 0 ,2

proof end;

Lm16: mult_2 . (In 1,2),(In 1,2) = In 1,2

proof end;

set om = mult_2 ;

Lm17: A \ {(In 0 ,2)} = {(In 1,2)}
by Lm2, CARD_1:88, ZFMISC_1:23;

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

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

proof end;

reconsider nm = In 1,2 as Element of A \ {nd} by Lm17, TARSKI:def 1;

reconsider od0 = add_2 as BinOp of A ;

reconsider om0 = mult_2 as BinOp of A ;

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

proof end;

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

Lm21: for a being Element of dL holds a + (0. dL) = a

proof end;

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

Lm23: for a, b being Element of dL holds a + b = b + a

proof end;

reconsider om1 = mult_2 as DnT of nd,A by Lm19, REALSET1:def 8;

Lm24: 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

proof end;

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

proof end;

definition

func dL-Z_2 -> doubleLoopStr equals :: REALSET2:def 10
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 10 :

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 )

proof end;

end;

registration

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

proof end;

end;

registration

cluster non empty non trivial strict add-associative doubleLoopStr ;
existence
ex b₁ being non empty non trivial strict doubleLoopStr st b₁ is add-associative

proof end;

end;

registration

cluster -> natural Element of the carrier of dL-Z_2 ;
coherence
for b₁ being Element of dL-Z_2 holds b₁ is natural by CARD_1:88, TARSKI:def 2;

end;

registration

cluster empty natural Element of the carrier of dL-Z_2 ;
existence
ex b₁ being Element of dL-Z_2 st b₁ is empty

proof end;

cluster non empty natural Element of the carrier of dL-Z_2 ;
existence
not for b₁ being Element of dL-Z_2 holds b₁ is empty

proof end;

end;

definition

let L be non trivial doubleLoopStr ;
attr L is Field-like means :Def11: :: REALSET2:def 11
( 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 = the carrier of L \ {(0. L)} & e = 1. L & P = the multF of L || (the carrier of L \ {(0. L)}) holds
addLoopStr(# B,P,e #) is AbGroup ) );

end;

:: deftheorem Def11 defines Field-like REALSET2:def 11 :

for L being non trivial 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 = the carrier of L \ {(0. L)} & e = 1. L & P = the multF of L || (the carrier of L \ {(0. L)}) holds
addLoopStr(# B,P,e #) is AbGroup ) ) );

registration

let A be non trivial 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;

registration

cluster non trivial -> non empty doubleLoopStr ;
coherence
for b₁ being doubleLoopStr st not b₁ is trivial holds
not b₁ is empty ;

end;

registration

cluster non empty non degenerated right_complementable strict Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ;
existence
ex b₁ being non degenerated doubleLoopStr st
( b₁ is strict & b₁ is Field-like & b₁ is Abelian & b₁ is distributive & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable )

proof end;

end;

registration

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

proof end;

end;

Lm26: for F being non degenerated doubleLoopStr holds 1. F is Element of the carrier of F \ {(0. F)}

proof end;

deffunc H₁( 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 ;
canceled;
canceled;
canceled;
func omf F -> DnT of 0. F,the carrier of F equals :: REALSET2:def 15
the multF of F;
coherence
the multF of F is DnT of 0. F,the carrier of F by Def11;

end;

:: deftheorem REALSET2:def 12 :

canceled;

:: deftheorem REALSET2:def 13 :

canceled;

:: deftheorem REALSET2:def 14 :

canceled;

:: deftheorem defines omf REALSET2:def 15 :

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 U2 of F #) is AbGroup

proof end;

theorem :: REALSET2:2

canceled;

theorem :: REALSET2:3

canceled;

theorem :: REALSET2:4

canceled;

theorem :: REALSET2:5

canceled;

theorem :: REALSET2:6

for F being Field
for a being Element of F holds
( a + (0. F) = a & (0. F) + a = a ) by RLVECT_1:def 15;

theorem Th7: :: REALSET2:7

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 )

proof end;

theorem Th8: :: REALSET2:8

for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b, c being Element of the carrier of F \ {(0. F)} holds (a * b) * c = a * (b * c)

proof end;

theorem Th9: :: REALSET2:9

for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b being Element of the carrier of F \ {(0. F)} holds a * b = b * a

proof end;

theorem Th10: :: REALSET2:10

for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a being Element of the carrier of F \ {(0. F)} holds
( a * (1. F) = a & (1. F) * a = a )

proof end;

theorem Th11: :: REALSET2:11

for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a being Element of the carrier of F \ {(0. F)} ex b being Element of the carrier of F \ {(0. F)} st
( a * b = 1. F & b * a = 1. F )

proof end;

theorem :: REALSET2:12

for F being Field
for x, y being Element of F st x + y = 0. F holds
y = (comp F) . x

proof end;

theorem :: REALSET2:13

for F being Field
for x being Element of F holds x = (comp F) . ((comp F) . x)

proof end;

theorem :: REALSET2:14

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:15

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

theorem :: REALSET2:16

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

theorem :: REALSET2:17

for F being Field
for a being Element of F holds a * (0. F) = 0. F by VECTSP_1:36;

theorem :: REALSET2:18

for F being Field
for a being Element of F holds (0. F) * a = 0. F by VECTSP_1:39;

theorem :: REALSET2:19

for F being Field
for a, b being Element of F holds - (a * b) = a * (- b) by VECTSP_1:40;

theorem :: REALSET2:20

for F being Field holds (1. F) * (0. F) = 0. F by VECTSP_1:36;

theorem :: REALSET2:21

for F being Field holds (0. F) * (1. F) = 0. F by VECTSP_1:39;

theorem :: REALSET2:22

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 Th23: :: REALSET2:23

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)

proof end;

theorem Th24: :: REALSET2:24

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

proof end;

theorem Th25: :: REALSET2:25

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 )

proof end;

definition

let F be Field;
canceled;
canceled;
func revf F -> UnOp of the carrier of F \ {(0. F)} means :Def18: :: REALSET2:def 18
for x being Element of the carrier of F \ {(0. F)} holds (omf F) . x,(it . x) = 1. F;
existence
ex b₁ being UnOp of the carrier of F \ {(0. F)} st
for x being Element of the carrier of F \ {(0. F)} holds (omf F) . x,(b₁ . x) = 1. F

proof end;

uniqueness
for b₁, b₂ being UnOp of the carrier of F \ {(0. F)} st ( for x being Element of the carrier of F \ {(0. F)} holds (omf F) . x,(b₁ . x) = 1. F ) & ( for x being Element of the carrier of F \ {(0. F)} holds (omf F) . x,(b₂ . x) = 1. F ) holds
b₁ = b₂

proof end;

end;

:: deftheorem REALSET2:def 16 :

canceled;

:: deftheorem REALSET2:def 17 :

canceled;

:: deftheorem Def18 defines revf REALSET2:def 18 :

for F being Field
for b₂ being UnOp of the carrier of F \ {(0. F)} holds
( b₂ = revf F iff for x being Element of the carrier of F \ {(0. F)} holds (omf F) . x,(b₂ . x) = 1. F );

theorem :: REALSET2:26

for F being Field
for x, y being Element of the carrier of F \ {(0. F)} st x * y = 1. F holds
y = (revf F) . x

proof end;

theorem :: REALSET2:27

for F being Field
for x being Element of the carrier of F \ {(0. F)} holds x = (revf F) . ((revf F) . x)

proof end;

theorem :: REALSET2:28

for F being Field
for a, b being Element of the carrier of F \ {(0. F)} holds
( (omf F) . a,b is Element of the carrier of F \ {(0. F)} & (revf F) . a is Element of the carrier of F \ {(0. F)} )

proof end;

theorem :: REALSET2:29

for F being Field
for a, b, c being Element of F st a + b = a + c holds
b = c by RLVECT_1:21;

theorem :: REALSET2:30

for F being Field
for a being Element of the carrier of F \ {(0. F)}
for b, c being Element of the carrier of F st a * b = a * c holds
b = c

proof end;

registration

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

proof end;

end;

theorem :: REALSET2:31

for F being non degenerated doubleLoopStr holds 1. F is Element of the carrier of F \ {(0. F)} by Lm26;