:: From Double Loops to Fields
:: by Wojciech Skaba and Micha{\l} Muzalewski
::
:: Received September 27, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

Lm1: 0 = 0. F_Real
by STRUCT_0:def 6, VECTSP_1:def 15;

Lm2: for a, b being Element of F_Real st a <> 0. F_Real holds
ex x being Element of F_Real st a * x = b

proof end;

Lm3: for a, b being Element of F_Real st a <> 0. F_Real holds
ex x being Element of F_Real st x * a = b

proof end;

Lm4: ( ( for a, x, y being Element of F_Real st a <> 0. F_Real & a * x = a * y holds
x = y ) & ( for a, x, y being Element of F_Real st a <> 0. F_Real & x * a = y * a holds
x = y ) )
by VECTSP_1:33;

Lm5: ( ( for a being Element of F_Real holds a * (0. F_Real) = 0. F_Real ) & ( for a being Element of F_Real holds (0. F_Real) * a = 0. F_Real ) )
by VECTSP_1:44;

registration

cluster F_Real -> multLoop_0-like ;
coherence
F_Real is multLoop_0-like by Lm2, Lm3, Lm4, Lm5, ALGSTR_1:34;

end;

definition

let L be non empty left_add-cancelable add-right-invertible addLoopStr ;
let a be Element of L;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
func - a -> Element of L means :Def7: :: ALGSTR_2:def 7
a + it = 0. L;
existence
ex b₁ being Element of L st a + b₁ = 0. L by ALGSTR_1:def 9;
uniqueness
for b₁, b₂ being Element of L st a + b₁ = 0. L & a + b₂ = 0. L holds
b₁ = b₂ by ALGSTR_0:def 3;

end;

:: deftheorem ALGSTR_2:def 1 :
canceled;

:: deftheorem ALGSTR_2:def 2 :
canceled;

:: deftheorem ALGSTR_2:def 3 :
canceled;

:: deftheorem ALGSTR_2:def 4 :
canceled;

:: deftheorem ALGSTR_2:def 5 :
canceled;

:: deftheorem ALGSTR_2:def 6 :
canceled;

:: deftheorem Def7 defines - ALGSTR_2:def 7 :
for L being non empty left_add-cancelable add-right-invertible addLoopStr
for a, b₃ being Element of L holds
( b₃ = - a iff a + b₃ = 0. L );

definition

let L be non empty left_add-cancelable add-right-invertible addLoopStr ;
let a, b be Element of L;
func a - b -> Element of L equals :: ALGSTR_2:def 8
a + (- b);
correctness
coherence
a + (- b) is Element of L;
;

end;

:: deftheorem defines - ALGSTR_2:def 8 :
for L being non empty left_add-cancelable add-right-invertible addLoopStr
for a, b being Element of L holds a - b = a + (- b);

registration

cluster non empty non degenerated strict left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
existence
ex b₁ being non empty doubleLoopStr st
( b₁ is strict & b₁ is Abelian & b₁ is add-associative & b₁ is commutative & b₁ is associative & b₁ is distributive & not b₁ is degenerated & b₁ is left_zeroed & b₁ is right_zeroed & b₁ is Loop-like & b₁ is well-unital & b₁ is multLoop_0-like )

proof end;

end;

definition

mode doubleLoop is non empty left_zeroed Loop-like multLoop_0-like right_zeroed well-unital doubleLoopStr ;

end;

definition

mode leftQuasi-Field is non degenerated Abelian add-associative right-distributive doubleLoop;

end;

theorem :: ALGSTR_2:1

canceled;

theorem :: ALGSTR_2:2

canceled;

theorem :: ALGSTR_2:3

canceled;

theorem :: ALGSTR_2:4

canceled;

theorem :: ALGSTR_2:5

canceled;

theorem :: ALGSTR_2:6

canceled;

theorem :: ALGSTR_2:7

canceled;

theorem :: ALGSTR_2:8

canceled;

theorem :: ALGSTR_2:9

canceled;

theorem :: ALGSTR_2:10

canceled;

theorem :: ALGSTR_2:11

canceled;

theorem :: ALGSTR_2:12

for L being non empty doubleLoopStr holds
( L is leftQuasi-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) ) )

proof end;

theorem :: ALGSTR_2:13

canceled;

theorem Th14: :: ALGSTR_2:14

for G being Abelian right-distributive doubleLoop
for a, b being Element of G holds a * (- b) = - (a * b)

proof end;

theorem Th15: :: ALGSTR_2:15

for G being non empty left_add-cancelable add-right-invertible Abelian addLoopStr
for a being Element of G holds - (- a) = a

proof end;

theorem :: ALGSTR_2:16

for G being Abelian right-distributive doubleLoop holds (- (1. G)) * (- (1. G)) = 1. G

proof end;

theorem :: ALGSTR_2:17

for G being Abelian right-distributive doubleLoop
for a, x, y being Element of G holds a * (x - y) = (a * x) - (a * y)

proof end;

definition

mode rightQuasi-Field is non degenerated Abelian add-associative left-distributive doubleLoop;

end;

theorem :: ALGSTR_2:18

canceled;

theorem :: ALGSTR_2:19

for L being non empty doubleLoopStr holds
( L is rightQuasi-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )

proof end;

theorem :: ALGSTR_2:20

canceled;

theorem Th21: :: ALGSTR_2:21

for G being left-distributive doubleLoop
for b, a being Element of G holds (- b) * a = - (b * a)

proof end;

theorem :: ALGSTR_2:22

canceled;

theorem :: ALGSTR_2:23

for G being Abelian left-distributive doubleLoop holds (- (1. G)) * (- (1. G)) = 1. G

proof end;

theorem :: ALGSTR_2:24

for G being left-distributive doubleLoop
for x, y, a being Element of G holds (x - y) * a = (x * a) - (y * a)

proof end;

definition

mode doublesidedQuasi-Field is non degenerated Abelian add-associative distributive doubleLoop;

end;

theorem :: ALGSTR_2:25

canceled;

theorem :: ALGSTR_2:26

for L being non empty doubleLoopStr holds
( L is doublesidedQuasi-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )

proof end;

definition

mode _Skew-Field is associative doublesidedQuasi-Field;

end;

Lm6: for L being non empty doubleLoopStr
for a, b being Element of L st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & a * b = 1. L holds
b * a = 1. L

proof end;

Lm7: for L being non empty doubleLoopStr
for a being Element of L st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) holds
(1. L) * a = a * (1. L)

proof end;

Lm8: for L being non empty doubleLoopStr st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) holds
for a being Element of L st a <> 0. L holds
ex x being Element of L st x * a = 1. L

proof end;

theorem :: ALGSTR_2:27

canceled;

theorem :: ALGSTR_2:28

canceled;

theorem :: ALGSTR_2:29

canceled;

theorem :: ALGSTR_2:30

canceled;

theorem :: ALGSTR_2:31

canceled;

theorem Th32: :: ALGSTR_2:32

for L being non empty doubleLoopStr holds
( L is _Skew-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )

proof end;

definition

mode _Field is commutative _Skew-Field;

end;

theorem :: ALGSTR_2:33

canceled;

theorem :: ALGSTR_2:34

for L being non empty doubleLoopStr holds
( L is _Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) )

proof end;