:: From Double Loops to Fields :: by Wojciech Skaba and Micha{\l} Muzalewski :: :: Received September 27, 1990 :: Copyright (c) 1990-2021 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;