:: by Wojciech Skaba and Micha{\l} Muzalewski

::

:: Received September 27, 1990

:: Copyright (c) 1990-2016 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;

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

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

existence

ex b_{1} being Element of L st a + b_{1} = 0. L
by ALGSTR_1:def 4;

uniqueness

for b_{1}, b_{2} being Element of L st a + b_{1} = 0. L & a + b_{2} = 0. L holds

b_{1} = b_{2}
by ALGSTR_0:def 3;

end;
let a be Element of L;

existence

ex b

uniqueness

for b

b

:: deftheorem Def1 defines - ALGSTR_2:def 1 :

for L being non empty left_add-cancelable add-right-invertible addLoopStr

for a, b_{3} being Element of L holds

( b_{3} = - a iff a + b_{3} = 0. L );

for L being non empty left_add-cancelable add-right-invertible addLoopStr

for a, b

( b

definition

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

let a, b be Element of L;

correctness

coherence

a + (- b) is Element of L;

;

end;
let a, b be Element of L;

correctness

coherence

a + (- b) is Element of L;

;

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

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

ex b_{1} being non empty doubleLoopStr st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is commutative & b_{1} is associative & b_{1} is distributive & not b_{1} is degenerated & b_{1} is left_zeroed & b_{1} is right_zeroed & b_{1} is Loop-like & b_{1} is well-unital & b_{1} is multLoop_0-like )
end;

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

( b

proof end;

definition

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

end;
definition
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.

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

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

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

for a being Element of G holds - (- a) = a

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)

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.

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

( 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:9

for G being left-distributive doubleLoop

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

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.

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

( 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.

:: A Skew-Field is defined as a double sided quasi-field extended

:: with the associativity of multiplication.

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.

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

( 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.

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

:: of multiplication.

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

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

:: The F_Real example in accordance with the many theorems proved above

:: is used to prove the existence.