:: by J\'ozef Bia{\l}as

::

:: Received June 20, 1990

:: Copyright (c) 1990-2016 Association of Mizar Users

definition

((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0) is BinOp of 2

((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1) is BinOp of 2
end;

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);

((((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 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);

((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1) is BinOp of 2

proof end;

:: deftheorem defines add_2 REALSET2:def 1 :

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

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);

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 SUBSET_1:def 8;

Lm4: In (1,2) = 1

by Lm1, SUBSET_1:def 8;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

proof end;

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))}

proof end;

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)))

proof end;

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

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

proof end;

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

proof end;

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

proof end;

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

doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #) is doubleLoopStr ;

end;

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)) #);

doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #) is doubleLoopStr ;

:: deftheorem defines dL-Z_2 REALSET2:def 3 :

dL-Z_2 = doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #);

dL-Z_2 = doubleLoopStr(# 2,add_2,mult_2,(In (1,2)),(In (0,2)) #);

registration
end;

registration
end;

registration

existence

ex b_{1} being Element of dL-Z_2 st b_{1} is empty

not for b_{1} being Element of dL-Z_2 holds b_{1} is empty

end;
ex b

proof end;

existence not for b

proof 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 ) ) );

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;

coherence

not doubleLoopStr(# A,od,om,nm,nd #) is empty ;

end;
let od be BinOp of A;

let nd be Element of A;

let om be BinOp of A;

let nm be Element of A;

coherence

not doubleLoopStr(# A,od,om,nm,nd #) is empty ;

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

ex b_{1} being non degenerated doubleLoopStr st

( b_{1} is strict & b_{1} is Field-like & b_{1} is Abelian & b_{1} is distributive & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable )
end;

cluster non empty non degenerated non trivial right_complementable strict Abelian add-associative right_zeroed distributive Field-like for doubleLoopStr ;

existence ex b

( b

proof end;

registration

for b_{1} being non degenerated doubleLoopStr st b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is Abelian & b_{1} is commutative & b_{1} is associative & b_{1} is well-unital & b_{1} is distributive & b_{1} is almost_left_invertible holds

b_{1} is Field-like
end;

cluster non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative -> non degenerated Field-like for doubleLoopStr ;

coherence for b

b

proof end;

deffunc H

definition

let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ;

coherence

the multF of F is DnT of 0. F, the carrier of F by Def4;

end;
coherence

the multF of F is DnT of 0. F, the carrier of F by Def4;

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

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

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 )

for a being Element of F ex b being Element of F st

( a + b = 0. F & b + a = 0. F )

proof end;

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)

for a, b, c being Element of NonZero F holds (a * b) * c = a * (b * c)

proof end;

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

for a, b being Element of NonZero F holds a * b = b * a

proof end;

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 )

for a being Element of NonZero F holds

( a * (1. F) = a & (1. F) * a = a )

proof end;

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 )

for a being Element of NonZero F ex b being Element of NonZero F st

( a * b = 1. F & b * a = 1. F )

proof end;

theorem :: REALSET2:10

theorem :: REALSET2:11

theorem :: REALSET2:12

theorem :: REALSET2:15

theorem :: REALSET2:18

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)

for a, b, c being Element of F holds (a * b) * c = a * (b * c)

proof end;

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

for a, b being Element of F holds a * b = b * a

proof end;

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 )

for a being Element of F holds

( a * (1. F) = a & (1. F) * a = a )

proof end;

definition

let F be Field;

ex b_{1} being UnOp of (NonZero F) st

for x being Element of NonZero F holds (omf F) . (x,(b_{1} . x)) = 1. F

for b_{1}, b_{2} being UnOp of (NonZero F) st ( for x being Element of NonZero F holds (omf F) . (x,(b_{1} . x)) = 1. F ) & ( for x being Element of NonZero F holds (omf F) . (x,(b_{2} . x)) = 1. F ) holds

b_{1} = b_{2}

end;
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 for x being Element of NonZero F holds (omf F) . (x,(it . x)) = 1. F;

ex b

for x being Element of NonZero F holds (omf F) . (x,(b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines revf REALSET2:def 6 :

for F being Field

for b_{2} being UnOp of (NonZero F) holds

( b_{2} = revf F iff for x being Element of NonZero F holds (omf F) . (x,(b_{2} . x)) = 1. F );

for F being Field

for b

( b

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 )

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 )

proof end;

theorem :: REALSET2:25

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

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

proof end;

registration

for b_{1} being non degenerated doubleLoopStr st b_{1} is Field-like & b_{1} is Abelian & b_{1} is distributive & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable holds

( b_{1} is commutative & b_{1} is associative & b_{1} is well-unital & b_{1} is almost_left_invertible )
end;

cluster non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like -> non degenerated almost_left_invertible well-unital associative commutative for doubleLoopStr ;

coherence for b

( b

proof end;