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

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

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

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

:: Below is the basic definition of the mode of DOUBLE LOOP.
:: The F_Real example in accordance with the many theorems proved above
:: is used to prove the existence.

registration

cluster F_Real -> multLoop_0-like ;

coherence
F_Real is multLoop_0-like by Lm2, Lm3, Lm4, Lm5, ALGSTR_1:16;

end;

:: In the following part of this article the negation and minus functions
:: are defined. This is the only definition of both functions in this article
:: while some of their features are independently proved
:: for various structures.

definition

let L be non empty left_add-cancelable add-right-invertible addLoopStr ;
let a be Element of L;

func - a -> Element of L means :Def1: :: ALGSTR_2:def 1
a + it = 0. L;

existence
ex b₁ being Element of L st a + b₁ = 0. L by ALGSTR_1:def 4;
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 Def1 defines - ALGSTR_2:def 1 :
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 2
a + (- b);

correctness
coherence
a + (- b) is Element of L;
;

end;

:: deftheorem defines - ALGSTR_2:def 2 :
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 well-unital distributive associative commutative for 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;

:: The following theorem shows that the basic set of axioms of the
:: left quasi-field may be replaced with the following one,
:: by just removing a few and adding some other axioms.

theorem :: ALGSTR_2:1

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

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

proof end;

theorem Th3: :: ALGSTR_2:3

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

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

proof end;

theorem :: ALGSTR_2:5

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;

:: RIGHT QUASI-FIELD
:: The next contemplated algebraic structure is so called right quasi-field.
:: This structure is defined as a DOUBLE LOOP augmented with three axioms.
:: The reasoning is similar to that of left quasi-field.

definition

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

end;

theorem :: ALGSTR_2:6

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 Th7: :: ALGSTR_2:7

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

proof end;

theorem :: ALGSTR_2:8

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

proof end;

theorem :: ALGSTR_2:9

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

proof end;

:: DOUBLE SIDED QUASI-FIELD
:: The next contemplated algebraic structure is so called double sided
:: quasi-field. This structure is also defined as a DOUBLE LOOP augmented
:: with four axioms, while its relevance to left/right quasi-field is
:: independently contemplated.
:: The reasoning is similar to that of left/right quasi-field.

definition

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

end;

theorem :: ALGSTR_2:10

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;

:: SKEW FIELD
:: A Skew-Field is defined as a double sided quasi-field extended
:: with the associativity of multiplication.

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;

:: The following theorem shows that the basic set of axioms of the
:: skew field may be replaced with the following one,
:: by just removing a few and adding some other axioms.
:: A few theorems proved earlier are highly utilized.

theorem Th11: :: ALGSTR_2:11

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;

:: FIELD
:: A _Field is defined as a Skew-Field with the axiom of the commutativity
:: of multiplication.

definition

mode _Field is commutative _Skew-Field;

end;

theorem :: ALGSTR_2:12

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;