:: 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
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
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 & 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
Lm7:
add_2 . (In 0 ,2),(In 1,2) = In 1,2
Lm8:
add_2 . (In 1,2),(In 0 ,2) = In 1,2
Lm9:
add_2 . (In 1,2),(In 1,2) = In 0 ,2
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
Lm14:
mult_2 . (In 0 ,2),(In 1,2) = In 0 ,2
Lm15:
mult_2 . (In 1,2),(In 0 ,2) = In 0 ,2
Lm16:
mult_2 . (In 1,2),(In 1,2) = In 1,2
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)}
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)
reconsider dL = doubleLoopStr(# A,od0,om0,nm,nd #) as non empty doubleLoopStr ;
Lm21:
for a being Element of dL holds a + (0. dL) = a
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
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
Lm25:
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 :: 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 :
:: deftheorem Def11 defines Field-like REALSET2:def 11 :
Lm26:
for F being non degenerated doubleLoopStr holds 1. F is Element of the carrier of F \ {(0. F)}
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 :: REALSET2:1
theorem :: REALSET2:2
canceled;
theorem :: REALSET2:3
canceled;
theorem :: REALSET2:4
canceled;
theorem :: REALSET2:5
canceled;
theorem :: REALSET2:6
theorem Th7: :: REALSET2:7
theorem Th8: :: REALSET2:8
theorem Th9: :: REALSET2:9
theorem Th10: :: REALSET2:10
theorem Th11: :: REALSET2:11
theorem :: REALSET2:12
theorem :: REALSET2:13
theorem :: REALSET2:14
theorem :: REALSET2:15
theorem :: REALSET2:16
theorem :: REALSET2:17
theorem :: REALSET2:18
theorem :: REALSET2:19
theorem :: REALSET2:20
theorem :: REALSET2:21
theorem :: REALSET2:22
theorem Th23: :: REALSET2:23
theorem Th24: :: REALSET2:24
theorem Th25: :: REALSET2:25
:: deftheorem REALSET2:def 16 :
canceled;
:: deftheorem REALSET2:def 17 :
canceled;
:: deftheorem Def18 defines revf REALSET2:def 18 :
theorem :: REALSET2:26
theorem :: REALSET2:27
theorem :: REALSET2:28
theorem :: REALSET2:29
theorem :: REALSET2:30
theorem :: REALSET2:31