:: From Double Loops to Fields :: by Wojciech Skaba and Micha{\l} Muzalewski :: :: Received September 27, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin 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 proofend; 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 proofend; 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 b1 being Element of L st a + b1 = 0. L by ALGSTR_1:def_4; uniqueness for b1, b2 being Element of L st a + b1 = 0. L & a + b2 = 0. L holds b1 = b2 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, b3 being Element of L holds ( b3 = - a iff a + b3 = 0. L ); definition let L be non empty left_add-cancelable add-right-invertible addLoopStr ; let a, b be Element of L; funca - 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 associative commutative well-unital distributive for doubleLoopStr ; existence ex b1 being non empty doubleLoopStr st ( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is commutative & b1 is associative & b1 is distributive & not b1 is degenerated & b1 is left_zeroed & b1 is right_zeroed & b1 is Loop-like & b1 is well-unital & b1 is multLoop_0-like ) proofend; 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) ) ) ) proofend; theorem Th2: :: ALGSTR_2:2 for G being Abelian right-distributive doubleLoop for a, b being Element of G holds a * (- b) = - (a * b) proofend; 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 proofend; theorem :: ALGSTR_2:4 for G being Abelian right-distributive doubleLoop holds (- (1. G)) * (- (1. G)) = 1. G proofend; 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) proofend; :: 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) ) ) ) proofend; theorem Th7: :: ALGSTR_2:7 for G being left-distributive doubleLoop for b, a being Element of G holds (- b) * a = - (b * a) proofend; theorem :: ALGSTR_2:8 for G being Abelian left-distributive doubleLoop holds (- (1. G)) * (- (1. G)) = 1. G proofend; theorem :: ALGSTR_2:9 for G being left-distributive doubleLoop for x, y, a being Element of G holds (x - y) * a = (x * a) - (y * a) proofend; :: 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) ) ) ) proofend; :: 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 proofend; 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) proofend; 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 proofend; :: 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) ) ) ) proofend; :: 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 ) ) ) proofend;