:: Groups
:: by Wojciech A. Trybulec
::
:: Received July 3, 1990
:: Copyright (c) 1990-2017 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 NUMBERS, NAT_1, INT_1, XBOOLE_0, ALGSTR_0, SUBSET_1, BINOP_2,
RELAT_1, REAL_1, ARYTM_3, CARD_1, ARYTM_1, BINOP_1, STRUCT_0, FUNCT_1,
SETWISEO, FINSEQOP, ZFMISC_1, NEWTON, COMPLEX1, XXREAL_0, FINSET_1,
TARSKI, RLVECT_1, SUPINF_2, GROUP_1, ORDINAL1;
notations TARSKI, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, RELAT_1, FUNCT_1, XREAL_0, FUNCT_2, BINOP_2, BINOP_1, STRUCT_0,
ALGSTR_0, RLVECT_1, INT_1, NAT_1, FINSEQOP, SETWISEO, INT_2;
constructors BINOP_1, SETWISEO, XXREAL_0, REAL_1, NAT_1, NAT_D, BINOP_2,
FINSEQOP, RLVECT_1;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, INT_1,
STRUCT_0, ALGSTR_0, CARD_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve m,n for Nat;
reserve i,j for Integer;
reserve S for non empty multMagma;
reserve r,r1,r2,s,s1,s2,t,t1,t2 for Element of S;
definition
let IT be multMagma;
attr IT is unital means
:: GROUP_1:def 1
ex e being Element of IT st for h being
Element of IT holds h * e = h & e * h = h;
attr IT is Group-like means
:: GROUP_1:def 2
ex e being Element of IT st for h being
Element of IT holds h * e = h & e * h = h & ex g being Element of IT st h * g =
e & g * h = e;
attr IT is associative means
:: GROUP_1:def 3
for x,y,z being Element of IT holds (x*y )*z = x*(y*z);
end;
registration
cluster Group-like -> unital for multMagma;
end;
registration
cluster strict Group-like associative non empty for multMagma;
end;
definition
mode Group is Group-like associative non empty multMagma;
end;
theorem :: GROUP_1:1
((for r,s,t holds (r * s) * t = r * (s * t)) & ex t st for s1 holds s1
* t = s1 & t * s1 = s1 & ex s2 st s1 * s2 = t & s2 * s1 = t) implies S is Group
;
theorem :: GROUP_1:2
(for r,s,t holds r * s * t = r * (s * t)) & (for r,s holds (ex t st r
* t = s) & (ex t st t * r = s)) implies S is associative Group-like;
theorem :: GROUP_1:3
multMagma (# REAL, addreal #) is associative Group-like;
reserve G for Group-like non empty multMagma;
reserve e,h for Element of G;
definition
let G be multMagma such that
G is unital;
func 1_G -> Element of G means
:: GROUP_1:def 4
for h being Element of G holds h * it = h & it * h = h;
end;
theorem :: GROUP_1:4
(for h holds h * e = h & e * h = h) implies e = 1_G;
reserve G for Group;
reserve f,g,h for Element of G;
definition
let G,h;
func h" -> Element of G means
:: GROUP_1:def 5
h * it = 1_G & it * h = 1_G;
involutiveness;
end;
theorem :: GROUP_1:5
h * g = 1_G & g * h = 1_G implies g = h";
theorem :: GROUP_1:6
h * g = h * f or g * h = f * h implies g = f;
theorem :: GROUP_1:7
h * g = h or g * h = h implies g = 1_G;
theorem :: GROUP_1:8
(1_G)" = 1_G;
theorem :: GROUP_1:9
h" = g" implies h = g;
theorem :: GROUP_1:10
h" = 1_G implies h = 1_G;
::$CT
theorem :: GROUP_1:12
h * g = 1_G implies h = g" & g = h";
theorem :: GROUP_1:13
h * f = g iff f = h" * g;
theorem :: GROUP_1:14
f * h = g iff f = g * h";
theorem :: GROUP_1:15
ex f st g * f = h;
theorem :: GROUP_1:16
ex f st f * g = h;
theorem :: GROUP_1:17
(h * g)" = g" * h";
theorem :: GROUP_1:18
g * h = h * g iff (g * h)" = g" * h";
theorem :: GROUP_1:19
g * h = h * g iff g" * h" = h" * g";
theorem :: GROUP_1:20
g * h = h * g iff g * h" = h" * g;
reserve u for UnOp of G;
definition
let G;
func inverse_op(G) -> UnOp of G means
:: GROUP_1:def 6
it.h = h";
end;
registration
let G be associative non empty multMagma;
cluster the multF of G -> associative;
end;
theorem :: GROUP_1:21
for G being unital non empty multMagma holds 1_G is_a_unity_wrt
the multF of G;
theorem :: GROUP_1:22
for G being unital non empty multMagma holds the_unity_wrt the
multF of G = 1_G;
registration
let G be unital non empty multMagma;
cluster the multF of G -> having_a_unity;
end;
theorem :: GROUP_1:23
inverse_op(G) is_an_inverseOp_wrt the multF of G;
registration
let G;
cluster the multF of G -> having_an_inverseOp;
end;
theorem :: GROUP_1:24
the_inverseOp_wrt the multF of G = inverse_op(G);
definition
let G be non empty multMagma;
func power G -> Function of [:the carrier of G,NAT:], the carrier of G means
:: GROUP_1:def 7
for h being Element of G holds it.(h,0) = 1_G &
for n being Nat holds it.(h,n + 1) = it.(h,n) * h;
end;
definition
let G,h; let i be Integer;
func h |^ i -> Element of G equals
:: GROUP_1:def 8
power(G).(h,|.i.|) if 0 <= i
otherwise (power(G).(h,|.i.|))";
end;
definition
let G,h; let n be natural Number;
redefine func h |^ n equals
:: GROUP_1:def 9
power(G).(h,n);
end;
theorem :: GROUP_1:25
h |^ 0 = 1_G;
theorem :: GROUP_1:26
h |^ 1 = h;
theorem :: GROUP_1:27
h |^ 2 = h * h;
theorem :: GROUP_1:28
h |^ 3 = h * h * h;
theorem :: GROUP_1:29
h |^ 2 = 1_G iff h" = h;
theorem :: GROUP_1:30
i <= 0 implies h |^ i = (h |^ |.i.|)";
theorem :: GROUP_1:31
(1_G) |^ i = 1_G;
theorem :: GROUP_1:32
h |^ (-1) = h";
theorem :: GROUP_1:33
h |^ (i + j) = (h |^ i) * (h |^ j);
theorem :: GROUP_1:34
h |^ (i + 1) = h |^ i * h & h |^ (i + 1) = h * (h |^ i);
theorem :: GROUP_1:35
h |^ (i * j) = h |^ i |^ j;
theorem :: GROUP_1:36
h |^ -i = (h |^ i)";
theorem :: GROUP_1:37
h" |^ i = (h |^ i)";
theorem :: GROUP_1:38
g * h = h * g implies (g * h) |^ i = g |^ i * (h |^ i);
theorem :: GROUP_1:39
g * h = h * g implies g |^ i * (h |^ j) = h |^ j * (g |^ i);
theorem :: GROUP_1:40
g * h = h * g implies g * (h |^ i) = h |^ i * g;
definition
let G,h;
attr h is being_of_order_0 means
:: GROUP_1:def 10
h |^ n = 1_G implies n = 0;
end;
registration
let G;
cluster 1_G -> non being_of_order_0;
end;
definition
let G,h;
func ord h -> Element of NAT means
:: GROUP_1:def 11
it = 0 if h is being_of_order_0
otherwise
h |^ it = 1_G & it <> 0 & for m st h |^ m = 1_G & m <> 0 holds it <= m;
end;
theorem :: GROUP_1:41
h |^ ord h = 1_G;
theorem :: GROUP_1:42
ord 1_G = 1;
theorem :: GROUP_1:43
ord h = 1 implies h = 1_G;
theorem :: GROUP_1:44
h |^ n = 1_G implies ord h divides n;
definition
let G be finite 1-sorted;
redefine func card G -> Element of NAT;
end;
theorem :: GROUP_1:45
for G being non empty finite 1-sorted holds card G >= 1;
definition
let IT be multMagma;
attr IT is commutative means
:: GROUP_1:def 12
for x, y being Element of IT holds x*y = y*x;
end;
registration
cluster strict commutative for Group;
end;
definition
let FS be commutative non empty multMagma;
let x,y be Element of FS;
redefine func x*y;
commutativity;
end;
theorem :: GROUP_1:46
multMagma (# REAL, addreal #) is commutative Group;
reserve A for commutative Group;
reserve a,b for Element of A;
theorem :: GROUP_1:47
(a * b)" = a" * b";
theorem :: GROUP_1:48
(a * b) |^ i = a |^ i * (b |^ i);
theorem :: GROUP_1:49
addLoopStr (# the carrier of A, the multF of A, 1_A #) is Abelian
add-associative right_zeroed right_complementable;
begin :: Addenda
:: from COMPTRIG, 2006.08.12, A.T.
theorem :: GROUP_1:50
for L be unital non empty multMagma for x be Element of L holds
(power L).(x,1) = x;
theorem :: GROUP_1:51
for L be unital non empty multMagma for x be Element of L holds (power
L).(x,2) = x*x;
theorem :: GROUP_1:52
for L be associative commutative unital non empty multMagma for x,y be
Element of L for n be Nat holds (power L).(x*y,n) = (power L).(x,n)
* (power L).(y,n);
:: Moved from ENDALG, 17.01_2006, AK
definition
let G,H be multMagma;
let IT be Function of G,H;
attr IT is unity-preserving means
:: GROUP_1:def 13
IT.1_G = 1_H;
end;