:: From Loops to Abelian Multiplicative Groups with Zero
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received July 10, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: ALGSTR_1:1
theorem :: ALGSTR_1:2
theorem :: ALGSTR_1:3
:: deftheorem ALGSTR_1:def 1 :
canceled;
:: deftheorem ALGSTR_1:def 2 :
canceled;
:: deftheorem defines Extract ALGSTR_1:def 3 :
theorem :: ALGSTR_1:4
canceled;
theorem Th5: :: ALGSTR_1:5
theorem :: ALGSTR_1:6
Lm1:
for a being Element of Trivial-addLoopStr holds a + (0. Trivial-addLoopStr ) = a
by Th5;
Lm2:
for a being Element of Trivial-addLoopStr holds (0. Trivial-addLoopStr ) + a = a
by Th5;
Lm3:
for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st a + x = b
Lm4:
for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st x + a = b
Lm5:
for a, x, y being Element of Trivial-addLoopStr st a + x = a + y holds
x = y
by Th5;
Lm6:
for a, x, y being Element of Trivial-addLoopStr st x + a = y + a holds
x = y
by Th5;
:: deftheorem ALGSTR_1:def 4 :
canceled;
:: deftheorem Def5 defines left_zeroed ALGSTR_1:def 5 :
:: deftheorem ALGSTR_1:def 6 :
canceled;
:: deftheorem ALGSTR_1:def 7 :
canceled;
:: deftheorem Def8 defines add-left-invertible ALGSTR_1:def 8 :
:: deftheorem Def9 defines add-right-invertible ALGSTR_1:def 9 :
:: deftheorem ALGSTR_1:def 10 :
canceled;
:: deftheorem ALGSTR_1:def 11 :
canceled;
:: deftheorem Def12 defines Loop-like ALGSTR_1:def 12 :
Lm7:
for L being addLoopStr st L is left_add-cancelable holds
for x, y, z being Element of L st x + y = x + z holds
y = z
by ALGSTR_0:def 3;
Lm8:
for L being addLoopStr st L is right_add-cancelable holds
for x, y, z being Element of L st y + x = z + x holds
y = z
by ALGSTR_0:def 4;
theorem Th7: :: ALGSTR_1:7
Lm9:
for a, b, c being Element of Trivial-addLoopStr holds (a + b) + c = a + (b + c)
by Th5;
Lm10:
for a, b being Element of Trivial-addLoopStr holds a + b = b + a
by Th5;
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 Def5, Lm1, Lm2, Lm3, Lm4, Lm5, Lm6, Lm9, Th7, RLVECT_1:def 6, RLVECT_1:def 7;
end;
theorem :: ALGSTR_1:8
canceled;
theorem Th9: :: ALGSTR_1:9
theorem :: ALGSTR_1:10
canceled;
theorem :: ALGSTR_1:11
theorem :: ALGSTR_1:12
canceled;
theorem :: ALGSTR_1:13
canceled;
theorem :: ALGSTR_1:14
canceled;
theorem :: ALGSTR_1:15
canceled;
theorem :: ALGSTR_1:16
canceled;
theorem :: ALGSTR_1:17
canceled;
theorem Th18: :: ALGSTR_1:18
theorem :: ALGSTR_1:19
Lm11:
for a being Element of Trivial-multLoopStr holds a * (1. Trivial-multLoopStr ) = a
by Th18;
Lm12:
for a being Element of Trivial-multLoopStr holds (1. Trivial-multLoopStr ) * a = a
by Th18;
Lm13:
for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st a * x = b
Lm14:
for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st x * a = b
:: deftheorem ALGSTR_1:def 13 :
canceled;
:: deftheorem Def14 defines invertible ALGSTR_1:def 14 :
:: deftheorem ALGSTR_1:def 15 :
canceled;
Lm15:
for a, b, c being Element of Trivial-multLoopStr holds (a * b) * c = a * (b * c)
by Th18;
Lm16:
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
Lm17:
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)
Lm18:
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
theorem :: ALGSTR_1:20
canceled;
theorem :: ALGSTR_1:21
canceled;
theorem Th22: :: ALGSTR_1:22
Lm19:
for a, b being Element of Trivial-multLoopStr holds a * b = b * a
by Th18;
theorem :: ALGSTR_1:23
canceled;
theorem :: ALGSTR_1:24
theorem :: ALGSTR_1:25
canceled;
theorem :: ALGSTR_1:26
:: deftheorem ALGSTR_1:def 16 :
canceled;
:: deftheorem ALGSTR_1:def 17 :
canceled;
:: deftheorem ALGSTR_1:def 18 :
canceled;
:: deftheorem defines / ALGSTR_1:def 19 :
:: deftheorem ALGSTR_1:def 20 :
canceled;
:: deftheorem ALGSTR_1:def 21 :
canceled;
:: deftheorem ALGSTR_1:def 22 :
canceled;
:: deftheorem defines multEX_0 ALGSTR_1:def 23 :
Lm21:
0 = 0. multEX_0
;
Lm22:
1 = 1_ multEX_0
;
theorem :: ALGSTR_1:27
canceled;
theorem :: ALGSTR_1:28
canceled;
theorem :: ALGSTR_1:29
canceled;
theorem :: ALGSTR_1:30
canceled;
theorem :: ALGSTR_1:31
canceled;
theorem Th32: :: ALGSTR_1:32
theorem Th33: :: ALGSTR_1:33
Lm23:
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
Lm24:
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
Lm25:
for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & a * x = a * y holds
x = y
Lm26:
for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & x * a = y * a holds
x = y
Lm27:
for a being Element of multEX_0 holds a * (0. multEX_0 ) = 0. multEX_0
Lm28:
for a being Element of multEX_0 holds (0. multEX_0 ) * a = 0. multEX_0
:: deftheorem Def24 defines almost_invertible ALGSTR_1:def 24 :
:: deftheorem ALGSTR_1:def 25 :
canceled;
:: deftheorem Def26 defines multLoop_0-like ALGSTR_1:def 26 :
theorem Th34: :: ALGSTR_1:34
Lm29:
for a, b, c being Element of multEX_0 holds (a * b) * c = a * (b * c)
theorem :: ALGSTR_1:35
canceled;
theorem :: ALGSTR_1:36
canceled;
Lm30:
for a, b being Element of multEX_0 holds a * b = b * a
theorem :: ALGSTR_1:37
canceled;
theorem :: ALGSTR_1:38
canceled;
:: deftheorem Def27 defines " ALGSTR_1:def 27 :
theorem :: ALGSTR_1:39
canceled;
theorem :: ALGSTR_1:40
:: deftheorem defines / ALGSTR_1:def 28 :