begin
definition
canceled;canceled;canceled;canceled;canceled;canceled;canceled;func add_2 -> BinOp of 2
equals
(((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
func mult_2 -> BinOp of 2
equals
(((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
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 :
:: deftheorem defines mult_2 REALSET2:def 9 :
set x = In 0 ,2;
set y = In 1,2;
Lm1:
1 in 2
by CARD_1:88, TARSKI:def 2;
Lm2:
0 in 2
by CARD_1:88, 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, REALSET1:14;
reconsider nd = In 0 ,2 as Element of A ;
Lm5:
dom (1,1 .--> 0 ) = {[1,1]}
by FUNCOP_1:19;
Lm6:
dom (1,0 .--> 1) = {[1,0 ]}
by FUNCOP_1:19;
Lm7:
dom (0 ,1 .--> 1) = {[0 ,1]}
by FUNCOP_1:19;
Lm8:
add_2 . (In 0 ,2),(In 0 ,2) = In 0 ,2
Lm9:
add_2 . (In 0 ,2),(In 1,2) = In 1,2
Lm10:
add_2 . (In 1,2),(In 0 ,2) = In 1,2
Lm11:
add_2 . (In 1,2),(In 1,2) = In 0 ,2
Lm12:
dom (1,1 .--> 1) = {[1,1]}
by FUNCOP_1:19;
Lm13:
dom (1,0 .--> 0 ) = {[1,0 ]}
by FUNCOP_1:19;
Lm14:
dom (0 ,1 .--> 0 ) = {[0 ,1]}
by FUNCOP_1:19;
Lm15:
mult_2 . (In 0 ,2),(In 0 ,2) = In 0 ,2
Lm16:
mult_2 . (In 0 ,2),(In 1,2) = In 0 ,2
Lm17:
mult_2 . (In 1,2),(In 0 ,2) = In 0 ,2
Lm18:
mult_2 . (In 1,2),(In 1,2) = In 1,2
set om = mult_2 ;
Lm19:
A \ {(In 0 ,2)} = {(In 1,2)}
by Lm3, Lm4, CARD_1:88, ZFMISC_1:23;
then Lm20:
[:(A \ {(In 0 ,2)}),(A \ {(In 0 ,2)}):] = {[(In 1,2),(In 1,2)]}
by ZFMISC_1:35;
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)}
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)
reconsider dL = doubleLoopStr(# A,od0,om0,nm,nd #) as non empty doubleLoopStr ;
Lm23:
for a being Element of dL holds a + (0. dL) = a
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
reconsider om1 = mult_2 as DnT of nd,A by Lm21, REALSET1:def 8;
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
Lm27:
for a, b, d being Element of dL holds
( a * (b + d) = (a * b) + (a * d) & (b + d) * a = (b * a) + (d * a) )
definition
func dL-Z_2 -> doubleLoopStr equals
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 :
:: deftheorem Def11 defines Field-like REALSET2:def 11 :
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;
deffunc H1( non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ) -> set = the carrier of $1;
:: deftheorem REALSET2:def 12 :
canceled;
:: deftheorem REALSET2:def 13 :
canceled;
:: deftheorem REALSET2:def 14 :
canceled;
:: deftheorem defines omf REALSET2:def 15 :
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th23:
theorem Th24:
theorem Th25:
:: deftheorem REALSET2:def 16 :
canceled;
:: deftheorem REALSET2:def 17 :
canceled;
:: deftheorem Def18 defines revf REALSET2:def 18 :
theorem
theorem
theorem
theorem
theorem