:: From Loops to Abelian Multiplicative Groups with Zero
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received July 10, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: ALGSTR_1:1
for L being non empty addLoopStr
for a, b being Element of L st ( 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) ) & a + b = 0. L holds
b + a = 0. L
proofend;

theorem :: ALGSTR_1:2
for L being non empty addLoopStr
for a being Element of L st ( 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) ) holds
(0. L) + a = a + (0. L)
proofend;

theorem :: ALGSTR_1:3
for L being non empty addLoopStr st ( 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) ) holds
for a being Element of L ex x being Element of L st x + a = 0. L
proofend;

definition
let x be set ;
func Extract x ->  Element of {x} equals :: ALGSTR_1:def 1
x;
coherence
 x is Element of {x} by TARSKI:def_1;
end;

:: deftheorem  defines Extract ALGSTR_1:def_1_:_
 for x being set holds Extract x = x;

theorem Th4: :: ALGSTR_1:4
for a, b being Element of Trivial-addLoopStr holds a = b
proofend;

theorem :: ALGSTR_1:5
for a, b being Element of Trivial-addLoopStr holds a + b = 0. Trivial-addLoopStr by Th4;

Lm1:  ( ( for a being Element of Trivial-addLoopStr holds a + (0. Trivial-addLoopStr) = a ) & ( for a being Element of Trivial-addLoopStr holds (0. Trivial-addLoopStr) + a = a ) )
by Th4;

Lm2:  for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st a + x = b
proofend;

Lm3:  for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st x + a = b
proofend;

Lm4:  ( ( for a, x, y being Element of Trivial-addLoopStr st a + x = a + y holds
x = y ) & ( for a, x, y being Element of Trivial-addLoopStr st x + a = y + a holds
x = y ) )
by Th4;

definition
let IT be non empty addLoopStr ;
attrIT is left_zeroed  means :Def2: :: ALGSTR_1:def 2
 for a being Element of IT holds (0. IT) + a = a;
end;

:: deftheorem Def2 defines left_zeroed ALGSTR_1:def_2_:_
 for IT being non empty addLoopStr holds
( IT is left_zeroed iff for a being Element of IT holds (0. IT) + a = a );

definition
let L be non empty addLoopStr ;
attrL is add-left-invertible  means :Def3: :: ALGSTR_1:def 3
 for a, b being Element of L ex x being Element of L st x + a = b;
attrL is add-right-invertible  means :Def4: :: ALGSTR_1:def 4
 for a, b being Element of L ex x being Element of L st a + x = b;
end;

:: deftheorem Def3 defines add-left-invertible ALGSTR_1:def_3_:_
 for L being non empty addLoopStr holds
( L is add-left-invertible iff for a, b being Element of L ex x being Element of L st x + a = b );

:: deftheorem Def4 defines add-right-invertible ALGSTR_1:def_4_:_
 for L being non empty addLoopStr holds
( L is add-right-invertible iff for a, b being Element of L ex x being Element of L st a + x = b );

definition
let IT be non empty addLoopStr ;
attrIT is Loop-like  means :Def5: :: ALGSTR_1:def 5
( IT is left_add-cancelable & IT is right_add-cancelable & IT is add-left-invertible & IT is add-right-invertible );
end;

:: deftheorem Def5 defines Loop-like ALGSTR_1:def_5_:_
 for IT being non empty addLoopStr holds
( IT is Loop-like iff ( IT is left_add-cancelable & IT is right_add-cancelable & IT is add-left-invertible & IT is add-right-invertible ) );

registration
cluster non empty Loop-like  ->  non empty left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is Loop-like holds
( b1 is left_add-cancelable & b1 is right_add-cancelable & b1 is add-left-invertible & b1 is add-right-invertible ) by Def5;
cluster non empty left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible  ->  non empty Loop-like for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is left_add-cancelable & b1 is right_add-cancelable & b1 is add-left-invertible & b1 is add-right-invertible holds
b1 is Loop-like by Def5;
end;

theorem Th6: :: ALGSTR_1:6
for L being non empty addLoopStr holds
( L is Loop-like iff ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( for a, b being Element of L ex x being Element of L st x + a = b ) & ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) ) )
proofend;

Lm5:  for a, b, c being Element of Trivial-addLoopStr holds (a + b) + c = a + (b + c)
by Th4;

Lm6:  for a, b being Element of Trivial-addLoopStr holds a + b = b + a
by Th4;

registration
cluster Trivial-addLoopStr  ->  add-associative right_zeroed left_zeroed Loop-like ;
coherence
 ( Trivial-addLoopStr is add-associative & Trivial-addLoopStr is Loop-like & Trivial-addLoopStr is right_zeroed & Trivial-addLoopStr is left_zeroed ) by Def2, Lm1, Lm2, Lm3, Lm4, Lm5, Th6, RLVECT_1:def_3, RLVECT_1:def_4;
end;

registration
cluster non empty strict right_zeroed left_zeroed Loop-like for addLoopStr ;
existence
 ex b1 being non empty addLoopStr st
( b1 is strict & b1 is left_zeroed & b1 is right_zeroed & b1 is Loop-like )
proofend;
end;

definition
mode Loop is non empty right_zeroed left_zeroed Loop-like addLoopStr ;
end;

registration
cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for addLoopStr ;
existence
 ex b1 being Loop st
( b1 is strict & b1 is add-associative )
proofend;
end;

registration
cluster non empty Loop-like  ->  non empty add-left-invertible for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is Loop-like holds
b1 is add-left-invertible ;
cluster non empty right_complementable add-associative right_zeroed  ->  non empty left_zeroed Loop-like for addLoopStr ;
coherence
 for b1 being non empty addLoopStr st b1 is add-associative & b1 is right_zeroed & b1 is right_complementable holds
( b1 is left_zeroed & b1 is Loop-like )
proofend;
end;

theorem Th7: :: ALGSTR_1:7
for L being non empty addLoopStr holds
( L is AddGroup 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) ) ) )
proofend;

registration
cluster Trivial-addLoopStr  ->  Abelian ;
coherence
 Trivial-addLoopStr is Abelian by Lm6, RLVECT_1:def_2;
end;

registration
cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for addLoopStr ;
existence
 ex b1 being AddGroup st
( b1 is strict & b1 is Abelian )
proofend;
end;

theorem :: ALGSTR_1:8
for L being non empty addLoopStr holds
( L is Abelian AddGroup 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 ) ) ) by Th7, RLVECT_1:def_2;

registration
cluster Trivial-multLoopStr  ->  non empty ;
coherence
 not Trivial-multLoopStr is empty ;
end;

theorem Th9: :: ALGSTR_1:9
for a, b being Element of Trivial-multLoopStr holds a = b
proofend;

theorem :: ALGSTR_1:10
for a, b being Element of Trivial-multLoopStr holds a * b = 1. Trivial-multLoopStr by Th9;

Lm7:  ( ( for a being Element of Trivial-multLoopStr holds a * (1. Trivial-multLoopStr) = a ) & ( for a being Element of Trivial-multLoopStr holds (1. Trivial-multLoopStr) * a = a ) )
by Th9;

Lm8:  for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st a * x = b
proofend;

Lm9:  for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st x * a = b
proofend;

definition
let IT be non empty multLoopStr ;
attrIT is invertible  means :Def6: :: ALGSTR_1:def 6
( ( for a, b being Element of IT ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT ex x being Element of IT st x * a = b ) );
end;

:: deftheorem Def6 defines invertible ALGSTR_1:def_6_:_
 for IT being non empty multLoopStr holds
( IT is invertible iff ( ( for a, b being Element of IT ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT ex x being Element of IT st x * a = b ) ) );

notation
let L be non empty multLoopStr ;
synonym  cancelable L for  mult-cancelable ;
end;

registration
cluster non empty cancelable strict well-unital invertible for multLoopStr ;
existence
 ex b1 being non empty multLoopStr st
( b1 is strict & b1 is well-unital & b1 is invertible & b1 is cancelable )
proofend;
end;

definition
mode multLoop is non empty cancelable well-unital invertible multLoopStr ;
end;

registration
cluster Trivial-multLoopStr  ->  cancelable well-unital invertible ;
coherence
 ( Trivial-multLoopStr is well-unital & Trivial-multLoopStr is invertible & Trivial-multLoopStr is cancelable ) by Def6, Lm7, Lm8, Lm9, VECTSP_1:def_6;
end;

Lm10:  for a, b, c being Element of Trivial-multLoopStr holds (a * b) * c = a * (b * c)
by Th9;

registration
cluster non empty left_mult-cancelable right_mult-cancelable cancelable strict unital associative right_unital well-unital left_unital invertible for multLoopStr ;
existence
 ex b1 being multLoop st
( b1 is strict & b1 is associative )
proofend;
end;

definition
mode multGroup is associative multLoop;
end;

Lm11:  for L being non empty multLoopStr
for a, b being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L 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) ) & a * b = 1. L holds
b * a = 1. L
proofend;

Lm12:  for L being non empty multLoopStr
for a being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L 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) ) holds
(1. L) * a = a * (1. L)
proofend;

Lm13:  for L being non empty multLoopStr st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L 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) ) holds
for a being Element of L ex x being Element of L st x * a = 1. L
proofend;

theorem Th11: :: ALGSTR_1:11
for L being non empty multLoopStr holds
( L is multGroup iff ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L 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) ) ) )
proofend;

registration
cluster Trivial-multLoopStr  ->  associative ;
coherence
 Trivial-multLoopStr is associative by Lm10, GROUP_1:def_3;
end;

Lm14:  for a, b being Element of Trivial-multLoopStr holds a * b = b * a
by Th9;

registration
cluster non empty left_mult-cancelable right_mult-cancelable cancelable strict unital associative commutative right_unital well-unital left_unital invertible for multLoopStr ;
existence
 ex b1 being multGroup st
( b1 is strict & b1 is commutative )
proofend;
end;

theorem :: ALGSTR_1:12
for L being non empty multLoopStr holds
( L is commutative multGroup iff ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L 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, b being Element of L holds a * b = b * a ) ) ) by Th11, GROUP_1:def_12;

notation
let L be non empty cancelable invertible multLoopStr ;
let x be Element of L;
synonym x " for  / x;
end;

registration
let L be non empty cancelable invertible multLoopStr ;
cluster  ->  left_invertible for Element of the carrier of L;
coherence
 for b1 being Element of L holds b1 is left_invertible
proofend;
end;

theorem :: ALGSTR_1:13
for G being multGroup
for a being Element of G holds
( (a ") * a = 1. G & a * (a ") = 1. G )
proofend;

definition
let L be non empty cancelable invertible multLoopStr ;
let a, b be Element of L;
funca / b ->  Element of L equals :: ALGSTR_1:def 7
a * (b ");
correctness
coherence
a * (b ") is Element of L;
;
end;

:: deftheorem  defines / ALGSTR_1:def_7_:_
 for L being non empty cancelable invertible multLoopStr
for a, b being Element of L holds a / b = a * (b ");

definition
func multEX_0  ->  strict multLoopStr_0  equals :: ALGSTR_1:def 8
 multLoopStr_0(# REAL,multreal,0,1 #);
correctness
coherence
multLoopStr_0(# REAL,multreal,0,1 #) is strict multLoopStr_0 ;
;
end;

:: deftheorem  defines multEX_0 ALGSTR_1:def_8_:_
 multEX_0 = multLoopStr_0(# REAL,multreal,0,1 #);

registration
cluster multEX_0  ->  non empty strict ;
coherence
 not multEX_0 is empty ;
end;

Lm15: now__::_thesis:_for_x,_e_being_Element_of_multEX_0_st_e_=_1_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let x, e be Element of multEX_0; ::_thesis: ( e = 1 implies ( x * e = x & e * x = x ) )
reconsider a = x as Real ;
assume A1: e = 1 ; ::_thesis: ( x * e = x & e * x = x )
hence x * e = a * 1 by BINOP_2:def_11
.= x ;
::_thesis: e * x = x
thus e * x = 1 * a by A1, BINOP_2:def_11
.= x ; ::_thesis: verum
end;

registration
cluster multEX_0  ->  strict well-unital ;
coherence
 multEX_0 is well-unital
proofend;
end;

Lm16:  0 = 0. multEX_0
;

Lm17:  1 = 1_ multEX_0
;

theorem Th14: :: ALGSTR_1:14
for q, p being Real st q <> 0 holds
ex y being Real st p = q * y
proofend;

theorem Th15: :: ALGSTR_1:15
for q, p being Real st q <> 0 holds
ex y being Real st p = y * q
proofend;

Lm18:  for a, b being Element of multEX_0 st a <> 0. multEX_0 holds
ex x being Element of multEX_0 st a * x = b
proofend;

Lm19:  for a, b being Element of multEX_0 st a <> 0. multEX_0 holds
ex x being Element of multEX_0 st x * a = b
proofend;

Lm20:  for a, x, y being Element of multEX_0 st a <> 0. multEX_0 &amp; a * x = a * y holds
x = y
proofend;

Lm21:  for a, x, y being Element of multEX_0 st a <> 0. multEX_0 &amp; x * a = y * a holds
x = y
proofend;

Lm22:  for a being Element of multEX_0 holds a * (0. multEX_0) = 0. multEX_0
proofend;

Lm23:  for a being Element of multEX_0 holds (0. multEX_0) * a = 0. multEX_0
proofend;

definition
let IT be non empty multLoopStr_0 ;
attrIT is almost_invertible  means :Def9: :: ALGSTR_1:def 9
( ( for a, b being Element of IT st a <> 0. IT holds
ex x being Element of IT st a * x = b ) &amp; ( for a, b being Element of IT st a <> 0. IT holds
ex x being Element of IT st x * a = b ) );
end;

:: deftheorem Def9 defines almost_invertible ALGSTR_1:def_9_:_
 for IT being non empty multLoopStr_0 holds
( IT is almost_invertible iff ( ( for a, b being Element of IT st a <> 0. IT holds
ex x being Element of IT st a * x = b ) &amp; ( for a, b being Element of IT st a <> 0. IT holds
ex x being Element of IT st x * a = b ) ) );

definition
let IT be non empty multLoopStr_0 ;
attrIT is multLoop_0-like  means :Def10: :: ALGSTR_1:def 10
( IT is almost_invertible &amp; IT is almost_cancelable &amp; ( for a being Element of IT holds a * (0. IT) = 0. IT ) &amp; ( for a being Element of IT holds (0. IT) * a = 0. IT ) );
end;

:: deftheorem Def10 defines multLoop_0-like ALGSTR_1:def_10_:_
 for IT being non empty multLoopStr_0 holds
( IT is multLoop_0-like iff ( IT is almost_invertible &amp; IT is almost_cancelable &amp; ( for a being Element of IT holds a * (0. IT) = 0. IT ) &amp; ( for a being Element of IT holds (0. IT) * a = 0. IT ) ) );

theorem Th16: :: ALGSTR_1:16
for L being non empty multLoopStr_0 holds
( L is multLoop_0-like iff ( ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) &amp; ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) &amp; ( for a, x, y being Element of L st a <> 0. L &amp; a * x = a * y holds
x = y ) &amp; ( for a, x, y being Element of L st a <> 0. L &amp; x * a = y * a holds
x = y ) &amp; ( for a being Element of L holds a * (0. L) = 0. L ) &amp; ( for a being Element of L holds (0. L) * a = 0. L ) ) )
proofend;

registration
cluster non empty multLoop_0-like  ->  non empty almost_cancelable almost_invertible for multLoopStr_0 ;
coherence
 for b1 being non empty multLoopStr_0 st b1 is multLoop_0-like holds
( b1 is almost_invertible &amp; b1 is almost_cancelable ) by Def10;
end;

registration
cluster non empty non degenerated strict well-unital multLoop_0-like for multLoopStr_0 ;
existence
 ex b1 being non empty multLoopStr_0 st
( b1 is strict &amp; b1 is well-unital &amp; b1 is multLoop_0-like &amp; not b1 is degenerated )
proofend;
end;

definition
mode multLoop_0 is non empty non degenerated well-unital multLoop_0-like multLoopStr_0 ;
end;

registration
cluster multEX_0  ->  strict well-unital multLoop_0-like ;
coherence
 ( multEX_0 is well-unital &amp; multEX_0 is multLoop_0-like ) by Lm18, Lm19, Lm20, Lm21, Lm22, Lm23, Th16;
end;

Lm24:  for a, b, c being Element of multEX_0 holds (a * b) * c = a * (b * c)
proofend;

registration
cluster non empty non degenerated non trivial strict almost_left_cancelable almost_right_cancelable almost_cancelable unital associative right_unital well-unital left_unital almost_invertible multLoop_0-like for multLoopStr_0 ;
existence
 ex b1 being multLoop_0 st
( b1 is strict &amp; b1 is associative &amp; not b1 is degenerated )
proofend;
end;

definition
mode multGroup_0 is associative multLoop_0;
end;

registration
cluster multEX_0  ->  strict associative ;
coherence
 multEX_0 is associative by Lm24, GROUP_1:def_3;
end;

Lm25:  for a, b being Element of multEX_0 holds a * b = b * a
proofend;

registration
cluster non empty non degenerated non trivial strict almost_left_cancelable almost_right_cancelable almost_cancelable unital associative commutative right_unital well-unital left_unital almost_invertible multLoop_0-like for multLoopStr_0 ;
existence
 ex b1 being multGroup_0 st
( b1 is strict &amp; b1 is commutative )
proofend;
end;

definition
let L be non empty almost_cancelable almost_invertible multLoopStr_0 ;
let x be Element of L;
assume A1: x <> 0. L ;
redefine func x "  means :Def11: :: ALGSTR_1:def 11
it * x = 1. L;
compatibility
 for b1 being Element of the carrier of L holds
( b1 = x " iff b1 * x = 1. L )
proofend;
end;

:: deftheorem Def11 defines " ALGSTR_1:def_11_:_
 for L being non empty almost_cancelable almost_invertible multLoopStr_0
for x being Element of L st x <> 0. L holds
for b3 being Element of the carrier of L holds
( b3 = x " iff b3 * x = 1. L );

theorem :: ALGSTR_1:17
for G being non empty almost_cancelable associative well-unital almost_invertible multLoopStr_0
for a being Element of G st a <> 0. G holds
( (a ") * a = 1. G &amp; a * (a ") = 1. G )
proofend;

definition
let L be non empty almost_cancelable almost_invertible multLoopStr_0 ;
let a, b be Element of L;
funca / b ->  Element of L equals :: ALGSTR_1:def 12
a * (b ");
correctness
coherence
a * (b ") is Element of L;
;
end;

:: deftheorem  defines / ALGSTR_1:def_12_:_
 for L being non empty almost_cancelable almost_invertible multLoopStr_0
for a, b being Element of L holds a / b = a * (b ");

:: from SCMRING1, 2010,02.06, A.T.
registration
cluster1 -element  -> 1 -element right_complementable Abelian add-associative right_zeroed for addLoopStr ;
coherence
 for b1 being 1 -element addLoopStr holds
( b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable )
proofend;
cluster non empty trivial  ->  non empty right-distributive well-unital for doubleLoopStr ;
coherence
 for b1 being non empty doubleLoopStr st b1 is trivial holds
( b1 is well-unital &amp; b1 is right-distributive )
proofend;
end;

registration
cluster1 -element  -> 1 -element Group-like associative commutative for multMagma ;
coherence
 for b1 being 1 -element multMagma holds
( b1 is Group-like &amp; b1 is associative &amp; b1 is commutative )
proofend;
end;