:: From Loops to Abelian Multiplicative Groups with Zero
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received July 10, 1990
:: Copyright (c) 1990-2018 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, SUBSET_1, ARYTM_3, SUPINF_2, RLVECT_1,
STRUCT_0, ARYTM_1, VECTSP_1, RELAT_1, MESFUNC1, GROUP_1, BINOP_1,
NUMBERS, BINOP_2, CARD_1, REAL_1, ALGSTR_1, ZFMISC_1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, BINOP_2, FUNCT_7, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1,
RLVECT_1;
constructors BINOP_1, BINOP_2, VECTSP_1, RLVECT_1, FUNCT_5, XXREAL_0, REAL_1,
FUNCT_7, GROUP_1;
registrations NUMBERS, VECTSP_1, ALGSTR_0, XREAL_0, ORDINAL1, STRUCT_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions VECTSP_1, ALGSTR_0, RLVECT_1, GROUP_1;
equalities STRUCT_0, ALGSTR_0, ORDINAL1;
expansions STRUCT_0, VECTSP_1, ALGSTR_0, RLVECT_1, GROUP_1;
theorems RLVECT_1, VECTSP_1, TARSKI, XCMPLX_1, BINOP_2, GROUP_1, ALGSTR_0,
STRUCT_0;
begin :: GROUPS
reserve L for non empty addLoopStr;
reserve a,b,c,x for Element of L;
theorem Th1:
(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)) implies (a+b = 0.L implies b+a = 0.L)
proof
assume that
A1: for a holds a + 0.L = a and
A2: for a ex x st a+x = 0.L and
A3: for a,b,c holds (a+b)+c = a+(b+c);
consider x such that
A4: b + x = 0.L by A2;
assume
A5: a+b = 0.L;
thus b+a = (b+a) + (b+x) by A1,A4
.= ((b+a) + b) + x by A3
.= (b + 0.L) + x by A3,A5
.= 0.L by A1,A4;
end;
theorem
(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)) implies 0.L+a = a+0.L
proof
assume that
A1: for a holds a + 0.L = a and
A2: for a ex x st a+x = 0.L and
A3: for a,b,c holds (a+b)+c = a+(b+c);
consider x such that
A4: a + x = 0.L by A2;
thus 0.L+a = a + (x+a) by A3,A4
.= a+0.L by A1,A2,A3,A4,Th1;
end;
theorem
(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)) implies for a ex x st x+a = 0.L
proof
assume that
A1: for a holds a + 0.L = a and
A2: for a ex x st a+x = 0.L and
A3: for a,b,c holds (a+b)+c = a+(b+c);
let a;
consider x such that
A4: a + x = 0.L by A2;
x+a=0.L by A1,A2,A3,A4,Th1;
hence thesis;
end;
definition
let x be set;
func Extract x -> Element of {x} equals
x;
coherence by TARSKI:def 1;
end;
theorem Th4:
for a,b being Element of Trivial-addLoopStr holds a = b
proof
let a,b be Element of Trivial-addLoopStr;
thus a = {} by TARSKI:def 1
.= b by TARSKI:def 1;
end;
theorem
for a,b be Element of Trivial-addLoopStr holds a+b = 0.
Trivial-addLoopStr by Th4;
Lm1: ( for a be Element of Trivial-addLoopStr holds a + 0.Trivial-addLoopStr =
a)& for a be Element of Trivial-addLoopStr holds 0.Trivial-addLoopStr + a = a
by Th4;
Lm2: for a,b be Element of Trivial-addLoopStr ex x be Element of
Trivial-addLoopStr st a+x=b
proof
let a,b be Element of Trivial-addLoopStr;
take 0.Trivial-addLoopStr;
thus thesis by Th4;
end;
Lm3: for a,b be Element of Trivial-addLoopStr ex x be Element of
Trivial-addLoopStr st x+a=b
proof
let a,b be Element of Trivial-addLoopStr;
take 0.Trivial-addLoopStr;
thus thesis by Th4;
end;
Lm4: ( for a,x,y be Element of Trivial-addLoopStr holds a+x=a+y implies x=y)&
for a,x,y be Element of Trivial-addLoopStr holds x+a=y+a implies x=y by Th4;
definition
let IT be non empty addLoopStr;
attr IT is left_zeroed means
for a being Element of IT holds 0.IT + a = a;
end;
definition
let L be non empty addLoopStr;
attr L is add-left-invertible means
:Def3:
for a,b be Element of L ex x being Element of L st x + a = b;
attr L is add-right-invertible means
:Def4:
for a,b be Element of L ex x being Element of L st a + x = b;
end;
definition
let IT be non empty addLoopStr;
attr IT is Loop-like means
IT is left_add-cancelable
right_add-cancelable add-left-invertible add-right-invertible;
end;
registration
cluster Loop-like -> left_add-cancelable right_add-cancelable
add-left-invertible add-right-invertible for non empty addLoopStr;
coherence;
cluster left_add-cancelable right_add-cancelable add-left-invertible
add-right-invertible -> Loop-like for non empty addLoopStr;
coherence;
end;
theorem Th6:
for L being non empty addLoopStr holds L is Loop-like iff (for a,
b be Element of L ex x being Element of L st a+x=b) & (for a,b be Element of L
ex x being Element of L st x+a=b) & (for a,x,y be Element of L holds a+x=a+y
implies x=y) & for a,x,y be Element of L holds x+a=y+a implies x=y
proof
let L be non empty addLoopStr;
thus L is Loop-like implies (for a,b be Element of L ex x being Element of L
st a+x=b) & (for a,b be Element of L ex x being Element of L st x+a=b) & (for a
,x,y be Element of L holds a+x=a+y implies x=y) & for a,x,y being Element of L
st x+a=y+a holds x=y by Def3,Def4,ALGSTR_0:def 3,def 4;
assume that
A1: ( for a,b be Element of L ex x being Element of L st a+x=b)& for a,b
be Element of L ex x being Element of L st x+a=b and
A2: for a,x,y be Element of L holds a+x=a+y implies x=y and
A3: for a,x,y be Element of L holds x+a=y+a implies x=y;
thus L is left_add-cancelable
proof
let x,x,x be Element of L;
thus thesis by A2;
end;
thus L is right_add-cancelable
proof
let x,x,x be Element of L;
thus thesis by A3;
end;
thus thesis by A1;
end;
Lm5: for a,b,c be Element of Trivial-addLoopStr holds (a+b)+c = a+(b+c) by Th4;
Lm6: for a,b be Element of Trivial-addLoopStr holds a+b = b+a by Th4;
registration
cluster Trivial-addLoopStr -> add-associative Loop-like right_zeroed
left_zeroed;
coherence by Lm1,Lm2,Lm3,Lm4,Lm5,Th6;
end;
registration
cluster strict left_zeroed right_zeroed Loop-like for non empty addLoopStr;
existence
proof
take Trivial-addLoopStr;
thus thesis;
end;
end;
definition
mode Loop is left_zeroed right_zeroed Loop-like non empty addLoopStr;
end;
registration
cluster strict add-associative for Loop;
existence
proof
take Trivial-addLoopStr;
thus thesis;
end;
end;
registration
cluster Loop-like -> add-left-invertible for non empty addLoopStr;
coherence;
cluster add-associative right_zeroed right_complementable -> left_zeroed
Loop-like for non empty addLoopStr;
coherence
proof
let L;
assume
A1: L is add-associative right_zeroed right_complementable;
then reconsider
G = L as add-associative right_zeroed right_complementable non
empty addLoopStr;
A2: for a,x,y be Element of L holds x+a=y +a implies x=y by A1,RLVECT_1:8;
thus for a holds 0.L + a = a by A1,RLVECT_1:4;
A3: for a,b ex x st x+a=b
proof
let a,b;
reconsider a9 = a, b9 = b as Element of G;
reconsider x = b9 + -a9 as Element of L;
take x;
(b9+-a9)+a9 = b9+(-a9+a9) by RLVECT_1:def 3
.= b9+0.G by RLVECT_1:5
.= b by RLVECT_1:4;
hence thesis;
end;
( for a,b ex x st a+x=b)& for a,x,y be Element of L holds a+x=a+y
implies x=y by A1,RLVECT_1:7,8;
hence thesis by A3,A2,Th6;
end;
end;
theorem Th7:
L is AddGroup 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)
proof
thus L is AddGroup implies (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) by Th6,RLVECT_1:def 3,def 4;
assume that
A1: for a holds a + 0.L = a and
A2: for a ex x st a+x = 0.L and
A3: for a,b,c holds (a+b)+c = a+(b+c);
L is right_complementable
proof
let a be Element of L;
thus ex x st a+x = 0.L by A2;
end;
hence thesis by A1,A3,RLVECT_1:def 3,def 4;
end;
registration
cluster Trivial-addLoopStr -> Abelian;
coherence by Lm6;
end;
registration
cluster strict Abelian for AddGroup;
existence
proof
take Trivial-addLoopStr;
thus thesis;
end;
end;
theorem
L is Abelian AddGroup 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 by
Th7,RLVECT_1:def 2;
registration
cluster Trivial-multLoopStr -> non empty;
coherence;
end;
theorem Th9:
for a,b being Element of Trivial-multLoopStr holds a = b
proof
let a,b be Element of Trivial-multLoopStr;
thus a = {} by TARSKI:def 1
.= b by TARSKI:def 1;
end;
theorem
for a,b be Element of Trivial-multLoopStr holds a*b = 1.
Trivial-multLoopStr by Th9;
Lm7: ( for a be Element of Trivial-multLoopStr holds a * 1.
Trivial-multLoopStr = a)& for a be Element of Trivial-multLoopStr holds 1.
Trivial-multLoopStr * a = a by Th9;
Lm8: for a,b be Element of Trivial-multLoopStr ex x be Element of
Trivial-multLoopStr st a*x=b
proof
let a,b be Element of Trivial-multLoopStr;
take 1_Trivial-multLoopStr;
thus thesis by Th9;
end;
Lm9: for a,b be Element of Trivial-multLoopStr ex x be Element of
Trivial-multLoopStr st x*a=b
proof
let a,b be Element of Trivial-multLoopStr;
take 1_Trivial-multLoopStr;
thus thesis by Th9;
end;
definition
let IT be non empty multLoopStr;
attr IT is invertible means
:Def6:
(for a,b be Element of IT ex x being
Element of IT st a*x=b) & for a,b be Element of IT ex x being Element of IT st
x*a=b;
end;
notation
let L be non empty multLoopStr;
synonym L is cancelable for L is mult-cancelable;
end;
registration
cluster strict well-unital invertible cancelable for non empty multLoopStr;
existence
proof
Trivial-multLoopStr is well-unital invertible cancelable by Lm7,Lm8
,Lm9;
hence thesis;
end;
end;
definition
mode multLoop is well-unital invertible cancelable non empty multLoopStr;
end;
registration
cluster Trivial-multLoopStr -> well-unital invertible cancelable;
coherence by Lm7,Lm8,Lm9;
end;
Lm10: for a,b,c be Element of Trivial-multLoopStr holds (a*b)*c = a*(b*c) by
Th9;
registration
cluster strict associative for multLoop;
existence
proof
Trivial-multLoopStr is associative by Lm10;
hence thesis;
end;
end;
definition
mode multGroup is associative multLoop;
end;
reserve L for non empty multLoopStr;
reserve a,b,c,x,y,z for Element of L;
Lm11: (for a holds a * 1.L = a) & (for a ex x st a*x = 1.L) & (for a,b,c holds
(a*b)*c = a*(b*c)) implies (a*b = 1.L implies b*a = 1.L)
proof
assume that
A1: for a holds a * 1.L = a and
A2: for a ex x st a*x = 1.L and
A3: for a,b,c holds (a*b)*c = a*(b*c);
consider x such that
A4: b * x = 1.L by A2;
assume
A5: a*b = 1.L;
thus b*a = (b*a) * (b*x) by A1,A4
.= ((b*a) * b) * x by A3
.= (b * 1.L) * x by A3,A5
.= 1.L by A1,A4;
end;
Lm12: (for a holds a * 1.L = a) & (for a ex x st a*x = 1.L) & (for a,b,c holds
(a*b)*c = a*(b*c)) implies 1.L*a = a*1.L
proof
assume that
A1: for a holds a * 1.L = a and
A2: for a ex x st a*x = 1.L and
A3: for a,b,c holds (a*b)*c = a*(b*c);
consider x such that
A4: a * x = 1.L by A2;
thus 1.L*a = a * (x*a) by A3,A4
.= a*1.L by A1,A2,A3,A4,Lm11;
end;
Lm13: (for a holds a * 1.L = a) & (for a ex x st a*x = 1.L) & (for a,b,c holds
(a*b)*c = a*(b*c)) implies for a ex x st x*a = 1.L
proof
assume that
A1: for a holds a * 1.L = a and
A2: for a ex x st a*x = 1.L and
A3: for a,b,c holds (a*b)*c = a*(b*c);
let a;
consider x such that
A4: a * x = 1.L by A2;
x*a=1.L by A1,A2,A3,A4,Lm11;
hence thesis;
end;
theorem Th11:
L is multGroup iff (for a holds a * 1.L = a) & (for a ex x st a*
x = 1.L) & for a,b,c holds (a*b)*c = a*(b*c)
proof
thus L is multGroup implies (for a holds a * 1.L = a) & (for a ex x st a*x =
1.L) & for a,b,c holds (a*b)*c = a*(b*c) by Def6,GROUP_1:def 3;
assume that
A1: for a holds a * 1.L = a and
A2: for a ex x st a*x = 1.L and
A3: for a,b,c holds (a*b)*c = a*(b*c);
A4: for a,b be Element of L ex x being Element of L st x*a=b
proof
let a,b;
consider y such that
A5: y*a = 1.L by A1,A2,A3,Lm13;
take x = b*y;
thus x*a = b * 1.L by A3,A5
.= b by A1;
end;
A6: for a be Element of L holds 1.L * a = a
proof
let a;
thus 1.L*a = a*1.L by A1,A2,A3,Lm12
.= a by A1;
end;
A7: L is left_mult-cancelable
proof
let a,x,y;
consider z such that
A8: z*a = 1.L by A1,A2,A3,Lm13;
assume a*x = a*y;
then (z*a)*x = z*(a*y) by A3
.= (z*a)*y by A3;
hence x = 1.L * y by A6,A8
.= y by A6;
end;
A9: L is right_mult-cancelable
proof
let a,x,y;
consider z such that
A10: a*z = 1.L by A2;
assume x*a = y*a;
then x*(a*z) = (y*a)*z by A3
.= y*(a*z) by A3;
hence x = y * 1.L by A1,A10
.= y by A1;
end;
for a,b be Element of L ex x being Element of L st a*x=b
proof
let a,b;
consider y such that
A11: a*y = 1.L by A2;
take x = y*b;
thus a*x = 1.L * b by A3,A11
.= b by A6;
end;
hence thesis by A1,A3,A6,A4,A7,A9,Def6,GROUP_1:def 3,VECTSP_1:def 6;
end;
registration
cluster Trivial-multLoopStr -> associative;
coherence by Lm10;
end;
Lm14: for a,b be Element of Trivial-multLoopStr holds a*b = b*a by Th9;
registration
cluster strict commutative for multGroup;
existence
proof
Trivial-multLoopStr is commutative by Lm14;
hence thesis;
end;
end;
theorem
L is commutative multGroup iff (for a holds a * 1.L = a) & (for a ex x
st a*x = 1.L) & (for a,b,c holds (a*b)*c = a*(b*c)) & for a,b holds a*b = b*a
by Th11,GROUP_1:def 12;
notation
let L be invertible cancelable non empty multLoopStr;
let x be Element of L;
synonym x" for /x;
end;
registration
let L be invertible cancelable non empty multLoopStr;
cluster -> left_invertible for Element of L;
coherence
by Def6;
end;
reserve G for multGroup;
reserve a,b,c,x for Element of G;
theorem
a"*a=1.G & a*(a") = 1.G
proof
thus
A1: a"*a = 1.G by ALGSTR_0:def 30;
A2: for a,b,c holds (a*b)*c = a*(b*c) by Th11;
( for a holds a * 1.G = a)& for a ex x st a*x = 1.G by Th11;
hence thesis by A1,A2,Lm11;
end;
:: 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
multLoopStr_0 (# REAL, multreal,In(0,REAL),In(1,REAL) #);
correctness;
end;
registration
cluster multEX_0 -> non empty;
coherence;
end;
Lm15: now
let x, e be Element of multEX_0;
reconsider a = x as Real;
assume
A1: e = 1;
hence x*e = a*1 by BINOP_2:def 11
.= x;
thus e*x = 1*a by A1,BINOP_2:def 11
.= x;
end;
registration
cluster multEX_0 -> well-unital;
coherence
by Lm15;
end;
Lm16: for a,b be Element of multEX_0 st a<>0.multEX_0 ex x be Element of
multEX_0 st a*x=b
proof
let a,b be Element of multEX_0 such that
A1: a<>0.multEX_0;
reconsider p=a, q=b as Element of REAL;
reconsider x=q/p as Element of multEX_0;
p*(q/p) = q by A1,XCMPLX_1:87;
then a*x = b by BINOP_2:def 11;
hence thesis;
end;
Lm17: for a,b be Element of multEX_0 st a<>0.multEX_0 ex x be Element of
multEX_0 st x*a=b
proof
let a,b be Element of multEX_0 such that
A1: a<>0.multEX_0;
reconsider p=a, q=b as Element of REAL;
reconsider x=q/p as Element of multEX_0;
p*(q/p) = q by A1,XCMPLX_1:87;
then x*a = b by BINOP_2:def 11;
hence thesis;
end;
Lm18: for a,x,y be Element of multEX_0 st a<>0.multEX_0 holds a*x=a*y implies
x=y
proof
let a,x,y be Element of multEX_0 such that
A1: a<>0.multEX_0;
reconsider aa=a, p=x, q=y as Real;
assume a*x=a*y;
then aa*p = a*y by BINOP_2:def 11
.= aa*q by BINOP_2:def 11;
hence thesis by A1,XCMPLX_1:5;
end;
Lm19: for a,x,y be Element of multEX_0 st a<>0.multEX_0 holds x*a=y*a implies
x=y
proof
let a,x,y be Element of multEX_0 such that
A1: a<>0.multEX_0;
reconsider aa=a, p=x, q=y as Real;
assume x*a=y*a;
then p*aa = y*a by BINOP_2:def 11
.= q*aa by BINOP_2:def 11;
hence thesis by A1,XCMPLX_1:5;
end;
Lm20: for a be Element of multEX_0 holds a*0.multEX_0 = 0.multEX_0
proof
let a be Element of multEX_0;
reconsider aa=a as Real;
thus a*0.multEX_0 = aa*0 by BINOP_2:def 11
.= 0.multEX_0;
end;
Lm21: for a be Element of multEX_0 holds 0.multEX_0*a = 0.multEX_0
proof
let a be Element of multEX_0;
reconsider aa=a as Real;
thus 0.multEX_0*a = 0*aa by BINOP_2:def 11
.= 0.multEX_0;
end;
definition
let IT be non empty multLoopStr_0;
attr IT is almost_invertible means
:Def8:
(for a,b be Element of IT st a<>
0.IT ex x be Element of IT st a*x=b) & for a,b be Element of IT st a<>0.IT ex x
be Element of IT st x*a=b;
end;
definition
let IT be non empty multLoopStr_0;
attr IT is multLoop_0-like means
IT is almost_invertible
almost_cancelable & (for a be Element of IT holds a*0.IT = 0.IT) & for a be
Element of IT holds 0.IT*a = 0.IT;
end;
::$CT 2
theorem Th14:
for L being non empty multLoopStr_0 holds L is multLoop_0-like
iff (for a,b be Element of L st a<>0.L ex x be Element of L st a*x=b) & (for a,
b be Element of L st a<>0.L ex x be Element of L st x*a=b) & (for a,x,y be
Element of L st a<>0.L holds a*x=a*y implies x=y) & (for a,x,y be Element of L
st a<>0.L holds x*a=y*a implies x=y) & (for a be Element of L holds a*0.L = 0.L
) & for a be Element of L holds 0.L*a = 0.L
proof
let L be non empty multLoopStr_0;
hereby
assume
A1: L is multLoop_0-like;
then
A2: L is almost_invertible almost_cancelable;
hence (for a,b be Element of L st a<>0.L ex x be Element of L st a*x=b) &
for a,b be Element of L st a<>0.L ex x be Element of L st x*a=b;
thus for a,x,y be Element of L st a<>0.L holds a*x=a*y implies x=y
by A2,ALGSTR_0:def 20,def 36;
thus for a,x,y be Element of L st a<>0.L holds x*a=y*a implies x=y
by A2,ALGSTR_0:def 21,def 37;
thus (for a be Element of L holds a*0.L = 0.L) & for a be Element of L
holds 0.L*a = 0.L by A1;
end;
assume that
A3: ( for a,b be Element of L st a<>0.L ex x be Element of L st a*x=b)&
for a,b be Element of L st a<>0.L ex x be Element of L st x*a=b and
A4: for a,x,y be Element of L st a<>0.L holds a*x=a*y implies x=y and
A5: for a,x,y be Element of L st a<>0.L holds x*a=y*a implies x=y and
A6: ( for a be Element of L holds a*0.L = 0.L)& for a be Element of L
holds 0.L*a = 0.L;
A7: L is almost_right_cancelable
proof
let x being Element of L;
assume
A8: x <> 0.L;
let y,z be Element of L;
assume y*x = z*x;
hence thesis by A5,A8;
end;
L is almost_left_cancelable
proof
let x being Element of L;
assume
A9: x <> 0.L;
let y,z be Element of L;
assume x*y = x*z;
hence thesis by A4,A9;
end;
then L is almost_invertible almost_cancelable by A3,A7;
hence thesis by A6;
end;
registration
cluster multLoop_0-like -> almost_invertible almost_cancelable for non empty
multLoopStr_0;
coherence;
end;
registration
cluster strict well-unital multLoop_0-like non degenerated for non empty
multLoopStr_0;
existence
proof
multEX_0 is well-unital multLoop_0-like non degenerated
by Lm16,Lm17
,Lm18,Lm19,Lm20,Lm21,Th14;
hence thesis;
end;
end;
definition
mode multLoop_0 is well-unital non degenerated multLoop_0-like non empty
multLoopStr_0;
end;
registration
cluster multEX_0 -> well-unital multLoop_0-like;
coherence by Lm16,Lm17,Lm18,Lm19,Lm20,Lm21,Th14;
end;
Lm22: for a,b,c be Element of multEX_0 holds (a*b)*c = a*(b*c)
proof
let a,b,c be Element of multEX_0;
reconsider p=a, q=b, r=c as Real;
A1: b*c = q*r by BINOP_2:def 11;
a*b = p*q by BINOP_2:def 11;
hence (a*b)*c = (p*q)*r by BINOP_2:def 11
.= p*(q*r)
.= a*(b*c) by A1,BINOP_2:def 11;
end;
registration
cluster strict associative non degenerated for multLoop_0;
existence
proof
multEX_0 is associative non degenerated by Lm22;
hence thesis;
end;
end;
definition
mode multGroup_0 is associative non degenerated multLoop_0;
end;
registration
cluster multEX_0 -> associative;
coherence by Lm22;
end;
Lm23: for a,b be Element of multEX_0 holds a*b = b*a
proof
let a,b be Element of multEX_0;
reconsider p=a, q=b as Real;
thus a*b = q*p by BINOP_2:def 11
.= b*a by BINOP_2:def 11;
end;
registration
cluster strict commutative for multGroup_0;
existence
proof
multEX_0 is commutative non degenerated by Lm23;
hence thesis;
end;
end;
notation
let L be almost_invertible almost_cancelable non empty multLoopStr_0;
let x be Element of L;
synonym x" for /x;
end;
definition
let L be almost_invertible almost_cancelable non empty multLoopStr_0;
let x be Element of L;
assume
A1: x<>0.L;
redefine func x" means
:Def10:
it*x = 1.L;
compatibility
proof
let IT be Element of L;
ex x1 being Element of L st x1*x = 1.L by A1,Def8;
then
A2: x is left_invertible;
x is right_mult-cancelable by A1,ALGSTR_0:def 37;
hence thesis by A2,ALGSTR_0:def 30;
end;
end;
reserve G for associative almost_invertible almost_cancelable well-unital non
empty multLoopStr_0;
reserve a,x for Element of G;
theorem
a<>0.G implies a"*a=1.G & a*(a") = 1.G
proof
assume
A1: a<>0.G;
hence
A2: a"*a = 1.G by Def10;
consider x such that
A3: a*x = 1.G by A1,Def8;
a"*a*x = a" * 1.G by A3,GROUP_1:def 3;
then x = a" * 1.G by A2;
hence thesis by A3;
end;
definition
let L be almost_invertible almost_cancelable non empty multLoopStr_0;
let a, b be Element of L;
func a/b -> Element of L equals
a*(b");
correctness;
end;
:: from SCMRING1, 2010,02.06, A.T.
registration
cluster -> Abelian add-associative right_zeroed right_complementable
for 1-element addLoopStr;
coherence
proof
let S be 1-element addLoopStr;
thus (for v, w being Element of S holds v + w = w + v) & (for u, v, w
being Element of S holds u + v + w = u + (v + w)) & for v being Element of S
holds v + 0.S = v by STRUCT_0:def 10;
let v be Element of S;
take v;
thus thesis by STRUCT_0:def 10;
end;
cluster trivial -> well-unital right-distributive for
non empty doubleLoopStr;
coherence;
end;
registration
cluster -> Group-like associative commutative for 1-element multMagma;
coherence
proof
let H be 1-element multMagma;
hereby
set e = the Element of H;
take e;
let h be Element of H;
thus h * e = h & e * h = h by STRUCT_0:def 10;
take g = e;
thus h * g = e & g * h = e by STRUCT_0:def 10;
end;
thus for x, y, z being Element of H holds x*y*z = x*(y*z) by
STRUCT_0:def 10;
let x, y be Element of H;
thus thesis by STRUCT_0:def 10;
end;
end;