:: From Loops to Abelian Multiplicative Groups with Zero
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received July 10, 1990
:: Copyright (c) 1990-2021 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;
begin :: GROUPS
reserve L for non empty addLoopStr;
reserve a,b,c,x 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;
func Extract x -> Element of {x} equals
:: ALGSTR_1:def 1
x;
end;
theorem :: ALGSTR_1:4
for a,b being Element of Trivial-addLoopStr holds a = b;
theorem :: ALGSTR_1:5
for a,b be Element of Trivial-addLoopStr holds a+b = 0.
Trivial-addLoopStr;
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;
definition
let L be non empty addLoopStr;
attr L is add-left-invertible means
:: ALGSTR_1:def 3
for a,b be Element of L ex x being Element of L st x + a = b;
attr L is add-right-invertible means
:: ALGSTR_1:def 4
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
:: ALGSTR_1:def 5
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;
cluster left_add-cancelable right_add-cancelable add-left-invertible
add-right-invertible -> Loop-like for non empty addLoopStr;
end;
theorem :: ALGSTR_1:6
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;
registration
cluster Trivial-addLoopStr -> add-associative Loop-like right_zeroed
left_zeroed;
end;
registration
cluster strict left_zeroed right_zeroed Loop-like for non empty addLoopStr;
end;
definition
mode Loop is left_zeroed right_zeroed Loop-like non empty addLoopStr;
end;
registration
cluster strict add-associative for Loop;
end;
registration
cluster Loop-like -> add-left-invertible for non empty addLoopStr;
cluster add-associative right_zeroed right_complementable -> left_zeroed
Loop-like for non empty addLoopStr;
end;
theorem :: ALGSTR_1:7
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);
registration
cluster Trivial-addLoopStr -> Abelian;
end;
registration
cluster strict Abelian for AddGroup;
end;
theorem :: ALGSTR_1:8
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;
registration
cluster Trivial-multLoopStr -> non empty;
end;
theorem :: ALGSTR_1:9
for a,b being Element of Trivial-multLoopStr holds a = b;
theorem :: ALGSTR_1:10
for a,b be Element of Trivial-multLoopStr holds a*b = 1.
Trivial-multLoopStr;
definition
let IT be non empty multLoopStr;
attr IT is invertible means
:: ALGSTR_1:def 6
(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;
end;
definition
mode multLoop is well-unital invertible cancelable non empty multLoopStr;
end;
registration
cluster Trivial-multLoopStr -> well-unital invertible cancelable;
end;
registration
cluster strict associative for 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;
theorem :: ALGSTR_1:11
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);
registration
cluster Trivial-multLoopStr -> associative;
end;
registration
cluster strict commutative for multGroup;
end;
theorem :: ALGSTR_1:12
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
;
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;
end;
reserve G for multGroup;
reserve a,b,c,x for Element of G;
theorem :: ALGSTR_1:13
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
:: a*(b");
:: correctness;
:: end;
::$CD
definition
func multEX_0 -> strict multLoopStr_0 equals
:: ALGSTR_1:def 8
multLoopStr_0 (# REAL, multreal,In(0,REAL),In(1,REAL) #);
end;
registration
cluster multEX_0 -> non empty;
end;
registration
cluster multEX_0 -> well-unital;
end;
definition
let IT be non empty multLoopStr_0;
attr IT is almost_invertible means
:: ALGSTR_1:def 9
(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
:: ALGSTR_1:def 10
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 :: ALGSTR_1:16
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;
registration
cluster multLoop_0-like -> almost_invertible almost_cancelable for non empty
multLoopStr_0;
end;
registration
cluster strict well-unital multLoop_0-like non degenerated for non empty
multLoopStr_0;
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;
end;
registration
cluster strict associative non degenerated for multLoop_0;
end;
definition
mode multGroup_0 is associative non degenerated multLoop_0;
end;
registration
cluster multEX_0 -> associative;
end;
registration
cluster strict commutative for multGroup_0;
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
x<>0.L;
redefine func x" means
:: ALGSTR_1:def 11
it*x = 1.L;
end;
reserve G for associative almost_invertible almost_cancelable well-unital non
empty multLoopStr_0;
reserve a,x for Element of G;
theorem :: ALGSTR_1:17
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 12
a*(b");
end;
:: from SCMRING1, 2010,02.06, A.T.
registration
cluster -> Abelian add-associative right_zeroed right_complementable
for 1-element addLoopStr;
cluster trivial -> well-unital right-distributive for
non empty doubleLoopStr;
end;
registration
cluster -> Group-like associative commutative for 1-element multMagma;
end;