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

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
proof end;

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)
proof end;

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
proof end;

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
proof end;

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 + = a ) & ( for a being Element of Trivial-addLoopStr holds + a = a ) )
by Th4;

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

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

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 ;
attr IT is left_zeroed means :: ALGSTR_1:def 2
for a being Element of IT holds (0. IT) + a = a;
end;

:: deftheorem 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 ;
attr L 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;
attr L 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 ;
attr IT is Loop-like means :: ALGSTR_1:def 5
end;

:: deftheorem 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
coherence
for b1 being non empty addLoopStr st b1 is Loop-like holds
;
coherence
b1 is Loop-like
;
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 ) ) )
proof end;

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
coherence by Lm1, Lm2, Lm3, Lm4, Lm5, Th6;
end;

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

definition end;

registration
existence
ex b1 being Loop st
( b1 is strict & b1 is add-associative )
proof end;
end;

registration
coherence
for b1 being non empty addLoopStr st b1 is Loop-like holds
;
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 )
proof end;
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) ) ) )
proof end;

registration
coherence by Lm6;
end;

registration
existence
( b1 is strict & b1 is Abelian )
proof end;
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 ;

registration
coherence ;
end;

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

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 * = a ) & ( for a being Element of Trivial-multLoopStr holds * a = a ) )
by Th9;

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

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

definition
let IT be non empty multLoopStr ;
attr IT 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
existence
ex b1 being non empty multLoopStr st
( b1 is strict & b1 is well-unital & b1 is invertible & b1 is cancelable )
proof end;
end;

definition end;

registration
coherence by ;
end;

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

registration
existence
ex b1 being multLoop st
( b1 is strict & b1 is associative )
proof end;
end;

definition 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

proof end;

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)

proof end;

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

proof end;

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) ) ) )
proof end;

registration
coherence by Lm10;
end;

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

registration
existence
ex b1 being multGroup st
( b1 is strict & b1 is commutative )
proof end;
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 ;

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
by Def6;
end;

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

canceled;

:: definition
:: let L be invertible cancelable non empty multLoopStr;
:: let a, b be Element of L;
:: func a/b -> Element of L equals
:: a*(b");
:: correctness;
:: end;
::$CD definition func multEX_0 -> strict multLoopStr_0 equals :: ALGSTR_1:def 7 multLoopStr_0(# REAL,multreal,(In (0,REAL)),(In (1,REAL)) #); correctness coherence multLoopStr_0(# REAL,multreal,(In (0,REAL)),(In (1,REAL)) #) is strict multLoopStr_0 ; ; end; :: deftheorem defines multEX_0 ALGSTR_1:def 7 : multEX_0 = multLoopStr_0(# REAL,multreal,(In (0,REAL)),(In (1,REAL)) #); registration 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 .= x ; :: thesis: verum end; registration coherence by Lm15; end; Lm16: 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 proof end; Lm17: 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 proof end; Lm18: for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & a * x = a * y holds x = y proof end; Lm19: for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & x * a = y * a holds x = y proof end; Lm20: for a being Element of multEX_0 holds a * () = 0. multEX_0 proof end; Lm21: for a being Element of multEX_0 holds () * a = 0. multEX_0 proof end; definition let IT be non empty multLoopStr_0 ; attr IT is almost_invertible means :Def8: :: ALGSTR_1:def 8 ( ( for a, b being Element of IT st a <> 0. IT holds ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT st a <> 0. IT holds ex x being Element of IT st x * a = b ) ); end; :: deftheorem Def8 defines almost_invertible ALGSTR_1:def 8 : 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 ) & ( 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 ; attr IT is multLoop_0-like means :: ALGSTR_1:def 9 ( IT is almost_invertible & IT is almost_cancelable & ( for a being Element of IT holds a * (0. IT) = 0. IT ) & ( for a being Element of IT holds (0. IT) * a = 0. IT ) ); end; :: deftheorem defines multLoop_0-like ALGSTR_1:def 9 : for IT being non empty multLoopStr_0 holds ( IT is multLoop_0-like iff ( IT is almost_invertible & IT is almost_cancelable & ( for a being Element of IT holds a * (0. IT) = 0. IT ) & ( for a being Element of IT holds (0. IT) * a = 0. IT ) ) ); theorem :: ALGSTR_1:14 canceled; theorem :: ALGSTR_1:15 canceled; ::$CT 2
theorem Th14: :: 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 ) & ( 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 ) ) )
proof end;

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

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

definition end;

registration
coherence by ;
end;

Lm22: for a, b, c being Element of multEX_0 holds (a * b) * c = a * (b * c)
proof end;

registration
existence
ex b1 being multLoop_0 st
( b1 is strict & b1 is associative & not b1 is degenerated )
proof end;
end;

definition end;

registration
coherence by Lm22;
end;

Lm23: for a, b being Element of multEX_0 holds a * b = b * a
proof end;

registration
existence
ex b1 being multGroup_0 st
( b1 is strict & b1 is commutative )
proof end;
end;

notation
let L be non empty almost_cancelable almost_invertible multLoopStr_0 ;
let x be Element of L;
synonym x " for / x;
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 :Def10: :: ALGSTR_1:def 10
it * x = 1. L;
compatibility
for b1 being Element of the carrier of L holds
( b1 = x " iff b1 * x = 1. L )
proof end;
end;

:: deftheorem Def10 defines " ALGSTR_1:def 10 :
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 well-unital associative almost_invertible multLoopStr_0
for a being Element of G st a <> 0. G holds
( (a ") * a = 1. G & a * (a ") = 1. G )
proof end;

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

:: deftheorem defines / ALGSTR_1:def 11 :
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
coherence
for b1 being 1 -element addLoopStr holds
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable )
proof end;
coherence
for b1 being non empty doubleLoopStr st b1 is trivial holds
( b1 is well-unital & b1 is right-distributive )
;
end;

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