:: From Double Loops to Fields
:: by Wojciech Skaba and Micha{\l} Muzalewski
::
:: Received September 27, 1990
:: Copyright (c) 1990-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ALGSTR_0, CARD_1, SUPINF_2, VECTSP_1, SUBSET_1,
RELAT_1, ALGSTR_1, ARYTM_1, ARYTM_3, STRUCT_0, RLVECT_1, BINOP_1,
LATTICES, MESFUNC1, GROUP_1, ALGSTR_2, NUMBERS;
notations SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, REAL_1, STRUCT_0, ALGSTR_0,
RLVECT_1, GROUP_1, VECTSP_1, ALGSTR_1;
constructors BINOP_2, ALGSTR_1, RLVECT_1, VECTSP_1, MEMBERED, REAL_1,
XXREAL_0, NUMBERS, GROUP_1;
registrations VECTSP_1, ALGSTR_1, ALGSTR_0, MEMBERED, XREAL_0;
requirements SUBSET;
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.
registration
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 L be left_add-cancelable add-right-invertible non empty addLoopStr;
let a be Element of L;
func -a -> Element of L means
:: ALGSTR_2:def 1
a+it = 0.L;
end;
definition
let L be left_add-cancelable add-right-invertible non empty addLoopStr;
let a,b be Element of L;
func a-b -> Element of L equals
:: ALGSTR_2:def 2
a+ -b;
end;
registration
cluster strict Abelian add-associative commutative associative distributive
non degenerated left_zeroed right_zeroed Loop-like well-unital multLoop_0-like
for non empty doubleLoopStr;
end;
definition
mode doubleLoop is left_zeroed right_zeroed Loop-like well-unital
multLoop_0-like non empty doubleLoopStr;
end;
definition
mode leftQuasi-Field is Abelian add-associative 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.
theorem :: ALGSTR_2:1
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;
theorem :: ALGSTR_2:2
for G being Abelian right-distributive doubleLoop, a,b being
Element of G holds a*(-b) = -(a*b);
theorem :: ALGSTR_2:3
for G being Abelian left_add-cancelable add-right-invertible
non empty addLoopStr, a being Element of G holds -(-a) = a;
theorem :: ALGSTR_2:4
for G being Abelian right-distributive doubleLoop holds (-1.G)*(-1.G) = 1.G;
theorem :: ALGSTR_2:5
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;
theorem :: ALGSTR_2:6
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;
theorem :: ALGSTR_2:7
(-b)*a = -(b*a);
theorem :: ALGSTR_2:8
for G being Abelian left-distributive doubleLoop holds (-1.G)*(-1.G) = 1.G;
theorem :: ALGSTR_2:9
(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;
theorem :: ALGSTR_2:10
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.
theorem :: ALGSTR_2:11
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;
theorem :: ALGSTR_2:12
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;