Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### From Loops to Abelian Multiplicative Groups with Zero

by
Michal Muzalewski, and
Wojciech Skaba

MML identifier: ALGSTR_1
[ Mizar article, 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;

begin :: GROUPS

reserve L for non empty LoopStr;
reserve a,b,c,x,y,z for Element of L;

theorem :: ALGSTR_1:1
(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);

theorem :: ALGSTR_1:2
(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;

theorem :: ALGSTR_1:3
(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;

definition let x be set;
canceled 2;

func Extract x -> Element of {x} equals
:: ALGSTR_1:def 3
x;
end;

definition
func L_Trivial -> strict LoopStr equals
:: ALGSTR_1:def 4
LoopStr (# {{}}, op2, Extract {} #);
end;

definition
cluster L_Trivial -> non empty;
end;

canceled;

theorem :: ALGSTR_1:5
for a,b being Element of L_Trivial holds a = b;

theorem :: ALGSTR_1:6
for a,b be Element of L_Trivial holds a+b = 0.L_Trivial;

definition let IT be non empty LoopStr;
attr IT is left_zeroed means
:: ALGSTR_1:def 5
for a being Element of IT holds 0.IT + a = a;
end;

definition let L be non empty LoopStr;
:: ALGSTR_1:def 6
for a,b,c being Element of L holds
a + b = a + c implies b = c;

:: ALGSTR_1:def 7
for a,b,c being Element of L holds
b + a = c + a implies b = c;

:: ALGSTR_1:def 8
for a,b be Element of L
ex x being Element of L st x + a = b;

:: ALGSTR_1:def 9
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
:: ALGSTR_1:def 10
end;

definition
Loop-like (non empty LoopStr);
end;

theorem :: ALGSTR_1:7
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);

definition
cluster L_Trivial -> add-associative Loop-like right_zeroed left_zeroed;
end;

definition
cluster strict left_zeroed right_zeroed Loop-like (non empty LoopStr);
end;

definition
mode Loop is left_zeroed right_zeroed Loop-like (non empty LoopStr);
end;

definition
end;

definition
end;

definition
cluster Loop-like -> right_complementable (non empty LoopStr);
-> left_zeroed Loop-like (non empty LoopStr);
end;

canceled;

theorem :: ALGSTR_1:9
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));

definition
cluster L_Trivial -> Abelian;
end;

definition
cluster strict Abelian Group;
end;

canceled;

theorem :: ALGSTR_1:11
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);

definition
func multL_Trivial -> strict multLoopStr equals
:: ALGSTR_1:def 11
multLoopStr (# {{}}, op2, Extract {} #);
end;

definition
cluster multL_Trivial -> non empty;
end;

canceled 6;

theorem :: ALGSTR_1:18
for a,b being Element of multL_Trivial holds a = b;

theorem :: ALGSTR_1:19
for a,b be Element of multL_Trivial
holds a*b = 1_ multL_Trivial;

definition let IT be non empty multLoopStr;
attr IT is invertible means
:: ALGSTR_1:def 12
(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
:: ALGSTR_1:def 13
(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);
end;

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

definition
cluster multL_Trivial -> well-unital invertible cancelable;
end;

definition
cluster strict associative multLoop;
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;

canceled 2;

theorem :: ALGSTR_1:22
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));

definition
cluster multL_Trivial -> associative;
end;

definition
cluster strict commutative multGroup;
end;

canceled;

theorem :: ALGSTR_1:24
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);

definition
let L be invertible cancelable (non empty multLoopStr);
let a be Element of L;
canceled 2;

func a" -> Element of L means
:: ALGSTR_1:def 16
a*it = 1_ L;
end;

reserve G for multGroup;
reserve a,b,c,x for Element of G;

canceled;

theorem :: ALGSTR_1:26
a*(a") = 1_ G & a"*a=1_ G;

definition
let L be invertible cancelable (non empty multLoopStr);
let a, b be Element of L;
func a/b -> Element of L equals
:: ALGSTR_1:def 17
a*(b");
end;

definition
canceled 3;

func multEX_0 -> strict multLoopStr_0 equals
:: ALGSTR_1:def 21
multLoopStr_0 (# REAL, multreal, 1, 0 #);
end;

definition
cluster multEX_0 -> non empty;
end;

canceled 5;

theorem :: ALGSTR_1:32
for q,p be Real st q<>0 ex y be Real st p=q*y;

theorem :: ALGSTR_1:33
for q,p be Real st q<>0 ex y be Real st p=y*q;

definition let IT be non empty multLoopStr_0;
attr IT is almost_invertible means
:: ALGSTR_1:def 22
(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
:: ALGSTR_1:def 23
(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
:: ALGSTR_1:def 24
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 :: ALGSTR_1:34
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);

definition
cluster multLoop_0-like -> almost_invertible almost_cancelable
(non empty multLoopStr_0);
end;

definition
cluster strict well-unital multLoop_0-like non degenerated
(non empty multLoopStr_0);
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;
end;

definition
cluster strict associative non degenerated multLoop_0;
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;

canceled;

theorem :: ALGSTR_1:36
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);

definition
cluster multEX_0 -> associative;
end;

definition
cluster strict commutative multGroup_0;
end;

canceled;

theorem :: ALGSTR_1:38
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);

definition
let L be almost_invertible almost_cancelable (non empty multLoopStr_0);
let a be Element of L;
assume  a<>0.L;
func a" -> Element of L means
:: ALGSTR_1:def 25
a*it = 1_ L;
end;

reserve G for associative almost_invertible almost_cancelable well-unital
(non empty multLoopStr_0);
reserve a,x for Element of G;

canceled;

theorem :: ALGSTR_1:40
a<>0.G implies a*(a") = 1_ G & a"*a=1_ G;

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
:: ALGSTR_1:def 26
a*(b");
end;

```