:: Cyclic Groups and Some of Their Properties - Part I
:: by Dariusz Surowik
::
:: Received November 22, 1991
:: Copyright (c) 1991-2026 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, SUBSET_1, INT_1, GROUP_1, FINSEQ_1, XCMPLX_0, CARD_1,
XBOOLE_0, BINOP_2, FUNCT_1, BINOP_1, ARYTM_3, CARD_3, SETWISEO, RELAT_1,
TARSKI, NAT_1, SETWOP_2, FINSEQ_2, NEWTON, STRUCT_0, ORDINAL4, QC_LANG1,
GROUP_4, ARYTM_1, FINSET_1, XXREAL_0, GROUP_2, ALGSTR_0, ZFMISC_1,
REALSET1, REAL_1, INT_2, RLSUB_1, GRAPH_1, GR_CY_1, MEMBERED, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, RELAT_1, FUNCT_1, XREAL_0, FUNCT_2, FINSET_1, BINOP_1,
DOMAIN_1, INT_1, FINSEQ_1, FINSEQ_2, SETWISEO, SETWOP_2, BINOP_2,
REALSET1, INT_2, NAT_1, NAT_D, MEMBERED, RVSUM_1, XXREAL_0, STRUCT_0,
ALGSTR_0, GROUP_1, GROUP_2, GROUP_4;
constructors WELLORD2, BINOP_1, SETWISEO, XXREAL_0, REAL_1, NAT_1, NAT_D,
BINOP_2, FINSOP_1, SETWOP_2, RVSUM_1, REALSET1, GROUP_4, FUNCOP_1,
RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
INT_1, BINOP_2, MEMBERED, FINSEQ_1, REALSET1, STRUCT_0, GROUP_1, GROUP_2,
VALUED_0, ALGSTR_0, CARD_1, FINSEQ_2, ZFMISC_1, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions FUNCT_1, TARSKI, STRUCT_0, GROUP_1;
equalities BINOP_1, REALSET1, FINSEQ_2, FINSEQ_1, STRUCT_0, GROUP_2, GROUP_4,
SETWOP_2, ALGSTR_0, ORDINAL1;
expansions TARSKI, BINOP_1, STRUCT_0, GROUP_1;
theorems BINOP_1, INT_1, INT_2, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, ZFMISC_1,
FUNCT_2, FUNCOP_1, GROUP_1, GROUP_2, GROUP_4, TARSKI, FUNCT_1, CARD_1,
WELLORD2, FINSOP_1, RELSET_1, XBOOLE_0, RELAT_1, BINOP_2, NUMBERS,
SETWISEO, XREAL_1, XXREAL_0, ORDINAL1, RVSUM_1, SETWOP_2, FINSEQ_3,
NAT_D, STRUCT_0;
schemes BINOP_1, NAT_1, FINSEQ_1, FINSEQ_2;
begin
reserve i1 for Element of INT;
reserve j1,j2,j3 for Integer;
reserve p,s,k,n for Nat;
reserve x,y,xp,yp for set;
reserve G for Group;
reserve a,b for Element of G;
reserve F for FinSequence of G;
reserve I for FinSequence of INT;
Lm1: for n holds x in Segm (n) implies x is Element of NAT;
definition
redefine func addint means :: redefines addint (BINOP_2, definition)
for i1,i2 being Element of INT holds it.(i1,i2) = addreal.(i1,i2);
compatibility
proof
let b be BinOp of INT;
hereby
assume
A1: b = addint;
let i1,i2 be Element of INT;
thus b.(i1,i2) = i1 + i2 by A1,BINOP_2:def 20
.= addreal.(i1,i2) by BINOP_2:def 9;
end;
assume
A2: for i1,i2 being Element of INT holds b.(i1,i2) = addreal.(i1,i2);
now
let i1,i2 be Element of INT;
thus b.(i1,i2) = addreal.(i1,i2) by A2
.= i1 + i2 by BINOP_2:def 9
.= addint.(i1,i2) by BINOP_2:def 20;
end;
hence b = addint;
end;
end;
theorem
for i1 st i1 = 0 holds i1 is_a_unity_wrt addint by BINOP_2:4,SETWISEO:14;
theorem Th2:
Sum I = addint $$ I
proof
set g = addint, h = addcomplex;
set i = [#](I,the_unity_wrt g);
rng I c= COMPLEX by NUMBERS:11;
then reconsider f = I as FinSequence of COMPLEX by FINSEQ_1:def 4;
set j = [#](f,the_unity_wrt h);
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def 2;
A2: g $$ I = g $$ (finSeg n,i) & h $$ f = h $$ (finSeg n,j) by A1,
SETWOP_2:def 2;
defpred P[Nat] means g $$ (finSeg $1,i) = h $$ (finSeg $1,j);
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
set b = g $$(finSeg k,i);
set a = i.(k+1);
A5: not (k + 1) in Seg k by FINSEQ_3:8;
g $$ (finSeg (k+1),i) = g $$ (finSeg k \/ {. k+1 .},i) by FINSEQ_1:9
.= g.(b,a) by A5,SETWOP_2:2
.= b + a by BINOP_2:def 20
.= h.(h $$(finSeg k,j),j.(k+1)) by A4,BINOP_2:1,4,def 3
.= h $$ (finSeg k \/ {. k+1 .},j) by A5,SETWOP_2:2
.= h $$ (finSeg (k+1),j) by FINSEQ_1:9;
hence thesis;
end;
A6: Seg 0 = {}.NAT;
then g $$ (finSeg 0,[#](I,the_unity_wrt g)) = the_unity_wrt h by BINOP_2:1,4
,SETWISEO:31
.= h $$ (finSeg 0,[#](f,the_unity_wrt h)) by A6,SETWISEO:31;
then
A7: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A7,A3);
then g $$ I = h $$ f by A2;
hence thesis by RVSUM_1:def 10;
end;
definition
let I;
redefine func Sum(I) -> Element of INT equals :: redefines Sum (RVSUM_1, definition)
addint $$ I;
coherence
proof
Sum I = addint $$ I by Th2;
hence thesis;
end;
compatibility by Th2;
end;
theorem Th3:
Sum (<*> INT) = 0 by BINOP_2:4,FINSOP_1:10;
Lm2: Product(((len(<*> INT)) |->a)|^(<*> INT))=a|^Sum(<*> INT)
proof
(<*> the carrier of G)|^(<*> INT)=<*> the carrier of G by GROUP_4:21;
then Product((len(<*> INT)|->a)|^(<*> INT))=1_G by GROUP_4:8
.= a|^(Sum(<*> INT)) by Th3,GROUP_1:25;
hence thesis;
end;
Lm3: for I being FinSequence of INT
for w being Element of INT st
Product(((len I)|->a)|^I)=a|^Sum I holds
Product(((len (I^<*w*>))|->a)|^(I^<*w*>))=a|^Sum(I^<*w*>)
proof
let I;
let w be Element of INT;
assume
A1: Product(((len I)|->a)|^I)=a|^Sum I;
A2: len((len I) |->a) =len I by CARD_1:def 7;
A3: len <*a*> = 1 by FINSEQ_1:40
.= len <*w*> by FINSEQ_1:40;
Product(((len (I^<*w*>))|->a)|^(I^<*w*>)) =Product(((len I+1)|->a)|^(I^
<*w*>)) by FINSEQ_2:16
.= Product((((len I)|->a)^<*a*>)|^(I^<*w*>)) by FINSEQ_2:60
.= Product((((len I)|->a)|^I)^(<*a*>|^<*w*>)) by A2,A3,GROUP_4:19
.= Product((((len I)|->a)|^I))*Product(<*a*>|^<*@(@w)*>) by GROUP_4:5
.= Product((((len I)|->a)|^I))*Product(<*a|^(@w)*>) by GROUP_4:22
.= (a|^Sum I)*(a|^(@w)) by A1,FINSOP_1:11
.= a|^(Sum I+@w) by GROUP_1:33
.= a|^Sum(I^<*w*>) by RVSUM_1:74;
hence thesis;
end;
theorem Th4:
for I being FinSequence of INT holds Product(((len I)|->a)|^I) = a|^Sum I
proof
defpred P[FinSequence of INT] means Product(((len $1) |->a)|^($1))=a|^Sum($1
);
A1: for p being FinSequence of INT for x being Element of INT st P[p] holds
P[p^<*x*>] by Lm3;
A2: P[<*> INT] by Lm2;
for p being FinSequence of INT holds P[p] from FINSEQ_2:sch 2(A2,A1);
hence thesis;
end;
:: Finite groups and their some properties
theorem Th5:
b in gr {a} iff ex j1 st b=a|^j1
proof
A1: (ex j1 st b=a|^j1) implies b in gr {a}
proof
given j1 such that
A2: b =a|^j1;
consider n being Nat such that
A3: j1 = n or j1 = -n by INT_1:2;
per cases by A3;
suppose
A4: j1=n;
ex F,I st len F = len I & rng F c= {a} & Product(F |^ I) = b
proof
take F =(n |-> a);
A5: len F = n by CARD_1:def 7
.= len(n |->@ 1) by CARD_1:def 7;
Product(F|^(n |->@ 1)) = Product(F|^(len F |->@ 1)) by CARD_1:def 7
.=Product(n |-> a) by GROUP_4:25
.=b by A2,A4,GROUP_4:12;
hence thesis by A5,FUNCOP_1:13;
end;
hence thesis by GROUP_4:28;
end;
suppose
j1 = -n;
then
A6: b"=a|^(-(-n)) by A2,GROUP_1:36
.= a|^n;
ex F,I st len F = len I & rng F c= {a} & Product(F |^ I) = b"
proof
take F =(n |-> a);
A7: len F = n by CARD_1:def 7
.= len(n |->@ 1) by CARD_1:def 7;
Product(F|^(n |->@ 1)) = Product(F|^(len F |->@ 1)) by CARD_1:def 7
.=Product(n |-> a) by GROUP_4:25
.= b" by A6,GROUP_4:12;
hence thesis by A7,FUNCOP_1:13;
end;
then b" in gr {a} by GROUP_4:28;
then b"" in gr {a} by GROUP_2:51;
hence thesis;
end;
end;
b in gr {a} implies ex j1 st b=a|^j1
proof
assume b in gr {a};
then consider F,I such that
A8: len F = len I and
A9: rng F c= {a} and
A10: Product(F |^ I ) = b by GROUP_4:28;
take Sum I;
A11: for p be Nat st p in dom F holds F.p = ((len F)|-> a).p
proof
let p be Nat;
A12: dom F = Seg len F by FINSEQ_1:def 3;
assume
A13: p in dom F;
then F.p in rng F by FUNCT_1:def 3;
then F.p = a by A9,TARSKI:def 1
.= ((len F)|-> a).p by A12,A13,FUNCOP_1:7;
hence thesis;
end;
dom ((len F) |-> a) = Seg len F by FUNCOP_1:13
.= dom F by FINSEQ_1:def 3;
then b= Product(((len I) |-> a)|^I) by A8,A10,A11,FINSEQ_1:13
.= a|^Sum I by Th4;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th6:
for G being finite Group, a being Element of G holds
a is not being_of_order_0
proof
let G be finite Group, a be Element of G;
ex n st n<> 0 & a|^n = 1_G
proof
deffunc F(Nat) = a|^$1;
consider F being FinSequence such that
A1: len F = card G +1 and
A2: for p be Nat st p in dom F holds F.p = F(p) from FINSEQ_1:sch 2;
A3: dom F = Seg (card G + 1) by A1,FINSEQ_1:def 3;
A4: for y st y in rng F holds ex n st y=a|^n
proof
let y;
assume y in rng F;
then consider x being object such that
A5: x in dom F and
A6: F.x=y by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A5;
take n;
thus thesis by A2,A5,A6;
end;
for x being object holds x in rng F implies x in the carrier of G
proof
let y be object;
assume y in rng F;
then ex n st y= a|^n by A4;
hence thesis;
end;
then rng F c= the carrier of G;
then reconsider
F9=F as Function of Seg (card G +1),the carrier of G by A3,FUNCT_2:def 1
,RELSET_1:4;
A7: card G < card G +1 by XREAL_1:29;
card Segm card G = card the carrier of G &
card Seg(card G+1) = card Segm(card G +1) by FINSEQ_1:55;
then card the carrier of G in card Seg (card G +1) by A7,NAT_1:41;
then consider x,y being object such that
A8: x in Seg (card G +1) and
A9: y in Seg (card G +1) and
A10: x <> y and
A11: F9.x = F9.y by FINSEQ_4:65;
reconsider p=x,n=y as Element of NAT by A8,A9;
per cases by A10,XXREAL_0:1;
suppose
A12: n>p;
then reconsider t = n-p as Element of NAT by INT_1:5;
take t;
F9.p =a|^p by A2,A3,A8;
then a|^n=a|^p by A2,A3,A9,A11;
then a|^(n+-p)=a|^p *a|^(-p) by GROUP_1:33;
then a|^t =a|^(p+-p) by GROUP_1:33;
hence thesis by A12,GROUP_1:25;
end;
suppose
A13: p>n;
then reconsider t = p-n as Element of NAT by INT_1:5;
take t;
F9.p =a|^p by A2,A3,A8;
then a|^n=a|^p by A2,A3,A9,A11;
then a|^(p+-n)=a|^n *a|^(-n) by GROUP_1:33;
then a|^t =a|^(n+-n) by GROUP_1:33;
hence thesis by A13,GROUP_1:25;
end;
end;
hence thesis;
end;
theorem Th7:
for G being finite Group, a being Element of G holds ord a = card gr {a}
proof
let G be finite Group, a be Element of G;
deffunc F(Nat) = a|^$1;
consider F being FinSequence such that
A1: len F = ord a and
A2: for p be Nat st p in dom F holds F.p = F(p) from FINSEQ_1:sch 2;
A3: dom F = Seg ord a by A1,FINSEQ_1:def 3;
A4: for y st y in rng F holds ex n st y=a|^n
proof
let y;
assume y in rng F;
then consider x being object such that
A5: x in dom F and
A6: F.x=y by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A5;
take n;
thus thesis by A2,A5,A6;
end;
for x being object st x in rng F holds x in the carrier of gr {a}
proof
let y be object;
assume y in rng F;
then ex n st y= a|^n by A4;
then y in gr {a} by Th5;
hence thesis;
end;
then
A7: rng F c= the carrier of gr {a};
a is not being_of_order_0 by Th6;
then
A8: ord a <> 0 by GROUP_1:def 11;
A9: ex x st x in dom F & F.x=a
proof
set x9=1;
(ord a)+x9 > 0+x9 by A8,XREAL_1:6;
then (ord a) >= x9 by NAT_1:13;
then
A10: x9 in dom F by A3;
then F.x9=a|^x9 by A2
.=a by GROUP_1:26;
hence thesis by A10;
end;
then
A11: a in rng F by FUNCT_1:def 3;
the carrier of gr {a} c= rng F
proof
ex H being strict Subgroup of G st the carrier of H = rng F
proof
reconsider car=rng F as non empty set by A9,FUNCT_1:def 3;
the carrier of gr {a} c= the carrier of G by GROUP_2:def 5;
then
A12: car c= the carrier of G by A7;
dom(the multF of G)= [:the carrier of G,the carrier of G:] by
FUNCT_2:def 1;
then
A13: dom((the multF of G)||car)=[:car,car:] by A12,RELAT_1:62,ZFMISC_1:96;
for y being object st y in rng((the multF of G)||car) holds y in car
proof
let y be object;
set f=(the multF of G)||car;
assume y in rng(f);
then consider x being object such that
A14: x in dom(f) and
A15: f.x=y by FUNCT_1:def 3;
consider xp,yp being object such that
A16: [xp,yp]=x by A13,A14,RELAT_1:def 1;
yp in car by A13,A14,A16,ZFMISC_1:87;
then consider s such that
A17: yp = a|^s by A4;
xp in car by A13,A14,A16,ZFMISC_1:87;
then consider p such that
A18: xp = a|^p by A4;
A19: ex x st x in dom F & F.x=a|^(p+s)
proof
set t=(p+s) mod (ord a);
A20: t < ord a by A8,NAT_D:1;
per cases;
suppose
A21: t=0;
take ord a;
a |^(p+s)=a|^((ord a)*((p+s) div (ord a)) + ((p+s) mod (ord a
))) by A8,NAT_D:2
.=a|^((ord a)*((p+s) div (ord a)))*(a|^ ((p+s) mod (ord a)))
by GROUP_1:33
.=a|^(ord a)|^((p+s) div (ord a))*(a|^ ((p+s) mod (ord a))) by
GROUP_1:35
.=(1_G)|^((p+s) div (ord a))*(a|^ ((p+s) mod (ord a))) by
GROUP_1:41
.=(1_G) *(a|^ ((p+s) mod (ord a))) by GROUP_1:31
.=a|^0 by A21,GROUP_1:def 4
.= 1_G by GROUP_1:25
.= a|^(ord a) by GROUP_1:41
.= F.ord a by A2,A3,A8,FINSEQ_1:3;
hence thesis by A3,A8,FINSEQ_1:3;
end;
suppose
t>0;
then t+1 > 0+1 by XREAL_1:6;
then t >= 1 by NAT_1:13;
then
A22: t in dom F by A3,A20;
take t;
a|^(p+s)=a|^((ord a)*((p+s) div (ord a)) + ((p+s) mod (ord a)
)) by A8,NAT_D:2
.=a|^((ord a)*((p+s) div (ord a))) *(a|^ ((p+s) mod (ord a)))
by GROUP_1:33
.=a|^(ord a)|^((p+s) div (ord a)) *(a|^ ((p+s) mod (ord a)))
by GROUP_1:35
.=(1_G)|^((p+s) div (ord a)) *(a|^ ((p+s) mod (ord a))) by
GROUP_1:41
.=(1_G) *(a|^ ((p+s) mod (ord a))) by GROUP_1:31
.=a|^ ((p+s) mod (ord a)) by GROUP_1:def 4;
hence thesis by A2,A22;
end;
end;
y = a|^p*(a|^s) by A14,A15,A16,A18,A17,FUNCT_1:47
.= a|^(p+s) by GROUP_1:33;
hence thesis by A19,FUNCT_1:def 3;
end;
then rng((the multF of G)||car) c= car;
then reconsider op=(the multF of G)||car as BinOp of car by A13,
FUNCT_2:def 1,RELSET_1:4;
set H=multMagma(#car,op#);
A23: for f,g being Element of H, f9,g9 being Element of G st f = f9 & g
= g9 holds f9*g9 = f*g
proof
let f,g be Element of H;
let f9,g9 be Element of G;
A24: f*g = ((the multF of G)||car).[f,g];
assume f = f9 & g =g9;
hence thesis by A24,FUNCT_1:49;
end;
A25: ex e being Element of H st for h being Element of H holds h * e = h
& e * h = h & ex g being Element of H st h * g = e & g * h = e
proof
ex x st x in dom F & F.x=a|^(ord a)
proof
set x9=(ord a);
F.x9=a|^x9 by A2,A3,A8,FINSEQ_1:3;
hence thesis by A3,A8,FINSEQ_1:3;
end;
then a|^(ord a) in car by FUNCT_1:def 3;
then reconsider e=1_G as Element of H by GROUP_1:41;
take e;
for h being Element of H holds h * e = h & e * h = h & ex g being
Element of H st h * g = e & g * h = e
proof
let h be Element of H;
reconsider h9=h as Element of G by A12;
h*e = h9 *(1_G) by A23
.= h9 by GROUP_1:def 4;
hence h * e = h;
e*h = (1_G)*h9 by A23
.= h9 by GROUP_1:def 4;
hence e * h = h;
thus ex g being Element of H st h * g = e & g * h = e
proof
ex n st h=a|^n & 1 <= n & ord a >= n
proof
consider x being object such that
A26: x in dom F and
A27: F.x=h by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A26;
take n;
thus thesis by A2,A3,A26,A27,FINSEQ_1:1;
end;
then consider n such that
A28: h=a|^n and
A29: ord a >= n;
ex x st x in dom F & F.x =a|^(ord a - n)
proof
per cases by A29,XXREAL_0:1;
suppose
A30: ord a = n;
set x = ord a;
F.x=a|^x by A2,A3,A8,FINSEQ_1:3
.= 1_G by GROUP_1:41
.= a|^(ord a - n) by A30,GROUP_1:25;
hence thesis by A3,A8,FINSEQ_1:3;
end;
suppose
A31: ord a > n;
then reconsider x = ord a - n as Element of NAT by INT_1:5;
take x;
x in Seg ord a
proof
set r1 = ord a;
r1 <= r1 + n by NAT_1:11;
then
A32: x <= r1 by XREAL_1:20;
r1 - n > n -n by A31,XREAL_1:9;
then x >= 0 +1 by NAT_1:13;
hence thesis by A32;
end;
hence thesis by A2,A3;
end;
end;
then reconsider g =a|^(ord a - n) as Element of H by FUNCT_1:def 3;
A33: n+(ord a-n) =ord a;
A34: g * h =a|^(ord a - n) * (a|^n) by A23,A28
.=a|^(ord a) by A33,GROUP_1:33
.= e by GROUP_1:41;
h * g =a|^n *(a|^(ord a - n)) by A23,A28
.=a|^(ord a) by A33,GROUP_1:33
.= e by GROUP_1:41;
hence thesis by A34;
end;
end;
hence thesis;
end;
for f,g,h being Element of H holds (f * g) * h = f * (g * h)
proof
let f,g,h be Element of H;
reconsider f9=f,g9=g,h9=h as Element of G by A12;
A35: g * h = g9 * h9 by A23;
f9*g9 = f*g by A23;
then (f*g)*h =(f9*g9)*h9 by A23
.= f9*(g9*h9) by GROUP_1:def 3
.=f*(g*h) by A23,A35;
hence thesis;
end;
then reconsider H1=H as Group by A25,GROUP_1:1;
the carrier of gr {a} c= the carrier of G by GROUP_2:def 5;
then the carrier of H1 c= the carrier of G by A7;
then H1 is Subgroup of G by GROUP_2:def 5;
hence thesis;
end;
then consider H being strict Subgroup of G such that
A36: the carrier of H = rng F;
{a} c= the carrier of H by A11,A36,ZFMISC_1:31;
then gr {a} is Subgroup of H by GROUP_4:def 4;
hence thesis by A36,GROUP_2:def 5;
end;
then
A37: rng F = the carrier of gr {a} by A7,XBOOLE_0:def 10;
reconsider So = Seg ord a as finite set;
set ca = the carrier of gr {a};
F is one-to-one
proof
let x,y be object;
assume that
A38: x in dom F and
A39: y in dom F and
A40: F.x = F.y and
A41: x<>y;
reconsider s=y as Element of NAT by A39;
reconsider p=x as Element of NAT by A38;
A42: F.p=a|^p & F.s=a|^s by A2,A38,A39;
reconsider s9=s,p9=p,z= ord a as Real;
per cases;
suppose
p<=s;
then reconsider r1=s-p as Element of NAT by INT_1:5;
p >0 by A3,A38,FINSEQ_1:1;
then
A43: z<z+p9 by XREAL_1:29;
s9<=z by A3,A39,FINSEQ_1:1;
then s9<z+p9 by A43,XXREAL_0:2;
then
A44: s9-p9<z+p9-p9 by XREAL_1:9;
1_G=a|^s*(a|^p)" by A40,A42,GROUP_1:def 5;
then a|^0=a|^s*(a|^p)" by GROUP_1:25;
then a|^0=a|^s*(a|^(-p)) by GROUP_1:36;
then a|^0=a|^(s+(-p)) by GROUP_1:33;
then
A45: 1_G=a|^r1 by GROUP_1:25;
r1 <> 0 & a is not being_of_order_0 by A41,Th6;
hence thesis by A45,A44,GROUP_1:def 11;
end;
suppose
s<=p;
then reconsider r2=p-s as Element of NAT by INT_1:5;
s >0 by A3,A39,FINSEQ_1:1;
then
A46: z<z+s9 by XREAL_1:29;
p9<=z by A3,A38,FINSEQ_1:1;
then p9<z+s9 by A46,XXREAL_0:2;
then
A47: p9-s9<z+s9-s9 by XREAL_1:9;
1_G=a|^p*(a|^s)" by A40,A42,GROUP_1:def 5;
then a|^0=a|^p*(a|^s)" by GROUP_1:25;
then a|^0=a|^p*(a|^(-s)) by GROUP_1:36;
then a|^0=a|^(p+(-s)) by GROUP_1:33;
then
A48: 1_G=a|^r2 by GROUP_1:25;
r2 <> 0 & a is not being_of_order_0 by A41,Th6;
hence thesis by A48,A47,GROUP_1:def 11;
end;
end;
then Seg ord a,the carrier of gr {a} are_equipotent by A3,A37,WELLORD2:def 4;
then card So = card ca by CARD_1:5;
hence thesis by FINSEQ_1:57;
end;
theorem Th8:
for G being finite Group, a being Element of G holds ord a divides card G
proof
let G be finite Group, a be Element of G;
ord a = card gr {a} by Th7;
hence thesis by GROUP_2:148;
end;
theorem Th9:
for G being finite Group, a being Element of G holds a|^card G = 1_G
proof
let G be finite Group, a be Element of G;
ord a divides card G by Th8;
then consider t being Nat such that
A1: card G = ord a * t by NAT_D:def 3;
a|^card G = a |^ ord a |^ t by A1,GROUP_1:35
.= (1_G) |^ t by GROUP_1:41
.= 1_G by GROUP_1:31;
hence thesis;
end;
theorem Th10:
for G being finite Group, a being Element of G holds
(a|^n)" = a|^(card G - (n mod card G))
proof
let G be finite Group;
let a be Element of G;
set q = card G;
set p9 = n mod q;
n mod q <=q by NAT_D:1;
then reconsider q9=q -( n mod q) as Element of NAT by INT_1:5;
a|^n*(a|^(q-(n mod q)))=a|^(n+q9) by GROUP_1:33
.= a|^((q*(n div q)+(n mod q))+q9) by NAT_D:2
.= a|^(q*(n div q)+q +(-p9+p9))
.= a|^(q*(n div q)+q)*(a|^(-p9+p9)) by GROUP_1:33
.= a|^(q*(n div q)+q)*(a|^(-p9)*(a|^p9)) by GROUP_1:33
.= a|^(q*(n div q)+q)*((a|^p9)"*(a|^p9)) by GROUP_1:36
.= a|^(q*(n div q)+q)*(1_G) by GROUP_1:def 5
.= a|^(q*(n div q+1)) by GROUP_1:def 4
.= a|^q|^(n div q+1) by GROUP_1:35
.= (1_G)|^(n div q+1) by Th9
.= 1_G by GROUP_1:31;
hence thesis by GROUP_1:12;
end;
registration
let G be Group;
cluster the multMagma of G -> Group-like;
coherence
proof
set H = the multMagma of G;
reconsider e = 1_G as Element of H;
take e;
let h be Element of H;
reconsider h9 = h as Element of G;
thus h * e = h9 * 1_G .= h by GROUP_1:def 4;
thus e * h = 1_G * h9 .= h by GROUP_1:def 4;
reconsider g = h9" as Element of H;
take g;
thus h * g = h9 * h9" .= e by GROUP_1:def 5;
thus g * h = h9" * h9 .= e by GROUP_1:def 5;
end;
end;
theorem Th11:
for G being strict finite Group st card G > 1
ex a being Element of G st a <> 1_G
proof
let G be strict finite Group;
assume that
A1: card G > 1 and
A2: for a being Element of G holds a = 1_G;
for a being Element of G holds a in (1).G
proof
let a be Element of G;
a = 1_G by A2;
then a in {1_G} by TARSKI:def 1;
hence thesis by GROUP_2:def 7;
end;
then the multMagma of G = (1).G by GROUP_2:62;
hence contradiction by A1,GROUP_2:69;
end;
theorem
for G being strict finite Group st card G = p & p is prime holds for H
being strict Subgroup of G holds H = (1).G or H = G
proof
let G be strict finite Group;
assume that
A1: card G = p and
A2: p is prime;
let H be strict Subgroup of G;
card H divides p by A1,GROUP_2:148;
then card H = 1 or card H = p by A2,INT_2:def 4;
hence thesis by A1,GROUP_2:70,73;
end;
definition
func INT.Group -> non empty strict multMagma equals
multMagma(#INT,addint#);
coherence;
end;
registration
cluster INT.Group -> associative Group-like;
coherence
proof
set G = INT.Group;
reconsider e=0 as Element of G by INT_1:def 2;
thus for h,g,f being Element of G holds (h * g) * f = h * (g * f)
proof
let h,g,f be Element of G;
reconsider A=h,B = g, C = f as Integer;
A1: g * f = B + C by BINOP_2:def 20;
h * g = A + B by BINOP_2:def 20;
hence (h * g) * f = A + B + C by BINOP_2:def 20
.= A + (B + C)
.= h * (g * f) by A1,BINOP_2:def 20;
end;
take e;
let h be Element of G;
reconsider A = h as Integer;
-A in INT by INT_1:def 2;
then reconsider g = - A as Element of G;
thus h * e = A + 0 by BINOP_2:def 20
.= h;
thus e * h = 0 + A by BINOP_2:def 20
.= h;
take g;
thus h * g = A + (- A) by BINOP_2:def 20
.= e;
thus g * h = (- A) + A by BINOP_2:def 20
.= e;
end;
end;
registration
cluster the carrier of INT.Group -> integer-membered;
coherence;
end;
registration
let a,b be Element of INT.Group;
identify a*b with a+b;
compatibility by BINOP_2:def 20;
end;
registration
let n be natural Number;
cluster Segm n -> natural-membered;
coherence;
end;
definition
let n be natural Number such that
A1: n > 0;
func addint(n) -> BinOp of Segm(n) means
:Def4:
for k,l being Element of Segm(n) holds it.(k,l) = (k+l) mod n;
existence
proof
reconsider n as non zero Nat by A1,TARSKI:1;
defpred P[Nat,Nat,set] means $3 = ($1+$2) mod n;
A2: for k,l being Element of Segm(n) ex c being Element of Segm(n) st P[k, l,c]
proof
let k,l be Element of Segm(n);
(k+l) mod n < n by NAT_D:1;
then reconsider c = (k+l) mod n as Element of Segm(n) by NAT_1:44;
take c;
thus thesis;
end;
ex o being BinOp of Segm n st for a,b being Element of Segm n holds P[
a,b,o.(a,b)] from BINOP_1:sch 3(A2);
hence thesis;
end;
uniqueness
proof
let i1,i2 be BinOp of Segm(n) such that
A3: for k,l being Element of Segm(n) holds i1.(k,l)=((k+l) mod n) and
A4: for k,l being Element of Segm(n) holds i2.(k,l)=((k+l) mod n);
for k,l being Element of Segm(n) holds i1.(k,l)=i2.(k,l)
proof
let k,l be Element of Segm(n);
thus i1.(k,l)=((k+l) mod n) by A3
.=i2.(k,l) by A4;
end;
hence thesis;
end;
end;
definition
let n be non zero Nat;
func INT.Group(n) -> non empty strict multMagma equals
multMagma(#Segm(n),addint(n)#);
coherence;
end;
registration
let n be non zero Nat;
cluster INT.Group(n) -> finite associative Group-like;
coherence
proof
set G = INT.Group(n);
thus the carrier of INT.Group(n) is finite;
reconsider e=0 as Element of G by NAT_1:44;
thus for h,g,f being Element of G holds (h * g) * f = h * (g * f)
proof
let h,g,f be Element of G;
reconsider A = h, B = g, C = f as Element of Segm(n);
A1: g * f = (B + C) mod n by Def4;
h * g = (A + B) mod n by Def4;
hence (h * g) * f = (((A + B) mod n) + C) mod n by Def4
.= ((A + B) + C) mod n by NAT_D:22
.= (A + (B + C)) mod n
.= (A + ((B + C) mod n)) mod n by NAT_D:22
.= h * (g * f) by A1,Def4;
end;
take e;
let h be Element of G;
reconsider A = h as Element of Segm(n);
A2: A < n by NAT_1:44;
then consider p being Nat such that
A3: n=A+p by NAT_1:10;
thus h * e = (A + 0) mod n by Def4
.= h by A2,NAT_D:24;
thus e * h = (0 + A) mod n by Def4
.= h by A2,NAT_D:24;
(p mod n) < n by NAT_D:1;
then reconsider g = p mod n as Element of G by NAT_1:44;
reconsider B=g as Element of Segm(n);
take g;
A4: p <= n by A3,NAT_1:12;
thus h * g =e
proof
per cases by A4,XXREAL_0:1;
suppose
A5: p = n;
h * g = (A +B) mod n by Def4
.= (0 * n) mod n by A3,A5,NAT_D:25
.= e;
hence thesis;
end;
suppose
A6: p < n;
h * g = (A +B) mod n by Def4
.= n mod n by A3,A6,NAT_D:24
.= e by NAT_D:25;
hence thesis;
end;
end;
thus g * h = e
proof
per cases by A4,XXREAL_0:1;
suppose
p = n;
then g * h = (n mod n + 0) mod n by A3,Def4
.= (0 * n) mod n by NAT_D:25
.= e;
hence thesis;
end;
suppose
A7: p < n;
g * h = (A + B) mod n by Def4
.= n mod n by A3,A7,NAT_D:24
.= e by NAT_D:25;
hence thesis;
end;
end;
end;
end;
theorem Th13:
1_INT.Group = 0
proof
reconsider e = 0 as Element of INT.Group by INT_1:def 2;
for h being Element of INT.Group holds h * e = h & e * h = h;
hence thesis by GROUP_1:4;
end;
theorem Th14:
for n be non zero Nat holds 1_INT.Group(n) = 0
proof
let n be non zero Nat;
reconsider e = 0 as Element of Segm(n) by NAT_1:44;
reconsider e as Element of INT.Group(n);
for h being Element of INT.Group(n) holds h * e = h & e * h = h
proof
let h be Element of INT.Group(n);
reconsider A = h as Element of Segm(n);
reconsider A as Element of NAT;
A1: A < n by NAT_1:44;
A2: e * h = (0 + A) mod n by Def4
.= h by A1,NAT_D:24;
h * e = (A + 0) mod n by Def4
.= h by A1,NAT_D:24;
hence thesis by A2;
end;
hence thesis by GROUP_1:4;
end;
definition
let h be Integer;
func @'h -> Element of INT.Group equals
h;
coherence by INT_1:def 2;
end;
theorem Th15:
for h being Element of INT.Group holds h" = -h
proof
let h be Element of INT.Group;
-h in INT by INT_1:def 2;
then reconsider g=-h as Element of INT.Group;
h * g =1_INT.Group by Th13;
hence thesis by GROUP_1:12;
end;
Lm4: (@'1) |^ k = k
proof
defpred P[Nat] means (@'1)|^$1=$1;
A1: for k st P[k] holds P[k+1]
proof
let k;
assume (@'1)|^k = k;
then (@'1)|^k * (@'1) = k + 1;
hence thesis by GROUP_1:34;
end;
A2: P[0] by Th13,GROUP_1:25;
for k holds P[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th16:
j1 = (@'1) |^ j1
proof
consider k being Nat such that
A1: j1 = k or j1 = -k by INT_1:2;
per cases by A1;
suppose
j1=k;
hence thesis by Lm4;
end;
suppose
A2: j1=-k;
reconsider k9=k as Integer;
reconsider k9 as Element of INT.Group by INT_1:def 2;
(@'1)|^j1 = ((@'1)|^k)" by A2,GROUP_1:36
.= (k9)" by Lm4
.= j1 by A2,Th15;
hence thesis;
end;
end;
:: Definition of cyclic group
Lm5: INT.Group = gr {@'1}
proof
reconsider h = 1 as Element of INT by INT_1:def 2;
reconsider h as Element of INT.Group;
for G1 being Subgroup of INT.Group
st {h} c= the carrier of G1 holds (Omega). INT.Group is Subgroup of G1
proof
let G1 be Subgroup of INT.Group;
assume
A1: {h} c= the carrier of G1;
the carrier of (Omega).INT.Group c= the carrier of G1
proof
h in {h} by TARSKI:def 1;
then reconsider h99=h as Element of G1 by A1;
let x be object;
assume that
A2: x in the carrier of (Omega).INT.Group and
A3: not x in the carrier of G1;
reconsider x9=x as Integer by A2;
(h99)|^x9 in the carrier of G1 & (h99)|^x9=h|^x9 by GROUP_4:2;
hence contradiction by A3,Th16;
end;
hence thesis by GROUP_2:57;
end;
then for G1 being strict Subgroup of INT.Group st {h} c= the carrier of G1
holds (Omega).INT.Group is Subgroup of G1;
hence thesis by GROUP_4:def 4;
end;
definition
let IT be Group;
attr IT is cyclic means :Def7:
ex a being Element of IT st the multMagma of IT = gr {a};
end;
registration
cluster strict cyclic non trivial infinite for Group;
existence
proof
take INT.Group;
thus thesis by Lm5;
end;
end;
registration
let G be Group;
cluster (1).G -> cyclic;
coherence
proof
1_G in {1_G} by TARSKI:def 1;
then reconsider PG=1_G as Element of (1).G by GROUP_2:def 7;
take PG;
for G1 being Subgroup of (1).G st {PG} c= the carrier of G1 holds
(Omega).(1).G is Subgroup of G1
proof
let G1 be Subgroup of (1).G;
assume {PG} c= the carrier of G1;
then the carrier of (Omega).(1).G c=the carrier of G1 by GROUP_2:def 7;
hence thesis by GROUP_2:57;
end;
then for G1 being strict Subgroup of (1). G st {PG} c= the carrier of G1
holds (Omega).(1).G is Subgroup of G1;
hence thesis by GROUP_4:def 4;
end;
end;
registration
cluster strict finite trivial cyclic for Group;
existence
proof
take G = (1).the Group;
the carrier of G = {1_(the Group)} by GROUP_2:def 7; then
the carrier of G is trivial;
hence thesis;
end;
end;
theorem Th17:
G is cyclic Group iff ex a being Element of G st
for b being Element of G ex j1 st b=a|^j1
proof
thus G is cyclic Group implies ex a being Element of G st for b being
Element of G ex j1 st b=a|^j1
proof
assume G is cyclic Group;
then consider a being Element of G such that
A1: the multMagma of G = gr {a} by Def7;
take a;
for b being Element of G ex j1 st b=a|^j1 by A1,Th5,STRUCT_0:def 5;
hence thesis;
end;
given a being Element of G such that
A2: for b being Element of G ex j1 st b = a|^j1;
for b being Element of G holds b in gr {a}
proof
let b be Element of G;
ex j1 st b=a|^j1 by A2;
hence thesis by Th5;
end;
then the multMagma of G = gr {a} by GROUP_2:62;
hence thesis by Def7;
end;
theorem Th18:
for G being finite Group holds
G is cyclic iff ex a being Element of G st
for b being Element of G ex n st b = a|^n
proof
let G be finite Group;
thus G is cyclic implies ex a being Element of G st for b being Element of G
ex n st b=a|^n
proof
assume G is cyclic;
then consider a being Element of G such that
A1: for b being Element of G ex j2 st b=a|^j2 by Th17;
take a;
let b be Element of G;
consider j2 such that
A2: b = a|^j2 by A1;
consider n being Nat such that
A3: j2=n or j2=-n by INT_1:2;
per cases by A3;
suppose
j2=n;
hence thesis by A2;
end;
suppose
A4: j2=-n;
n mod card G <=card G by NAT_D:1;
then reconsider q9=card G -( n mod card G) as Element of NAT by INT_1:5;
take q9;
b=(a|^n)" by A2,A4,GROUP_1:36
.= a|^q9 by Th10;
hence thesis;
end;
end;
given a being Element of G such that
A5: for b being Element of G ex n st b=a|^n;
for b being Element of G ex j2 st b=a|^j2
proof
let b be Element of G;
consider n such that
A6: b=a|^n by A5;
reconsider n as Integer;
take n;
thus thesis by A6;
end;
hence thesis by Th17;
end;
theorem Th19:
for G being finite Group holds
( G is cyclic iff ex a being Element of G st ord a = card G )
proof
let G be finite Group;
thus G is cyclic implies ex a being Element of G st ord a = card G
proof
reconsider H = the multMagma of G as Group;
assume G is cyclic;
then consider a being Element of G such that
A1: the multMagma of G = gr {a};
take a;
ord a = card H by A1,Th7;
hence thesis;
end;
given a being Element of G such that
A2: ord a = card G;
ex a being Element of G st the multMagma of G = gr {a}
proof
consider a being Element of G such that
A3: ord a = card G by A2;
take a;
card gr {a} = card G by A3,Th7;
hence thesis by GROUP_2:73;
end;
hence thesis;
end;
theorem
for G being finite Group, H being strict Subgroup of G st G is cyclic
holds H is cyclic
proof
let G be finite Group, H be strict Subgroup of G;
A1: card H >= 1 by GROUP_1:45;
assume G is cyclic;
then consider a be Element of G such that
A2: for b being Element of G ex n st b = a|^n by Th18;
per cases by A1,XXREAL_0:1;
suppose
card H = 1;
then H = (1).G by GROUP_2:70;
hence thesis;
end;
suppose
A3: card H > 1;
defpred P[Nat] means $1 > 0 & a|^$1 is Element of H;
consider h being Element of H such that
A4: h <> 1_H by A3,Th11;
h is Element of G by GROUP_2:42;
then consider n such that
A5: h = a|^n by A2;
n <> 0
proof
assume n = 0;
then h = 1_G by A5,GROUP_1:25
.= 1_H by GROUP_2:44;
hence contradiction by A4;
end;
then
A6: ex n being Nat st P[n] by A5;
ex h1 being Element of H st for b being Element of H ex s st b = h1|^ s
proof
ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:
sch 5(A6);
then consider n being Nat such that
A7: n>0 and
A8: a|^n is Element of H and
A9: for k be Nat st k>0 & a|^k is Element of H holds n <= k;
consider h1 being Element of H such that
A10: h1 = a|^n by A8;
take h1;
for b being Element of H ex s st b = h1|^s
proof
let b be Element of H;
b is Element of G by GROUP_2:42;
then consider p such that
A11: b = a|^p by A2;
consider s,r being Nat such that
A12: p = (n*s) + r and
A13: r < n by A7,NAT_1:17;
reconsider s,r as Element of NAT by ORDINAL1:def 12;
take s;
r =0
proof
h1|^s=a|^n|^s by A10,GROUP_4:1;
then (h1|^s)"=(a|^n|^s)" by GROUP_2:48
.= (a|^(n * s ))" by GROUP_1:35;
then reconsider g= (a|^(n*s))" as Element of H;
reconsider b=a|^p as Element of H by A11;
a|^p = a|^(n*s) * (a|^r) by A12,GROUP_1:33;
then (a|^(n*s))" * (a|^p) = ((a|^(n*s))" *(a|^(n*s)))*(a|^r) by
GROUP_1:def 3
.= 1_G *(a|^r) by GROUP_1:def 5
.= a|^ r by GROUP_1:def 4;
then
A14: g*b = a|^r by GROUP_2:43;
assume r<>0;
hence contradiction by A9,A13,A14;
end;
then a|^p = a|^n|^s by A12,GROUP_1:35
.= h1|^s by A10,GROUP_4:1;
hence thesis by A11;
end;
hence thesis;
end;
hence thesis by Th18;
end;
end;
theorem
for G being strict finite Group st card G is prime holds G is cyclic
proof
let G be strict finite Group;
assume A1: card G is prime;
set p = card G;
ex a being Element of G st ord a = p
proof
assume
A2: for a being Element of G holds ord a <> p;
A3: now
let a be Element of G;
ord a divides p by Th8;
then ord a = 1 or ord a = p by A1,INT_2:def 4;
hence ord a = 1 by A2;
end;
for x being object
holds x in the carrier of G implies x in the carrier of (1).G
proof
let x be object;
assume x in the carrier of G;
then reconsider x9=x as Element of G;
ord x9 = 1 by A3;
then x9 = 1_G by GROUP_1:43;
then x9 in {1_G} by TARSKI:def 1;
hence thesis by GROUP_2:def 7;
end;
then the carrier of G c= the carrier of (1).G;
then G = (1).G by GROUP_2:61;
then card G = 1 by GROUP_2:69;
hence contradiction by A1,INT_2:def 4;
end;
hence thesis by Th19;
end;
theorem Th22:
for n being non zero Nat
ex g being Element of INT.Group(n) st
for b being Element of INT.Group(n) ex j1 st b = g|^j1
proof
let n be non zero Nat;
0+1 < n+1 by XREAL_1:6;
then
A1: n >=1 by NAT_1:13;
now
per cases by A1,XXREAL_0:1;
suppose
n=1;
then the carrier of INT.Group(n) = {1_INT.Group(n)} by Th14,CARD_1:49
.= the carrier of (1).INT.Group(n) by GROUP_2:def 7;
then INT.Group(n) = (1).INT.Group(n) by GROUP_2:61;
hence thesis by Th17;
end;
suppose
n>1;
then reconsider g9= 1 as Element of Segm(n) by NAT_1:44;
reconsider g=g9 as Element of INT.Group(n);
for b being Element of INT.Group(n) ex j1 st b = g|^j1
proof
let b be Element of INT.Group(n);
reconsider b9=b as Element of NAT by Lm1;
defpred P[Nat] means g|^$1 = $1 mod n;
A2: b9<n by NAT_1:44;
A3: for k st P[k] holds P[k+1]
proof
let k;
assume
A4: g|^k = k mod n;
k mod n < n by NAT_D:1;
then reconsider e=(k mod n) as Element of Segm(n) by NAT_1:44;
g|^(k+1) =g|^k*(g|^1) by GROUP_1:33
.=g|^k*g by GROUP_1:26
.= (e +g9) mod n by A4,Def4
.=(k+1) mod n by NAT_D:22;
hence thesis;
end;
g|^0 = 1_INT.Group(n) by GROUP_1:25
.= 0 by Th14
.= 0 mod n by NAT_D:26;
then
A5: P[0];
for k holds P[k] from NAT_1:sch 2(A5,A3);
then
A6: g|^b9=b9 mod n .= b by A2,NAT_D:24;
reconsider b9 as Integer;
take b9;
thus thesis by A6;
end;
hence thesis;
end;
end;
hence thesis;
end;
registration
cluster cyclic -> commutative for Group;
coherence
proof
let G;
assume
A1: G is cyclic;
for a,b being Element of G holds a * b = b * a
proof
let a,b be Element of G;
ex e being Element of G st ex j2 st a=e|^j2 & ex j3 st b=e|^j3
proof
consider e being Element of G such that
A2: for d being Element of G ex j3 st d=e|^j3 by A1,Th17;
take e;
( ex j2 st a=e|^j2)& ex j3 st b=e|^j3 by A2;
hence thesis;
end;
then consider e being Element of G,j2,j3 such that
A3: a = e|^j2 & b = e|^j3;
a * b = e |^(j3 + j2) by A3,GROUP_1:33
.= b * a by A3,GROUP_1:33;
hence thesis;
end;
hence thesis;
end;
end;
theorem
INT.Group = gr {@'1} by Lm5;
registration
cluster INT.Group -> cyclic;
coherence by Lm5;
end;
registration
let n be non zero Nat;
cluster INT.Group(n) -> cyclic;
coherence
proof
ex g being Element of INT.Group(n) st for b being Element of INT.Group(n)
ex j1 st b = g|^j1 by Th22;
hence thesis by Th17;
end;
end;