### The Mizar article:

### From Loops to Abelian Multiplicative Groups with Zero

**by****Michal Muzalewski, and****Wojciech Skaba**

- Received July 10, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: ALGSTR_1
- [ MML identifier index ]

environ vocabulary RLVECT_1, BOOLE, MIDSP_1, REALSET1, ARYTM_1, VECTSP_1, CAT_1, VECTSP_2, BINOP_1, RELAT_1, ARYTM_3, FUNCT_1, ALGSTR_1; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, REAL_1, BINOP_1, STRUCT_0, VECTSP_1, RLVECT_1, VECTSP_2, MIDSP_1; constructors BINOP_1, VECTSP_2, MIDSP_1, REAL_1, MEMBERED, XBOOLE_0; clusters SUBSET_1, VECTSP_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE, ARITHM; definitions RLVECT_1, STRUCT_0; theorems RLVECT_1, VECTSP_1, VECTSP_2, TARSKI, XCMPLX_1; begin :: GROUPS reserve L for non empty LoopStr; reserve a,b,c,x,y,z 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 A1: (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)); assume A2: a+b = 0.L; consider x such that A3: b + x = 0.L by A1; thus b+a = (b+a) + (b+x) by A1,A3 .= ((b+a) + b) + x by A1 .= (b + 0.L) + x by A1,A2 .= 0.L by A1,A3; end; theorem Th2: (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 A1: (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)); then consider x such that A2: a + x = 0.L; thus 0.L+a = a + (x+a) by A1,A2 .= a+0.L by A1,A2,Th1; end; theorem Th3: (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 A1: (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)); let a; consider x such that A2: a + x = 0.L by A1; x+a=0.L by A1,A2,Th1; hence thesis; end; definition let x be set; canceled 2; func Extract x -> Element of {x} equals x; coherence by TARSKI:def 1; end; definition func L_Trivial -> strict LoopStr equals :Def4: LoopStr (# {{}}, op2, Extract {} #); correctness; end; definition cluster L_Trivial -> non empty; coherence proof thus the carrier of L_Trivial is non empty by Def4; end; end; canceled; theorem Th5: for a,b being Element of L_Trivial holds a = b proof let a,b be Element of L_Trivial; thus a = {} by Def4,TARSKI:def 1 .= b by Def4,TARSKI:def 1; end; theorem for a,b be Element of L_Trivial holds a+b = 0.L_Trivial by Th5; Lm1: for a be Element of L_Trivial holds a + 0.L_Trivial = a by Th5; Lm2: for a be Element of L_Trivial holds 0.L_Trivial + a = a by Th5; Lm3: for a,b be Element of L_Trivial ex x be Element of L_Trivial st a+x=b proof let a,b be Element of L_Trivial; take x = 0.L_Trivial; thus a+x = b by Th5; end; Lm4: for a,b be Element of L_Trivial ex x be Element of L_Trivial st x+a=b proof let a,b be Element of L_Trivial; take x = 0.L_Trivial; thus x+a = b by Th5; end; Lm5: for a,x,y be Element of L_Trivial holds a+x=a+y implies x=y by Th5; Lm6: for a,x,y be Element of L_Trivial holds x+a=y+a implies x=y by Th5; definition let IT be non empty LoopStr; attr IT is left_zeroed means :Def5: for a being Element of IT holds 0.IT + a = a; end; definition let L be non empty LoopStr; attr L is add-left-cancelable means :Def6: for a,b,c being Element of L holds a + b = a + c implies b = c; attr L is add-right-cancelable means :Def7: for a,b,c being Element of L holds b + a = c + a implies b = c; attr L is add-left-invertible means :Def8: for a,b be Element of L ex x being Element of L st x + a = b; attr L is add-right-invertible means :Def9: for a,b be Element of L ex x being Element of L st a + x = b; end; definition let IT be non empty LoopStr; attr IT is Loop-like means :Def10: IT is add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible; end; definition cluster Loop-like -> add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible (non empty LoopStr); coherence by Def10; cluster add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible -> Loop-like (non empty LoopStr); coherence by Def10; end; theorem Th7: for L being non empty LoopStr 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 LoopStr; hereby assume L is Loop-like; then A1: L is add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible by Def10; hence for a,b be Element of L ex x being Element of L st a+x=b by Def9; thus for a,b be Element of L ex x being Element of L st x+a=b by A1,Def8; thus for a,x,y be Element of L holds a+x=a+y implies x=y by A1,Def6; let a,x,y be Element of L; thus x+a=y+a implies x=y by A1,Def7; end; assume (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); hence L is add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible by Def6,Def7,Def8,Def9; end; Lm7: for a,b,c be Element of L_Trivial holds (a+b)+c = a+(b+c) by Th5; Lm8: for a,b be Element of L_Trivial holds a+b = b+a by Th5; definition cluster L_Trivial -> add-associative Loop-like right_zeroed left_zeroed; coherence by Def5,Lm1,Lm2,Lm3,Lm4,Lm5,Lm6,Lm7,Th7,RLVECT_1:def 6,def 7; end; definition cluster strict left_zeroed right_zeroed Loop-like (non empty LoopStr); existence proof take L_Trivial; thus thesis; end; end; definition mode Loop is left_zeroed right_zeroed Loop-like (non empty LoopStr); end; definition cluster strict add-associative Loop; existence proof take L_Trivial; thus thesis; end; end; definition mode Group is add-associative Loop; end; definition cluster Loop-like -> right_complementable (non empty LoopStr); coherence proof let L be (non empty LoopStr); assume L is Loop-like; hence for a being Element of L ex x being Element of L st a+x = 0.L by Th7; end; cluster add-associative right_zeroed right_complementable -> left_zeroed Loop-like (non empty LoopStr); 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 LoopStr); thus for a holds 0.L + a = a by A1,RLVECT_1:10; now thus for a,b ex x st a+x=b by A1,RLVECT_1:20; thus for a,b ex x st x+a=b proof let a,b; reconsider a' = a, b' = b as Element of G; reconsider x = b' + -a' as Element of L; take x; (b'+-a')+a' = b'+(-a'+a') by RLVECT_1:def 6 .= b'+0.G by RLVECT_1:16 .= b by RLVECT_1:10; hence thesis; end; thus (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 by A1,RLVECT_1:21; end; hence L is Loop-like by Th7; end; end; canceled; theorem Th9: L is Group 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 Group 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 Th7,RLVECT_1:def 6,def 7; assume A1: (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)); now thus A2: for a be Element of L holds 0.L + a = a proof let a; thus 0.L+a = a+0.L by A1,Th2 .= a by A1; end; thus 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 A3: a+y = 0.L by A1; take x = y+b; thus a+x = 0.L + b by A1,A3 .= b by A2; end; thus 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 A4: y+a = 0.L by A1,Th3; take x = b+y; thus x+a = b + 0.L by A1,A4 .= b by A1; end; thus for a,x,y be Element of L holds a+x=a+y implies x=y proof let a,x,y; consider z such that A5: z+a = 0.L by A1,Th3; assume a+x = a+y; then (z+a)+x = z+(a+y) by A1 .= (z+a)+y by A1; hence x = 0.L + y by A2,A5 .= y by A2; end; thus for a,x,y be Element of L holds x+a=y+a implies x=y proof let a,x,y; consider z such that A6: a+z = 0.L by A1; assume x+a = y+a; then x+(a+z) = (y+a)+z by A1 .= y+(a+z) by A1; hence x = y + 0.L by A1,A6 .= y by A1; end; end; hence thesis by A1,Def5,Th7,RLVECT_1:def 6,def 7; end; definition cluster L_Trivial -> Abelian; coherence by Lm8,RLVECT_1:def 5; end; definition cluster strict Abelian Group; existence proof take L_Trivial; thus thesis; end; end; canceled; theorem L is Abelian Group 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 Th9,RLVECT_1:def 5; definition func multL_Trivial -> strict multLoopStr equals :Def11: multLoopStr (# {{}}, op2, Extract {} #); correctness; end; definition cluster multL_Trivial -> non empty; coherence proof thus the carrier of multL_Trivial is non empty by Def11; end; end; canceled 6; theorem Th18: for a,b being Element of multL_Trivial holds a = b proof let a,b be Element of multL_Trivial; thus a = {} by Def11,TARSKI:def 1 .= b by Def11,TARSKI:def 1; end; theorem for a,b be Element of multL_Trivial holds a*b = 1_ multL_Trivial by Th18; Lm9: for a be Element of multL_Trivial holds a * 1_ multL_Trivial = a by Th18; Lm10: for a be Element of multL_Trivial holds 1_ multL_Trivial * a = a by Th18; Lm11: for a,b be Element of multL_Trivial ex x be Element of multL_Trivial st a*x=b proof let a,b be Element of multL_Trivial; take x = 1_ multL_Trivial; thus a*x = b by Th18; end; Lm12: for a,b be Element of multL_Trivial ex x be Element of multL_Trivial st x*a=b proof let a,b be Element of multL_Trivial; take x = 1_ multL_Trivial; thus x*a = b by Th18; end; Lm13: for a,x,y be Element of multL_Trivial holds a*x=a*y implies x=y by Th18; Lm14: for a,x,y be Element of multL_Trivial holds x*a=y*a implies x=y by Th18; definition let IT be non empty multLoopStr; attr IT is invertible means :Def12: (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); attr IT is cancelable means :Def13: (for a,x,y be Element of IT holds a*x=a*y implies x=y) & (for a,x,y be Element of IT holds x*a=y*a implies x=y); end; definition cluster strict well-unital invertible cancelable (non empty multLoopStr); existence proof multL_Trivial is well-unital invertible cancelable by Def12,Def13,Lm9,Lm10,Lm11,Lm12,Lm13,Lm14,VECTSP_2:def 2; hence thesis; end; end; definition mode multLoop is well-unital invertible cancelable (non empty multLoopStr); end; definition cluster multL_Trivial -> well-unital invertible cancelable; coherence by Def12,Def13,Lm9,Lm10,Lm11,Lm12,Lm13,Lm14,VECTSP_2:def 2; end; Lm15: for a,b,c be Element of multL_Trivial holds (a*b)*c = a*(b*c) by Th18; definition cluster strict associative multLoop; existence proof multL_Trivial is associative by Lm15,VECTSP_1:def 16; 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; Lm16: (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 A1: (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)); assume A2: a*b = 1_ L; consider x such that A3: b * x = 1_ L by A1; thus b*a = (b*a) * (b*x) by A1,A3 .= ((b*a) * b) * x by A1 .= (b * 1_ L) * x by A1,A2 .= 1_ L by A1,A3; end; Lm17: (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 A1: (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)); then consider x such that A2: a * x = 1_ L; thus 1_ L*a = a * (x*a) by A1,A2 .= a*1_ L by A1,A2,Lm16; end; Lm18: (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 A1: (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)); let a; consider x such that A2: a * x = 1_ L by A1; x*a=1_ L by A1,A2,Lm16; hence thesis; end; canceled 2; theorem Th22: 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 Def12,VECTSP_1:def 16,VECTSP_2:def 2; assume A1: (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)); now thus A2: for a be Element of L holds 1_ L * a = a proof let a; thus 1_ L*a = a*1_ L by A1,Lm17 .= a by A1; end; thus 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 A3: a*y = 1_ L by A1; take x = y*b; thus a*x = 1_ L * b by A1,A3 .= b by A2; end; thus 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 A4: y*a = 1_ L by A1,Lm18; take x = b*y; thus x*a = b * 1_ L by A1,A4 .= b by A1; end; thus for a,x,y be Element of L holds a*x=a*y implies x=y proof let a,x,y; consider z such that A5: z*a = 1_ L by A1,Lm18; assume a*x = a*y; then (z*a)*x = z*(a*y) by A1 .= (z*a)*y by A1; hence x = 1_ L * y by A2,A5 .= y by A2; end; thus for a,x,y be Element of L holds x*a=y*a implies x=y proof let a,x,y; consider z such that A6: a*z = 1_ L by A1; assume x*a = y*a; then x*(a*z) = (y*a)*z by A1 .= y*(a*z) by A1; hence x = y * 1_ L by A1,A6 .= y by A1; end; end; hence thesis by A1,Def12,Def13,VECTSP_1:def 16,VECTSP_2:def 2; end; definition cluster multL_Trivial -> associative; coherence by Lm15,VECTSP_1:def 16; end; Lm19: for a,b be Element of multL_Trivial holds a*b = b*a by Th18; definition cluster strict commutative multGroup; existence proof multL_Trivial is commutative by Lm19,VECTSP_1:def 17; hence thesis; end; end; canceled; 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 Th22,VECTSP_1:def 17; definition let L be invertible cancelable (non empty multLoopStr); let a be Element of L; canceled 2; func a" -> Element of L means :Def16: a*it = 1_ L; existence by Def12; uniqueness by Def13; end; reserve G for multGroup; reserve a,b,c,x for Element of G; canceled; theorem a*(a") = 1_ G & a"*a=1_ G proof thus A1: a*(a") = 1_ G by Def16; (for a holds a * 1_ G = a) & (for a ex x st a*x = 1_ G) & (for a,b,c holds (a*b)*c = a*(b*c)) by Th22; hence (a")*a = 1_ G by A1,Lm16; 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; definition canceled 3; func multEX_0 -> strict multLoopStr_0 equals :Def21: multLoopStr_0 (# REAL, multreal, 1, 0 #); correctness; end; definition cluster multEX_0 -> non empty; coherence proof thus the carrier of multEX_0 is non empty by Def21; end; end; Lm20: for a,b be Element of multEX_0 for x,y be Real holds a = x & b = y implies a * b = x * y proof let a,b be Element of multEX_0; let x,y be Real; assume a=x & b=y; hence a * b = (multreal).(x,y) by Def21,VECTSP_1:def 10 .= x * y by VECTSP_1:def 14; end; Lm21: 0 = 0.multEX_0 by Def21,RLVECT_1:def 2; Lm22: 1 = 1_ multEX_0 by Def21,VECTSP_1:def 9; Lm23: for a be Element of multEX_0 holds a * 1_ multEX_0 = a proof let a be Element of multEX_0; reconsider aa=a as Real by Def21; thus a * 1_ multEX_0 = (multreal).(aa,1) by Def21,Lm22,VECTSP_1:def 10 .= aa * 1 by VECTSP_1:def 14 .= a; end; Lm24: for a be Element of multEX_0 holds 1_ multEX_0 * a = a proof let a be Element of multEX_0; reconsider aa=a as Real by Def21; thus 1_ multEX_0 * a = (multreal).(1,aa) by Def21,Lm22,VECTSP_1:def 10 .= 1 * aa by VECTSP_1:def 14 .= a; end; canceled 5; theorem Th32: for q,p be Real st q<>0 ex y be Real st p=q*y proof let q,p be Real; reconsider y = p/q as Real; assume A1: q<>0; take y; thus thesis by A1,XCMPLX_1:88; end; theorem Th33: for q,p be Real st q<>0 ex y be Real st p=y*q proof let q,p be Real; reconsider y =p/q as Real; assume A1: q<>0; take y; thus thesis by A1,XCMPLX_1:88; end; Lm25: 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 Real by Def21; consider r be Real such that A2: p*r = q by A1,Lm21,Th32; reconsider x=r as Element of multEX_0 by Def21; a*x = b by A2,Lm20; hence thesis; end; Lm26: 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 Real by Def21; consider r be Real such that A2: r*p = q by A1,Lm21,Th33; reconsider x=r as Element of multEX_0 by Def21; x*a = b by A2,Lm20; hence thesis; end; Lm27: 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; assume A2: a*x=a*y; reconsider aa=a, p=x, q=y as Real by Def21; aa*p = a*y by A2,Lm20 .= aa*q by Lm20; hence thesis by A1,Lm21,XCMPLX_1:5; end; Lm28: 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; assume A2: x*a=y*a; reconsider aa=a, p=x, q=y as Real by Def21; p*aa = y*a by A2,Lm20 .= q*aa by Lm20; hence thesis by A1,Lm21,XCMPLX_1:5; end; Lm29: 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 by Def21; thus a*0.multEX_0 = aa*0 by Lm20,Lm21 .= 0.multEX_0 by Def21,RLVECT_1:def 2; end; Lm30: 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 by Def21; thus 0.multEX_0*a = 0*aa by Lm20,Lm21 .= 0.multEX_0 by Def21,RLVECT_1:def 2; end; definition let IT be non empty multLoopStr_0; attr IT is almost_invertible means :Def22: (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); attr IT is almost_cancelable means :Def23: (for a,x,y be Element of IT st a<>0.IT holds a*x=a*y implies x=y) & (for a,x,y be Element of IT st a<>0.IT holds x*a=y*a implies x=y); end; definition let IT be non empty multLoopStr_0; attr IT is multLoop_0-like means :Def24: 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; theorem Th34: 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 L is multLoop_0-like; then L is almost_invertible almost_cancelable & (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 Def24; 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) & (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) by Def22,Def23; end; assume (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); then L is almost_invertible almost_cancelable & (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 Def22,Def23; hence thesis by Def24; end; definition cluster multLoop_0-like -> almost_invertible almost_cancelable (non empty multLoopStr_0); coherence by Def24; end; definition cluster strict well-unital multLoop_0-like non degenerated (non empty multLoopStr_0); existence proof multEX_0 is well-unital multLoop_0-like non degenerated by Lm21,Lm22,Lm23,Lm24,Lm25,Lm26,Lm27,Lm28,Lm29,Lm30,Th34,VECTSP_1:def 21, VECTSP_2:def 2; hence thesis; end; end; definition mode multLoop_0 is well-unital non degenerated multLoop_0-like (non empty multLoopStr_0); end; definition cluster multEX_0 -> well-unital multLoop_0-like; coherence by Lm23,Lm24,Lm25,Lm26,Lm27,Lm28,Lm29,Lm30,Th34,VECTSP_2:def 2; end; Lm31: 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 by Def21; A1: a*b = p*q by Lm20; A2: b*c = q*r by Lm20; thus (a*b)*c = (p*q)*r by A1,Lm20 .= p*(q*r) by XCMPLX_1:4 .= a*(b*c) by A2,Lm20; end; definition cluster strict associative non degenerated multLoop_0; existence proof multEX_0 is associative non degenerated by Lm21,Lm22,Lm31,VECTSP_1:def 16,def 21; hence thesis; end; end; definition mode multGroup_0 is associative non degenerated multLoop_0; end; reserve L for non empty multLoopStr_0; reserve a,b,c,x,y,z for Element of L; Lm32: 0.L <> 1_ L & (for a holds a * 1_ L = a) & (for a st a<>0.L ex x st a*x = 1_ L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a holds a*0.L = 0.L) implies (a*b = 1_ L implies b*a = 1_ L) proof assume that A1: 0.L <> 1_ L and A2: for a holds a * 1_ L = a and A3: for a st a<>0.L ex x st a*x = 1_ L and A4: for a,b,c holds (a*b)*c = a*(b*c) and A5: for a holds a*0.L = 0.L; assume A6: a*b = 1_ L; then b<>0.L by A1,A5; then consider x such that A7: b * x = 1_ L by A3; thus b*a = (b*a) * (b*x) by A2,A7 .= ((b*a) * b) * x by A4 .= (b * 1_ L) * x by A4,A6 .= 1_ L by A2,A7; end; Lm33: 0.L <> 1_ L & (for a holds a * 1_ L = a) & (for a st a<>0.L ex x st a*x = 1_ L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a holds a*0.L = 0.L) implies 1_ L*a = a*1_ L proof assume that A1: 0.L <> 1_ L and A2: for a holds a * 1_ L = a and A3: for a st a<>0.L ex x st a*x = 1_ L and A4: for a,b,c holds (a*b)*c = a*(b*c) and A5: for a holds a*0.L = 0.L; A6: a<>0.L implies 1_ L*a = a*1_ L proof assume a<>0.L; then consider x such that A7: a * x = 1_ L by A3; thus 1_ L*a = a * (x*a) by A4,A7 .= a*1_ L by A1,A2,A3,A4,A5,A7,Lm32; end; a=0.L implies 1_ L*a = a*1_ L proof assume A8: a=0.L; hence 1_ L*a = 0.L by A5 .= a*1_ L by A2,A8; end; hence thesis by A6; end; Lm34: 0.L <> 1_ L & (for a holds a * 1_ L = a) & (for a st a<>0.L ex x st a*x = 1_ L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a holds a*0.L = 0.L) implies for a st a<>0.L ex x st x*a = 1_ L proof assume that A1: 0.L <> 1_ L and A2: for a holds a * 1_ L = a and A3: for a st a<>0.L ex x st a*x = 1_ L and A4: for a,b,c holds (a*b)*c = a*(b*c) and A5: for a holds a*0.L = 0.L; let a; assume a<>0.L; then consider x such that A6: a * x = 1_ L by A3; x*a=1_ L by A1,A2,A3,A4,A5,A6,Lm32; hence thesis; end; canceled; theorem Th36: L is multGroup_0 iff 0.L <> 1_ L & (for a holds a * 1_ L = a) & (for a st a<>0.L ex x st a*x = 1_ L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a holds a*0.L = 0.L) & (for a holds 0.L*a = 0.L) proof thus L is multGroup_0 implies 0.L <> 1_ L & (for a holds a * 1_ L = a) & (for a st a<>0.L ex x st a*x = 1_ L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a holds a*0.L = 0.L) & (for a holds 0.L*a = 0.L) by Th34,VECTSP_1:def 16,def 21,VECTSP_2:def 2; assume that A1: 0.L <> 1_ L and A2: for a holds a * 1_ L = a and A3: for a st a<>0.L ex x st a*x = 1_ L and A4: for a,b,c holds (a*b)*c = a*(b*c) and A5: for a holds a*0.L = 0.L and A6: for a holds 0.L*a = 0.L; now thus A7: 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,A4,A5,Lm33 .= a by A2; end; thus for a,b be Element of L st a<>0.L ex x be Element of L st a*x=b proof let a,b; assume a<>0.L; then consider y such that A8: a*y = 1_ L by A3; take x = y*b; thus a*x = 1_ L * b by A4,A8 .= b by A7; end; thus for a,b be Element of L st a<>0.L ex x be Element of L st x*a=b proof let a,b; assume a<>0.L; then consider y such that A9: y*a = 1_ L by A1,A2,A3,A4,A5,Lm34; take x = b*y; thus x*a = b * 1_ L by A4,A9 .= b by A2; end; thus for a,x,y be Element of L st a<>0.L holds a*x=a*y implies x=y proof let a,x,y; assume a<>0.L; then consider z such that A10: z*a = 1_ L by A1,A2,A3,A4,A5,Lm34; assume a*x = a*y; then (z*a)*x = z*(a*y) by A4 .= (z*a)*y by A4; hence x = 1_ L * y by A7,A10 .= y by A7; end; thus for a,x,y be Element of L st a<>0.L holds x*a=y*a implies x=y proof let a,x,y; assume a<>0.L; then consider z such that A11: a*z = 1_ L by A3; assume x*a = y*a; then x*(a*z) = (y*a)*z by A4 .= y*(a*z) by A4; hence x = y * 1_ L by A2,A11 .= y by A2; end; end; hence thesis by A1,A2,A4,A5,A6,Th34,VECTSP_1:def 16,def 21,VECTSP_2:def 2; end; definition cluster multEX_0 -> associative; coherence by Lm31,VECTSP_1:def 16; end; Lm35: 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 by Def21; thus a*b = q*p by Lm20 .= b*a by Lm20; end; definition cluster strict commutative multGroup_0; existence proof multEX_0 is commutative non degenerated by Lm21,Lm22,Lm35,VECTSP_1:def 17,def 21; hence thesis; end; end; canceled; theorem L is commutative multGroup_0 iff (0.L <> 1_ L) & (for a holds a * 1_ L = a) & (for a st a<>0.L ex x st a*x = 1_ L) & (for a,b,c holds (a*b)*c = a*(b*c)) & (for a holds a*0.L = 0.L) & (for a holds 0.L*a = 0.L) & (for a,b holds a*b = b*a) by Th36,VECTSP_1:def 17; definition let L be almost_invertible almost_cancelable (non empty multLoopStr_0); let a be Element of L; assume A1: a<>0.L; func a" -> Element of L means :Def25: a*it = 1_ L; existence by A1,Def22; uniqueness by A1,Def23; end; reserve G for associative almost_invertible almost_cancelable well-unital (non empty multLoopStr_0); reserve a,x for Element of G; canceled; 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 Def25; consider x such that A3: x*a = 1_ G by A1,Def22; x*(a*(a")) = 1_ G * (a") by A3,VECTSP_1:def 16; then x = 1_ G * (a") by A2,VECTSP_2:def 2; hence thesis by A3,VECTSP_2:def 2; 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;

Back to top