Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### From Double Loops to Fields

by
Wojciech Skaba, and
Michal Muzalewski

MML identifier: ALGSTR_2
[ Mizar article, MML identifier index ]

```environ

vocabulary VECTSP_1, FUNCT_1, RLVECT_1, ALGSTR_1, VECTSP_2, ARYTM_1, LATTICES,
BINOP_1, ALGSTR_2;
notation REAL_1, BINOP_1, STRUCT_0, RLVECT_1, VECTSP_1, VECTSP_2, ALGSTR_1;
constructors BINOP_1, ALGSTR_1, VECTSP_2, REAL_1, MEMBERED, XBOOLE_0;
clusters VECTSP_1, ALGSTR_1, VECTSP_2, MEMBERED, ZFMISC_1, XBOOLE_0;

begin :: DOUBLE LOOPS

reserve L for non empty doubleLoopStr;

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

definition
cluster F_Real -> multLoop_0-like;
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 a be Element of L;
canceled 6;

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

definition
let a,b be Element of L;
func a-b -> Element of L equals
:: ALGSTR_2:def 8
a+ -b;
end;

definition
cluster strict Abelian add-associative commutative associative distributive
non degenerated left_zeroed right_zeroed Loop-like well-unital
multLoop_0-like (non empty doubleLoopStr);
end;

definition
mode doubleLoop is left_zeroed right_zeroed Loop-like
well-unital multLoop_0-like (non empty doubleLoopStr);
end;

definition
right-distributive non degenerated doubleLoop;
end;

reserve a,b,c,x,y,z for Element of L;

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

canceled 11;

theorem :: ALGSTR_2:12
L is leftQuasi-Field iff
(for a holds a + 0.L = a)
& (for a ex x st a+x = 0.L)
& (for a,b,c holds (a+b)+c = a+(b+c))
& (for a,b holds a+b = b+a)
& 0.L <> 1_ L
& (for a holds a * 1_ L = a)
& (for a holds 1_ L * a = a)
& (for a,b st a<>0.L ex x st a*x=b)
& (for a,b st a<>0.L ex x st x*a=b)
& (for a,x,y st a<>0.L holds a*x=a*y implies x=y)
& (for a,x,y st a<>0.L holds x*a=y*a implies x=y)
& (for a holds a*0.L = 0.L)
& (for a holds 0.L*a = 0.L)
& (for a,b,c holds a*(b+c) = a*b + a*c);

canceled;

theorem :: ALGSTR_2:14
for G being Abelian right-distributive doubleLoop,
a,b being Element of G holds a*(-b) = -(a*b);

theorem :: ALGSTR_2:15
(non empty LoopStr),
a being Element of G holds -(-a) = a;

theorem :: ALGSTR_2:16
for G being Abelian right-distributive doubleLoop holds
(-1_ G)*(-1_ G) = 1_ G;

theorem :: ALGSTR_2:17
for G being Abelian right-distributive doubleLoop,
a,x,y being Element of G holds
a*(x-y) = a*x - a*y;

:: 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 Abelian add-associative left-distributive
non degenerated doubleLoop;
end;

canceled;

theorem :: ALGSTR_2:19
L is rightQuasi-Field iff
(for a holds a + 0.L = a)
& (for a ex x st a+x = 0.L)
& (for a,b,c holds (a+b)+c = a+(b+c))
& (for a,b holds a+b = b+a)
& 0.L <> 1_ L
& (for a holds a * 1_ L = a)
& (for a holds 1_ L * a = a)
& (for a,b st a<>0.L ex x st a*x=b)
& (for a,b st a<>0.L ex x st x*a=b)
& (for a,x,y st a<>0.L holds a*x=a*y implies x=y)
& (for a,x,y st a<>0.L holds x*a=y*a implies x=y)
& (for a holds a*0.L = 0.L)
& (for a holds 0.L*a = 0.L)
& (for a,b,c holds (b+c)*a = b*a + c*a);

:: Below, the three features concerned with the - function,
:: numbered 20..22 are proved. Where necessary, a few additional
:: facts are included. They are independent of the similar proofs
:: performed for the left quasi-field.

reserve G for left-distributive doubleLoop,
a,b,x,y for Element of G;

canceled;

theorem :: ALGSTR_2:21
(-b)*a = -(b*a);

canceled;

theorem :: ALGSTR_2:23
for G being Abelian left-distributive doubleLoop holds
(-1_ G)*(-1_ G) = 1_ G;

theorem :: ALGSTR_2:24
(x-y)*a = x*a - y*a;

:: 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 Abelian add-associative distributive
non degenerated doubleLoop;
end;

reserve a,b,c,x,y,z for Element of L;

canceled;

theorem :: ALGSTR_2:26
L is doublesidedQuasi-Field iff
(for a holds a + 0.L = a)
& (for a ex x st a+x = 0.L)
& (for a,b,c holds (a+b)+c = a+(b+c))
& (for a,b holds a+b = b+a)
& 0.L <> 1_ L
& (for a holds a * 1_ L = a)
& (for a holds 1_ L * a = a)
& (for a,b st a<>0.L ex x st a*x=b)
& (for a,b st a<>0.L ex x st x*a=b)
& (for a,x,y st a<>0.L holds a*x=a*y implies x=y)
& (for a,x,y st a<>0.L holds x*a=y*a implies x=y)
& (for a holds a*0.L = 0.L)
& (for a holds 0.L*a = 0.L)
& (for a,b,c holds a*(b+c) = a*b + a*c)
& (for a,b,c holds (b+c)*a = b*a + c*a);

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

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

canceled 5;

theorem :: ALGSTR_2:32
L is _Skew-Field iff
(for a holds a + 0.L = a)
& (for a ex x st a+x = 0.L)
& (for a,b,c holds (a+b)+c = a+(b+c))
& (for a,b holds a+b = b+a)
& 0.L <> 1_ L
& (for a holds a * 1_ L = a)
& (for a st a<>0.L ex x st a*x = 1_ L)
& (for a holds a*0.L = 0.L)
& (for a holds 0.L*a = 0.L)
& (for a,b,c holds (a*b)*c = a*(b*c))
& (for a,b,c holds a*(b+c) = a*b + a*c)
& (for a,b,c holds (b+c)*a = b*a + c*a);

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

canceled;

theorem :: ALGSTR_2:34
L is _Field iff
(for a holds a + 0.L = a)
& (for a ex x st a+x = 0.L)
& (for a,b,c holds (a+b)+c = a+(b+c))
& (for a,b holds a+b = b+a)
& 0.L <> 1_ L
& (for a holds a * 1_ L = a)
& (for a st a<>0.L ex x st a*x = 1_ L)
& (for a holds a*0.L = 0.L)
& (for a,b,c holds (a*b)*c = a*(b*c))
& (for a,b,c holds a*(b+c) = a*b + a*c)
& (for a,b holds a*b = b*a);
```