Copyright (c) 1991 Association of Mizar Users
environ
vocabulary INT_1, REALSET1, FINSEQ_1, NAT_1, ORDINAL2, ARYTM, BINOP_1,
FUNCT_1, VECTSP_1, QC_LANG1, SETWISEO, RLVECT_1, FINSEQ_2, GROUP_1,
GROUP_4, RELAT_1, ARYTM_1, FUNCOP_1, FINSET_1, CARD_1, GROUP_2, TARSKI,
ARYTM_3, FILTER_0, RLSUB_1, GRAPH_1, GR_CY_1, CARD_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL2, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, REAL_1, FUNCT_2, SETWISEO, CARD_1,
FINSET_1, BINOP_1, DOMAIN_1, INT_1, INT_2, NAT_1, RLVECT_1, GROUP_2,
STRUCT_0, VECTSP_1, GROUP_1, GROUP_4, FUNCOP_1, FINSOP_1, SETWOP_2,
FINSEQ_1;
constructors WELLORD2, REAL_1, SETWISEO, DOMAIN_1, NAT_1, FUNCSDOM, GROUP_4,
FINSOP_1, NAT_LAT, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, CARD_1, INT_1, GROUP_1, GROUP_2, RELSET_1,
STRUCT_0, FINSEQ_1, ARYTM_3, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0,
ORDINAL2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions GROUP_1, SETWISEO, FUNCT_1, BINOP_1, VECTSP_1, TARSKI;
theorems AXIOMS, BINOP_1, INT_1, INT_2, NAT_1, REAL_1, FINSEQ_1, FINSEQ_2,
FINSEQ_4, VECTSP_1, ZFMISC_1, FUNCT_2, FUNCOP_1, GROUP_1, GROUP_2,
GROUP_4, TARSKI, FUNCT_1, CARD_1, WELLORD2, RLVECT_1, FINSOP_1, RELSET_1,
XREAL_0, ORDINAL2, XBOOLE_0, XBOOLE_1, SQUARE_1, RELAT_1, XCMPLX_0,
XCMPLX_1;
schemes BINOP_1, NAT_1, FINSEQ_1, FINSEQ_2;
begin
reserve i1,i2,i3 for Element of INT;
reserve j1,j2,j3 for Integer;
reserve p,s,r,g,k,n,m,q,t 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 the carrier of G;
reserve I for FinSequence of INT;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Some properties of modulo function ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem Th1:
m mod n = (n*k + m) mod n
proof
per cases by NAT_1:18;
suppose A1: n > 0;
m mod n = t implies (n*k + m) mod n = t
proof
assume m mod n = t;
then consider q such that A2: m = n * q + t & t < n by A1,NAT_1:def 2;
ex g st n*k + m = n*g + t & t < n
proof
take k + q;
n*k + m = (n*k + n*q) + t & t < n by A2,XCMPLX_1:1;
hence thesis by XCMPLX_1:8;
end;
hence thesis by NAT_1:def 2;
end;
hence thesis;
suppose n = 0;
hence thesis;
end;
theorem Th2:
(p+s) mod n = ((p mod n)+s) mod n
proof
per cases by NAT_1:18;
suppose n > 0;
then (p + s) mod n = (n*(p div n) + (p mod n) + s) mod n by NAT_1:47
.=(n*(p div n) + ((p mod n) + s)) mod n by XCMPLX_1:1
.=((p mod n) + s) mod n by Th1;
hence thesis;
suppose
A1: n = 0;
hence (p+s) mod n = 0 by NAT_1:def 2
.= ((p mod n)+s) mod n by A1,NAT_1:def 2;
end;
theorem
(p+s) mod n = (p + ( s mod n)) mod n by Th2;
theorem Th4:
k < n implies k mod n = k
proof
assume A1:k<n;
ex p st k=n*p + k & k<n
proof
k=n*0 + k;
hence thesis by A1;
end;
hence thesis by NAT_1:def 2;
end;
theorem Th5:
n mod n = 0
proof
per cases by NAT_1:18;
suppose A1:n>0;
ex p st n=n*p +0 & 0<n
proof
n=n*1+0;
hence thesis by A1;
end;
hence thesis by NAT_1:def 2;
suppose n = 0;
hence thesis by NAT_1:def 2;
end;
theorem Th6:
0 = 0 mod n
proof
n = 0 or n > 0 by NAT_1:18;
hence thesis by Th4,NAT_1:def 2;
end;
definition let n be natural number such that A1:n > 0;
func Segm (n) -> non empty Subset of NAT equals
:Def1: {p: p<n};
coherence
proof
set X={p:p<n};
0 in X by A1;
then reconsider X as non empty set;
X c= NAT
proof
for x holds x in X implies x in NAT
proof
let x be set;
assume x in X;
then ex p being Element of NAT st p=x & p<n;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis;
end;
end;
Lm1:
for n st n > 0 holds x in Segm (n) implies x is Nat;
canceled 3;
theorem Th10:
for n,s being natural number st n > 0 holds s in Segm (n) iff s < n
proof
let n,s be natural number;
assume A1: n>0;
A2: s is Nat by ORDINAL2:def 21;
s in { p : p<n } iff ex p st s=p & p<n;
hence thesis by A1,A2,Def1;
end;
canceled;
theorem
for n being natural number st n > 0 holds 0 in Segm (n) by Th10;
theorem Th13:
Segm (1) = {0}
proof
now let x;
thus x in Segm(1) implies x in { 0 }
proof assume A1:x in Segm(1);
Segm(1) = { p : p < 1 } by Def1;
then consider p such that
A2:x = p & (p < 1) by A1;
p < 0 + 1 by A2;
then p <= 0 by NAT_1:38;
then p = 0 by NAT_1:18;
hence thesis by A2,TARSKI:def 1;
end;
assume x in { 0 };
then x = 0 by TARSKI:def 1;
hence x in Segm(1) by Th10;
end;
hence Segm(1) = { 0 } by TARSKI:2;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Definition addint ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
func addint -> BinOp of INT means:
Def2: for i1,i2 being Element of INT holds
it.(i1,i2) = addreal.(i1,i2);
existence
proof
defpred P[Element of INT, Element of INT,set] means $3 = addreal.($1,$2);
A1:for i1,i2 being Element of INT ex c being Element of INT st P[i1,i2,c]
proof
let i1,i2 be Element of INT;
reconsider i1' = i1, i2' = i2 as Integer;
reconsider c = i1'+i2' as Element of INT by INT_1:12;
take c;
i1 is Element of REAL & i2 is Element of REAL by XREAL_0:def 1;
hence thesis by VECTSP_1:def 4;
end;
ex B being BinOp of INT st for i1,i2 being Element of INT holds
P[i1,i2,B.(i1,i2)] from BinOpEx(A1);
hence thesis;
end;
uniqueness
proof
let f1,f2 be BinOp of INT such that
A2:for i1,i2 being Element of INT holds
f1.(i1,i2)=addreal.(i1,i2) and
A3:for i1,i2 being Element of INT holds
f2.(i1,i2)=addreal.(i1,i2);
for i1,i2 being Element of INT holds f1.(i1,i2)=f2.(i1,i2)
proof
let i1,i2 be Element of INT;
thus f1.(i1,i2)=addreal.(i1,i2) by A2 .=f2.(i1,i2) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th14:
for j1,j2 holds addint.(j1,j2)=j1+j2
proof
let j1,j2;
reconsider j1'=j1,j2'=j2 as Element of INT by INT_1:12;
A1:j1 is Element of REAL & j2 is Element of REAL by XREAL_0:def 1;
thus addint.(j1,j2)=addreal.(j1',j2') by Def2
.=j1+j2 by A1,VECTSP_1:def 4;
end;
theorem Th15:
for i1 st i1 = 0 holds i1 is_a_unity_wrt addint
proof
let i1;
assume A1:i1=0;
A2: for i2 holds addint.(i1,i2) = i2
proof let i2;
reconsider e=i1 as Integer;
addint.(e,i2) =addint.(e,@i2) by GROUP_4:def 2
.= e +@i2 by Th14
.= i2 by A1,GROUP_4:def 2;
hence thesis;
end;
for i2 holds addint.(i2,i1) = i2
proof
let i2;
reconsider e=i1 as Integer;
addint.(i2,e) =addint.(@i2,e)by GROUP_4:def 2
.= @i2 + e by Th14
.= i2 by A1,GROUP_4:def 2;
hence thesis;
end;
hence i1 is_a_unity_wrt addint by A2,BINOP_1:11;
end;
theorem Th16:
the_unity_wrt addint = 0
proof
reconsider zero=0 as Element of INT by INT_1:12;
zero is_a_unity_wrt addint by Th15;
hence thesis by BINOP_1:def 8;
end;
theorem Th17:
addint has_a_unity
proof reconsider O = 0 as Element of INT by INT_1:12;
take O; thus thesis by Th15;
end;
theorem
addint is commutative
proof let i1,i2;
thus addint.(i1,i2) = addint.(@i1,i2) by GROUP_4:def 2
.= addint.(@i1,@i2) by GROUP_4:def 2
.= @i2 + (@i1) by Th14
.= addint.(@i2,@i1) by Th14
.= addint.(i2,@i1) by GROUP_4:def 2
.= addint.(i2,i1) by GROUP_4:def 2;
end;
theorem
addint is associative
proof let i1,i2,i3;
thus addint.(i1,addint.(i2,i3))
= addint.(@i1,addint.(i2,i3)) by GROUP_4:def 2
.= addint.(@i1,addint.(@i2,i3)) by GROUP_4:def 2
.= addint.(@i1,addint.(@i2,@i3)) by GROUP_4:def 2
.= addint.(@i1,@i2+@i3) by Th14
.= @i1+(@i2+@i3) by Th14
.= @i1+@i2+@i3 by XCMPLX_1:1
.= addint.((@i1+@i2),@i3) by Th14
.= addint.(addint.(@i1,@i2),@i3) by Th14
.= addint.(addint.(@i1,@i2),i3) by GROUP_4:def 2
.= addint.(addint.(@i1,i2),i3) by GROUP_4:def 2
.= addint.(addint.(i1,i2),i3) by GROUP_4:def 2;
end;
definition let F be FinSequence of INT;
func Sum(F) -> Integer equals
:Def3: addint $$ F;
coherence;
end;
theorem Th20:
Sum(I^<*i1*>) =Sum I +@i1
proof
thus Sum(I^<*i1*>) = addint $$ (I^<*i1*>) by Def3
.= addint.(addint $$ I,i1) by Th17,FINSOP_1:5
.= addint.(Sum I,i1) by Def3
.= addint.(Sum I,@i1) by GROUP_4:def 2
.= Sum I + @i1 by Th14;
end;
theorem
Sum <*i1*> = i1
proof set F = <*i1*>;
thus Sum F = addint $$ F by Def3 .= i1 by FINSOP_1:12;
end;
theorem Th22:
Sum (<*> INT) = 0
proof set F = <*> INT;
thus Sum F = addint $$ F by Def3
.= 0 by Th16,Th17,FINSOP_1:11;
end;
Lm2: Product(((len(<*> INT)) |->a)|^(<*> INT))=a|^Sum(<*> INT)
proof
A1:(<*> the carrier of G)|^(<*> INT)=<*> the carrier of G by GROUP_4:27;
len(<*> INT)|->a =0 |-> a by FINSEQ_1:32 .=<*> the carrier of G by FINSEQ_2:
72
;
then Product((len(<*> INT)|->a)|^(<*> INT))=1.G by A1,GROUP_4:11 .=
a|^(Sum(<*> INT)) by Th22,GROUP_1:59;
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;
A1:@(@w) =@(w) by GROUP_4:def 2 .=w by GROUP_4:def 2;
assume A2:Product(((len I)|->a)|^I)=a|^Sum I;
A3:len((len I) |->a) =len I by FINSEQ_2:69;
A4:len <*a*> = 1 by FINSEQ_1:57 .= len <*w*> by FINSEQ_1:57;
Product(((len (I^<*w*>))|->a)|^(I^<*w*>))
=Product(((len I+1)|->a)|^(I^<*w*>)) by FINSEQ_2:19
.= Product((((len I)|->a)^<*a*>)|^(I^<*w*>)) by FINSEQ_2:74
.= Product((((len I)|->a)|^I)^(<*a*>|^<*w*>)) by A3,A4,GROUP_4:25
.= Product((((len I)|->a)|^I))*Product(<*a*>|^<*@(@w)*>) by A1,GROUP_4:8
.= Product((((len I)|->a)|^I))*Product(<*a|^(@w)*>) by GROUP_4:28
.= (a|^Sum I)*(a|^(@w)) by A2,GROUP_4:12
.= a|^(Sum I+@w) by GROUP_1:63
.= a|^Sum(I^<*w*>) by Th20;
hence thesis;
end;
canceled;
theorem Th24:
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: P[<*> INT] by Lm2;
A2: for p being FinSequence of INT for x being Element of INT
st P[p] holds P[p^<*x*>] by Lm3;
for p being FinSequence of INT holds P[p] from IndSeqD(A1,A2);
hence thesis;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Finite groups and their some properties ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem Th25:
b in gr {a} iff ex j1 st b=a|^j1
proof
A1:b in gr {a} implies ex j1 st b=a|^j1
proof
assume b in gr {a};
then consider F,I such that A2: len F = len I and
A3: rng F c= {a} and A4: Product(F |^ I ) = b by GROUP_4:37;
A5:dom ((len F) |-> a) = Seg len F by FINSEQ_2:68
.= dom F by FINSEQ_1:def 3;
for p st p in dom F holds F.p = ((len F)|-> a).p
proof
let p;
A6: dom F = Seg len F by FINSEQ_1:def 3;
assume A7: p in dom F;
then F.p in rng F by FUNCT_1:def 5;
then F.p = a by A3,TARSKI:def 1 .= ((len F)|-> a).p by A6,A7,FINSEQ_2:70;
hence thesis;
end;
then A8: b= Product(((len I) |-> a)|^I) by A2,A4,A5,FINSEQ_1:17
.= a|^Sum I by Th24;
take Sum I;
thus thesis by A8;
end;
(ex j1 st b=a|^j1) implies b in gr {a}
proof
given j1 such that A9: b =a|^j1;
consider n such that A10: j1 = n or j1 = -n by INT_1:8;
now per cases by A10;
suppose A11:j1=n;
ex F,I st len F = len I & rng F c= {a} & Product(F |^ I) = b
proof
take F =(n |-> a);
A12: len F = n by FINSEQ_2:69 .= len(n |->@ 1) by FINSEQ_2:69;
F = Seg n --> a by FINSEQ_2:def 2;
then A13: rng F c= {a} by FUNCOP_1:19;
Product(F|^(n |->@ 1)) = Product(F|^(len F |->@ 1)) by FINSEQ_2:69
.=Product(n |-> a) by GROUP_4:31
.=b by A9,A11,GROUP_4:15;
hence thesis by A12,A13;
end;
hence thesis by GROUP_4:37;
suppose j1 = -n;
then A14: b"=a|^(-(-n)) by A9,GROUP_1:70 .= a|^n;
ex F,I st len F = len I & rng F c= {a} & Product(F |^ I) = b"
proof
take F =(n |-> a);
A15: len F = n by FINSEQ_2:69 .= len(n |->@ 1) by FINSEQ_2:69;
F = Seg n --> a by FINSEQ_2:def 2;
then A16: rng F c= {a} by FUNCOP_1:19;
Product(F|^(n |->@ 1)) = Product(F|^(len F |->@ 1)) by FINSEQ_2:69
.=Product(n |-> a) by GROUP_4:31 .= b" by A14,GROUP_4:15;
hence thesis by A15,A16;
end;
then b" in gr {a} by GROUP_4:37;
then b"" in gr {a} by GROUP_2:60;
hence thesis by GROUP_1:19;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th26:
G is finite implies a is_not_of_order_0
proof
assume A1:G is finite;
ex n st n<> 0 & a|^n = 1.G
proof
deffunc F(Nat) = a|^$1;
consider F being FinSequence such that A2: len F = ord G +1 and
A3: for p st p in Seg (ord G +1) holds F.p = F(p) from SeqLambda;
A4: dom F = Seg (ord G + 1) by A2,FINSEQ_1:def 3;
A5: 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 such that A6: x in dom F and A7: F.x=y by FUNCT_1:def 5;
reconsider n=x as Nat by A6;
take n;
thus thesis by A3,A4,A6,A7;
end;
rng F c= the carrier of G
proof
for x holds x in rng F implies x in the carrier of G
proof
let y;
assume y in rng F;
then ex n st y= a|^n by A5;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
then reconsider F'=F as Function of Seg (ord G +1),the carrier of G by A4,
FUNCT_2:def 1,RELSET_1:11;
consider c being finite set such that
A8: c = the carrier of G & ord G = card c by A1,GROUP_1:def 14;
A9:Card ord G = Card the carrier of G by A8,CARD_1:def 11;
A10:Card Seg(ord G+1) = Card (ord G +1) by FINSEQ_1:76;
ord G < ord G +1 by REAL_1:69;
then Card the carrier of G <` Card Seg (ord G +1) by A9,A10,CARD_1:73;
then consider x,y such that A11:x in Seg (ord G +1) and A12:y in
Seg (ord G +1)
and A13:x <> y and A14: F'.x = F'.y by FINSEQ_4:80;
reconsider p=x,n=y as Nat by A11,A12;
now per cases by A13,REAL_1:def 5;
suppose A15: n>p;
then reconsider t = n-p as Nat by INT_1:18;
reconsider e=0 as Integer;
take t;
A16: t <>0 by A15,SQUARE_1:11;
F'.p =a|^p by A3,A11;
then a|^n=a|^p by A3,A12,A14;
then a|^(n+-p)=a|^p *a|^(-p) by GROUP_1:64;
then a|^(n+-p)=a|^(p+-p) by GROUP_1:64;
then a|^t =a|^(p+-p) by XCMPLX_0:def 8;
then a|^t=a|^e by XCMPLX_0:def 6;
then a|^t=1.G by GROUP_1:59;
hence thesis by A16;
suppose A17: p>n;
then reconsider t = p-n as Nat by INT_1:18;
take t;
reconsider e=0 as Integer;
A18: t <>0 by A17,SQUARE_1:11;
F'.p =a|^p by A3,A11;
then a|^n=a|^p by A3,A12,A14;
then a|^(p+-n)=a|^n *a|^(-n) by GROUP_1:64;
then a|^(p+-n)=a|^(n+-n) by GROUP_1:64;
then a|^t =a|^(n+-n) by XCMPLX_0:def 8;
then a|^t=a|^e by XCMPLX_0:def 6;
then a|^t=1.G by GROUP_1:59;
hence thesis by A18;
end;
hence thesis;
end;
hence thesis by GROUP_1:def 10;
end;
theorem Th27:
G is finite implies ord a = ord gr {a}
proof
assume A1:G is finite;
then A2:gr {a} is finite by GROUP_2:48;
deffunc F(Nat) = a|^$1;
consider F being FinSequence such that A3: len F = ord a and
A4: for p st p in Seg ord a holds F.p = F(p) from SeqLambda;
A5: dom F = Seg ord a by A3,FINSEQ_1:def 3;
a is_not_of_order_0 by A1,Th26;
then A6:ord a <> 0 by GROUP_1:def 11;
then A7:ord a >0 by NAT_1:19;
A8: a in rng F
proof
ex x st x in dom F & F.x=a
proof
set x'=1;
A9:x' in dom F
proof
(ord a)+x' > 0+x' by A7,REAL_1:53;
then (ord a) >= x' by NAT_1:38;
hence thesis by A5,FINSEQ_1:3;
end;
then F.x'=a|^x' by A4,A5 .=a by GROUP_1:44;
hence thesis by A9;
end;
hence thesis by FUNCT_1:def 5;
end;
A10: rng F = the carrier of gr {a}
proof
A11: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 such that A12: x in dom F and A13: F.x=y by FUNCT_1:def 5
;
reconsider n=x as Nat by A12;
take n;
thus thesis by A4,A5,A12,A13;
end;
A14: rng F c= the carrier of gr {a}
proof
for x holds x in rng F implies x in the carrier of gr {a}
proof
let y;
assume y in rng F;
then consider n such that A15:y= a|^n by A11;
y in gr {a} by A15,Th25;
hence thesis by RLVECT_1:def 1;
end;
hence thesis by TARSKI:def 3;
end;
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 A8;
A16:dom(the mult of G)=
[:the carrier of G,the carrier of G:] by FUNCT_2:def 1;
the carrier of gr {a} c= the carrier of G by GROUP_2:def 5;
then A17: car c= the carrier of G by A14,XBOOLE_1:1;
then [:car,car:] c= [:the carrier of G,the carrier of G:] by ZFMISC_1:119
;
then A18:dom((the mult of G)|[:car,car:])=[:car,car:] by A16,RELAT_1:91;
rng((the mult of G)|[:car,car:]) c= car
proof
for y st y in rng((the mult of G)|[:car,car:]) holds y in car
proof
set f=(the mult of G)|[:car,car:];
let y;
assume y in rng(f);
then consider x such that A19:x in dom(f) and
A20: f.x=y by FUNCT_1:def 5;
consider xp,yp such that A21:[xp,yp]=x
by A18,A19,ZFMISC_1:102;
xp in car by A18,A19,A21,ZFMISC_1:106;
then consider p such that A22: xp = a|^p by A11;
yp in car by A18,A19,A21,ZFMISC_1:106;
then consider s such that A23: yp = a|^s by A11;
A24: y = (the mult of G).[a|^p,a|^s]
by A19,A20,A21,A22,A23,FUNCT_1:70
.= (the mult of G).(a|^p,a|^s) by BINOP_1:def 1
.= a|^p*(a|^s) by VECTSP_1:def 10
.= a|^(p+s) by GROUP_1:48;
a|^(p+s) in car
proof
ex x st x in dom F & F.x=a|^(p+s)
proof
per cases by NAT_1:18;
suppose A25:p+s=0;
A26:ord a in dom F by A5,A6,FINSEQ_1:5;
A27:a|^(p+s)=1.G by A25,GROUP_1:43
.= a|^(ord a) by GROUP_1:82 .= F.ord a by A4,A5,A26;
take ord a;
thus thesis by A5,A6,A27,FINSEQ_1:5;
suppose p+s>0;
thus thesis
proof
set t=(p+s) mod (ord a);
A28:t < ord a by A7,NAT_1:46;
now per cases by NAT_1:18;
suppose A29:t=0;
A30:ord a in dom F by A5,A6,FINSEQ_1:5;
A31:a|^(p+s)=a|^((ord a)*((p+s) div (ord a)) + ((p+s) mod (ord a))) by A7,
NAT_1:47
.=a|^((ord a)*((p+s) div (ord a)))*(a|^ ((p+s) mod (ord a))) by GROUP_1:48
.=a|^(ord a)|^((p+s) div (ord a))*(a|^ ((p+s) mod (ord a))) by GROUP_1:50
.=(1.G)|^((p+s) div (ord a))*(a|^ ((p+s) mod (ord a))) by GROUP_1:82
.=(1.G) *(a|^ ((p+s) mod (ord a))) by GROUP_1:42
.=a|^0 by A29,GROUP_1:def 4 .= 1.G by GROUP_1:43
.= a|^(ord a) by GROUP_1:82 .= F.ord a by A4,A5,A30;
take x = ord a;
thus x in dom F & F.x=a|^(p+s) by A5,A6,A31,FINSEQ_1:5;
suppose t>0;
then t+1 > 0+1 by REAL_1:53;
then A32:t >= 1 by NAT_1:38;
take x = t;
A33:t in dom F by A5,A28,A32,FINSEQ_1:3;
a|^(p+s)=a|^((ord a)*((p+s) div (ord a)) + ((p+s) mod (ord a))) by A7,NAT_1
:47
.=a|^((ord a)*((p+s) div (ord a))) *(a|^ ((p+s) mod (ord a))) by GROUP_1:48
.=a|^(ord a)|^((p+s) div (ord a)) *(a|^ ((p+s) mod (ord a))) by GROUP_1:50
.=(1.G)|^((p+s) div (ord a)) *(a|^ ((p+s) mod (ord a))) by GROUP_1:82
.=(1.G) *(a|^ ((p+s) mod (ord a))) by GROUP_1:42
.=a|^ ((p+s) mod (ord a)) by GROUP_1:def 4;
hence x in dom F & F.x=a|^(p+s) by A4,A5,A33;
end;
hence thesis;
end;
thus thesis;
end;
hence thesis by FUNCT_1:def 5;
end;
hence thesis by A24;
end;
hence thesis by TARSKI:def 3;
end;
then reconsider op=(the mult of G)|[:car,car:] as BinOp of car by A18,FUNCT_2:
def 1,RELSET_1:11;
set H=HGrStr(#car,op#);
H is Group
proof
A34: for f,g being Element of H ,
f',g' being Element of G
st f = f' & g = g' holds f'*g' = f*g
proof
let f,g be Element of H;
let f' ,g' be Element of G;
assume A35: f = f' & g =g';
set A = [:car,car:];
A36:f*g = ((the mult of G) | A).(f,g) by VECTSP_1:def 10
.= ((the mult of G) | A).[f,g] by BINOP_1:def 1;
f'*g' = (the mult of G).(f',g') by VECTSP_1:def 10
.= (the mult of G).[f',g'] by BINOP_1:def 1;
hence thesis by A35,A36,FUNCT_1:72;
end;
A37: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 f'=f as Element of G by A17,TARSKI:def 3;
reconsider g'=g as Element of G by A17,TARSKI:def 3;
reconsider h'=h as Element of G by A17,TARSKI:def 3;
A38: f'*g' = f*g by A34;
A39: g * h = g' * h' by A34;
(f*g)*h =(f'*g')*h' by A34,A38 .= f'*(g'*h') by VECTSP_1:def 16
.=f*(g*h) by A34,A39;
hence thesis;
end;
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
a|^(ord a) in car
proof
ex x st x in dom F & F.x=a|^(ord a)
proof
set x'=(ord a);
A40: x' in Seg ord a by A6,FINSEQ_1:5;
then F.x'=a|^x' by A4;
hence thesis by A5,A40;
end;
hence thesis by FUNCT_1:def 5;
end;
then reconsider e=1.G as Element of H by GROUP_1:82;
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 h'=h as Element of G by A17,TARSKI:def 3;
thus h * e = h
proof
h*e = h' *(1.G) by A34 .= h' by GROUP_1:def 4;
hence thesis;
end;
thus e * h = h
proof
e*h = (1.G)*h' by A34 .= h' by GROUP_1:def 4;
hence thesis;
end;
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 such that A41: x in dom F and A42: F.x=h by FUNCT_1:def 5;
reconsider n=x as Nat by A41;
take n;
thus thesis by A4,A5,A41,A42,FINSEQ_1:3;
end;
then consider n such that A43:h=a|^n and A44: ord a >= n;
a|^(ord a - n) in car
proof
ex x st x in dom F & F.x =a|^(ord a - n)
proof
per cases by A44,REAL_1:def 5;
suppose ord a = n;
then A45: ord a - n =0 by XCMPLX_1:14;
set x = ord a;
A46: x in dom F by A5,A6,FINSEQ_1:5;
then F.x=a|^x by A4,A5 .= 1.G by GROUP_1:82
.= a|^(ord a - n) by A45,GROUP_1:43;
hence thesis by A46;
suppose A47:ord a > n;
then reconsider x = ord a - n as Nat by INT_1:18;
take x;
x in Seg ord a
proof
reconsider r1=ord a ,r2=n as Real;
A48:x >= 1
proof
r1 - r2 > r2 -r2 by A47,REAL_1:54;
then r1-r2 > 0 by XCMPLX_1:14;
then x >= 0 +1 by NAT_1:38;
hence x >= 1;
end;
x <= ord a
proof
r1 <= r1 + r2 by NAT_1:29;
hence thesis by REAL_1:86;
end;
hence thesis by A48,FINSEQ_1:3;
end;
hence thesis by A3,A4,FINSEQ_1:def 3;
end;
hence thesis by FUNCT_1:def 5;
end;
then reconsider g =a|^(ord a - n) as Element of H;
A49:n+(ord a-n) =ord a
proof
reconsider n'=n ,z = ord a as Integer;
reconsider n''=n' ,z' =z as Real;
n+(ord a-n) = (z' + n'') - n'' by XCMPLX_1:29
.= z' + (n'' - n'') by XCMPLX_1:29 .= z'+0 by XCMPLX_1:14
.= z';
hence thesis;
end;
A50: h * g = e
proof
h * g =a|^n *(a|^(ord a - n)) by A34,A43
.=a|^(ord a) by A49,GROUP_1:64
.= e by GROUP_1:82;
hence thesis;
end;
g * h = e
proof
g * h =a|^(ord a - n) * (a|^n) by A34,A43
.=a|^(ord a) by A49,GROUP_1:65
.= e by GROUP_1:82;
hence thesis;
end;
hence thesis by A50;
end;
thus thesis;
end;
hence thesis;
end;
hence thesis by A37,GROUP_1:5;
end;
then reconsider H1=H as Group;
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 A14,XBOOLE_1:1;
then H1 is Subgroup of G by GROUP_2:def 5;
hence thesis;
end;
then consider H being strict Subgroup of G such that
A51: the carrier of H = rng F;
{a} c= the carrier of H by A8,A51,ZFMISC_1:37;
then gr {a} is Subgroup of H by GROUP_4:def 5;
hence the carrier of gr {a} c= rng F by A51,GROUP_2:def 5;
end;
hence thesis by A14,XBOOLE_0:def 10;
end;
F is one-to-one
proof
let x,y;
assume that A52: x in dom F and A53: y in dom F and A54: F.x = F.y
and A55:x<>y;
reconsider p=x as Nat by A52;
reconsider s=y as Nat by A53;
reconsider s'=s,p'=p,z= ord a as Real;
A56:F.p=a|^p by A4,A5,A52;
A57:F.s=a|^s by A4,A5,A53;
per cases;
suppose A58:p<=s;
then A59:p<s by A55,REAL_1:def 5;
reconsider r1=s-p as Nat by A58,INT_1:18;
A60: r1=s+-p by XCMPLX_0:def 8;
1.G=a|^s*(a|^p)" by A54,A56,A57,GROUP_1:def 5;
then a|^0=a|^s*(a|^p)" by GROUP_1:43;
then a|^0=a|^s*(a|^(-p)) by GROUP_1:71;
then a|^0=a|^(s+(-p)) by GROUP_1:64;
then A61:1.G=a|^r1 by A60,GROUP_1:43;
A62: r1 <> 0 by A59,SQUARE_1:11;
A63:p >0
proof
p>=1 by A5,A52,FINSEQ_1:3;
hence thesis by AXIOMS:22;
end;
A64:r1 < ord a
proof
A65: s'<=z by A5,A53,FINSEQ_1:3;
z<z+p' by A63,REAL_1:69;
then s'<z+p' by A65,AXIOMS:22;
then s'-p'<z+p'-p' by REAL_1:54;
then s'-p'<z+p'+-p' by XCMPLX_0:def 8;
then s'-p'<z+(p'+-p') by XCMPLX_1:1;
then s'-p'<z+0 by XCMPLX_0:def 6;
hence thesis;
end;
a is_not_of_order_0 by A1,Th26;
hence thesis by A61,A62,A64,GROUP_1:def 11;
suppose A66:s<=p;
then A67:s<p by A55,REAL_1:def 5;
reconsider r2=p-s as Nat by A66,INT_1:18;
A68: r2=p+-s by XCMPLX_0:def 8;
1.G=a|^p*(a|^s)" by A54,A56,A57,GROUP_1:def 5;
then a|^0=a|^p*(a|^s)" by GROUP_1:43;
then a|^0=a|^p*(a|^(-s)) by GROUP_1:71;
then a|^0=a|^(p+(-s)) by GROUP_1:64;
then A69:1.G=a|^r2 by A68,GROUP_1:43;
A70: r2 <> 0 by A67,SQUARE_1:11;
A71:s >0
proof
s>=1 by A5,A53,FINSEQ_1:3;
hence thesis by AXIOMS:22;
end;
A72:r2 < ord a
proof
A73: p'<=z by A5,A52,FINSEQ_1:3;
z<z+s' by A71,REAL_1:69;
then p'<z+s' by A73,AXIOMS:22;
then p'-s'<z+s'-s' by REAL_1:54;
then p'-s'<z+s'+-s' by XCMPLX_0:def 8;
then p'-s'<z+(s'+-s') by XCMPLX_1:1;
then p'-s'<z+0 by XCMPLX_0:def 6;
hence thesis;
end;
a is_not_of_order_0 by A1,Th26;
hence thesis by A69,A70,A72,GROUP_1:def 11;
end;
then A74: Seg ord a,the carrier of gr {a} are_equipotent by A5,A10,WELLORD2:def
4;
consider ca being finite set such that
A75: ca = the carrier of gr {a} & ord gr {a} = card ca by A2,GROUP_1:def 14;
reconsider So = Seg ord a as finite set;
card So = card ca by A74,A75,CARD_1:21;
hence thesis by A75,FINSEQ_1:78;
end;
theorem Th28:
G is finite implies ord a divides ord G
proof
assume A1: G is finite;
then ord a = ord gr {a} by Th27;
hence ord a divides ord G by A1,GROUP_2:178;
end;
theorem Th29:
G is finite implies a|^ord G = 1.G
proof
assume G is finite;
then ord a divides ord G by Th28;
then consider t being Nat such that
A1: ord G = ord a * t by NAT_1:def 3;
a|^ord G = a |^ ord a |^ t by A1,GROUP_1:50
.= (1.G) |^ t by GROUP_1:82 .= 1.G by GROUP_1:42;
hence thesis;
end;
theorem Th30:
G is finite implies (a|^n)" = a|^(ord G - (n mod ord G))
proof
assume A1: G is finite;
set q = ord G;
set p'=n mod q;
q >=1 by A1,GROUP_1:90;
then A2: q > 0 by AXIOMS:22;
then n mod q <=q by NAT_1:46;
then reconsider q'=q -( n mod q) as Nat by INT_1:18;
a|^n*(a|^(q-(n mod q)))=a|^(n+q') by GROUP_1:48
.= a|^((q*(n div q)+(n mod q))+q') by A2,NAT_1:47
.= a|^(q*(n div q)+(q'+(n mod q))) by XCMPLX_1:1
.= a|^(q*(n div q)+((q +(-(n mod q)))+(n mod q))) by XCMPLX_0:def 8
.= a|^(q*(n div q)+(q +(-p'+p'))) by XCMPLX_1:1
.= a|^(q*(n div q)+q +(-p'+p')) by XCMPLX_1:1
.= a|^(q*(n div q)+q)*(a|^(-p'+p')) by GROUP_1:64
.= a|^(q*(n div q)+q)*(a|^(-p')*(a|^p')) by GROUP_1:65
.= a|^(q*(n div q)+q)*((a|^p')"*(a|^p')) by GROUP_1:71
.= a|^(q*(n div q)+q)*(1.G) by GROUP_1:def 5
.= a|^(q*(n div q)+q*1) by GROUP_1:def 4
.= a|^(q*(n div q+1)) by XCMPLX_1:8
.= a|^q|^(n div q+1) by GROUP_1:50
.= (1.G)|^(n div q+1) by A1,Th29
.= 1.G by GROUP_1:42;
hence thesis by GROUP_1:20;
end;
theorem Th31:
for G being strict Group holds
ord G > 1 implies ex a being Element of G st a <> 1.G
proof let G be strict Group;
assume that A1: ord 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;
then a in the carrier of (1).G by GROUP_2:def 7;
hence thesis by RLVECT_1:def 1;
end;
then G = (1).G by GROUP_2:71;
hence contradiction by A1,GROUP_2:81;
end;
theorem
for G being strict Group holds
G is finite & ord G = p & p is prime implies
for H being strict Subgroup of G holds H = (1).G or H = G
proof let G be strict Group;
assume that A1: G is finite and A2: ord G = p and A3: p is prime;
let H be strict Subgroup of G;
A4:H is finite by A1,GROUP_2:48;
ord H divides p by A1,A2,GROUP_2:178;
then ord H = 1 or ord H = p by A3,INT_2:def 5;
hence thesis by A1,A2,A4,GROUP_2:82,85;
end;
theorem Th33:
HGrStr(#INT,addint#) is associative Group-like
proof
set G = HGrStr (# INT, addint #);
A1: now let h,g be Element of G, A,B be Integer;
assume h = A & g = B;
hence h * g = addint.(A,B) by VECTSP_1:def 10 .= A + B by Th14;
end;
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 by INT_1:12;
A2: h * g = A + B by A1;
A3: g * f = B + C by A1;
thus (h * g) * f = A + B + C by A1,A2
.= A + (B + C) by XCMPLX_1:1
.= h * (g * f) by A1,A3;
end;
reconsider e=0 as Element of G by INT_1:12;
take e;
let h be Element of G;
reconsider A = h as Integer by INT_1:12;
thus h * e = A + 0 by A1
.= h;
thus e * h = 0 + A by A1
.= h;
reconsider g = - A as Element of G by INT_1:12;
take g;
thus h * g = A + (- A) by A1
.= e by XCMPLX_0:def 6;
thus g * h = (- A) + A by A1
.= e by XCMPLX_0:def 6;
end;
definition
func INT.Group -> strict Group equals :
Def4: HGrStr(#INT,addint#);
coherence by Th33;
end;
definition let n such that A1:n > 0;
func addint(n) -> BinOp of Segm(n) means
:Def5: for k,l being Element of Segm(n) holds
it.(k,l) = (k+l) mod n;
existence
proof
defpred P[Element of Segm n,Element of Segm n,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);
reconsider k'=k,l'=l as Nat;
((k'+l') mod n) < n by A1,NAT_1:46;
then reconsider c = (k'+l') mod n as Element of Segm(n) by A1,Th10;
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 BinOpEx(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 by BINOP_1:2;
end;
end;
theorem Th34:
for n st n > 0 holds HGrStr(#Segm(n),addint(n)#) is associative Group-like
proof
let n;
assume A1:n>0;
set G = HGrStr (# Segm(n), addint(n) #);
A2: now let h,g be Element of G, A,B be Element of Segm(n);
assume h = A & g = B;
hence h * g = (addint(n)).(A,B) by VECTSP_1:def 10
.= (A + B) mod n by A1,Def5;
end;
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);
A3: h * g = (A + B) mod n by A2;
A4: g * f = (B + C) mod n by A2;
thus (h * g) * f = (((A + B) mod n) + C) mod n by A2,A3
.= ((A + B) + C) mod n by Th2
.=(A + (B + C)) mod n by XCMPLX_1:1
.=(A + ((B + C) mod n)) mod n by Th2
.= h * (g * f) by A2,A4;
end;
reconsider e=0 as Element of G by A1,Th10;
take e;
let h be Element of G;
reconsider A = h as Element of Segm(n);
reconsider A as Nat;
A5:A < n by A1,Th10;
thus h * e = (A + 0) mod n by A2
.= h by A5,Th4;
thus e * h = (0 + A) mod n by A2
.= h by A5,Th4;
consider p such that A6: n=A+p by A5,NAT_1:28;
A7: p <= n by A6,NAT_1:37;
(p mod n) < n by A1,NAT_1:46;
then reconsider g = p mod n as Element of G by A1,Th10;
take g;
reconsider B=g as Element of Segm(n);
thus h * g =e
proof
now per cases by A7,REAL_1:def 5;
suppose A8:p = n;
then n + 0 =A + n by A6;
then A9:A = 0 by XCMPLX_1:2;
h * g = (A +B) mod n by A2
.= (0 * n) mod n by A8,A9,Th5
.= e by GROUP_4:101;
hence thesis;
suppose A10:p < n;
h * g = (A +B) mod n by A2
.= n mod n by A6,A10,Th4
.= e by Th5;
hence thesis;
end;
hence thesis;
end;
thus g * h = e
proof
now per cases by A7,REAL_1:def 5;
suppose A11:p = n;
then n + 0 =A + n by A6;
then A = 0 by XCMPLX_1:2;
then g * h = (n mod n + 0) mod n by A2,A11
.= (0 * n) mod n by Th5
.= e by GROUP_4:101;
hence thesis;
suppose A12:p < n;
g * h = (A + B) mod n by A2
.=n mod n by A6,A12,Th4
.= e by Th5;
hence thesis;
end;
hence thesis;
end;
end;
definition let n such that A1: n > 0;
func INT.Group(n) -> strict Group equals
:Def6: HGrStr(#Segm(n),addint(n)#);
coherence by A1,Th34;
end;
theorem Th35:
1.INT.Group = 0
proof
A1: now let h,g be Element of INT.Group, A,B be Integer;
assume h = A & g = B;
hence h * g = addint.(A,B) by Def4,VECTSP_1:def 10
.= A + B by Th14;
end;
reconsider e = 0 as Element of INT by INT_1:12;
reconsider e as Element of INT.Group by Def4;
for h being Element of INT.Group holds h * e = h & e * h =
h
proof
let h be Element of INT.Group;
reconsider A = h as Integer by Def4,INT_1:12;
A2: h * e = A + 0 by A1
.= h;
e * h = 0 + A by A1
.= h;
hence thesis by A2;
end;
hence thesis by GROUP_1:10;
end;
theorem Th36:
for n st n>0 holds 1.INT.Group(n) = 0
proof
let n;
assume A1: n>0;
then A2: INT.Group(n) = HGrStr(#Segm(n),addint(n)#) by Def6;
A3: now let h,g be Element of INT.Group(n),
A,B be Element of Segm(n);
assume h = A & g = B;
hence h * g = (addint(n)).(A,B) by A2,VECTSP_1:def 10
.= (A + B) mod n by A1,Def5;
end;
reconsider e = 0 as Element of Segm(n) by A1,Th10;
reconsider e as Element of INT.Group(n) by A2;
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) by A2;
reconsider A as Nat;
A4:A < n by A1,Th10;
A5: h * e = (A + 0) mod n by A3
.= h by A4,Th4;
e * h = (0 + A) mod n by A3
.= h by A4,Th4;
hence thesis by A5;
end;
hence thesis by GROUP_1:10;
end;
definition
let h be Element of INT.Group;
func @'h -> Integer equals :
Def7: h;
coherence by Def4,INT_1:12;
end;
definition
let h be Integer;
func @'h -> Element of INT.Group equals
h;
coherence by Def4,INT_1:12;
end;
theorem Th37:
for h being Element of INT.Group holds h" = -@'h
proof
A1: now let h,g be Element of INT.Group, A,B be Integer;
assume h = A & g = B;
hence h * g = addint.(A,B) by Def4,VECTSP_1:def 10
.= A + B by Th14;
end;
let h be Element of INT.Group;
A2:h=@'h by Def7;
reconsider g=-@'h as Element of INT.Group by Def4,INT_1:12;
h *g =@'h + -@'h by A1,A2 .=1.INT.Group by Th35,XCMPLX_0:def 6;
hence thesis by GROUP_1:20;
end;
reserve G1 for Subgroup of INT.Group,
h for Element of INT.Group;
Lm4:now let h,g be Element of INT.Group, A,B be Integer;
assume h = A & g = B;
hence h * g = addint.(A,B) by Def4,VECTSP_1:def 10
.= A + B by Th14;
end;
theorem Th38:
for h st h=1 holds for k holds h|^k = k
proof
let h;
assume A1:h=1;
defpred P[Nat] means h|^$1=$1;
h|^0=0 by Th35,GROUP_1:43; then
A2: P[0];
A3: for k st P[k] holds P[k+1]
proof
let k; assume h|^k = k;
then h|^k * h = k + 1 by A1,Lm4;
hence thesis by GROUP_1:49;
end;
for k holds P[k] from Ind(A2,A3);
hence thesis;
end;
theorem Th39:
for h,j1 st h=1 holds j1 = h |^ j1
proof
let h,j1;
assume A1:h=1;
consider k such that A2:j1 = k or j1 = -k by INT_1:8;
now per cases by A2;
suppose j1=k;
hence thesis by A1,Th38;
suppose A3: j1=-k;
reconsider k'=k as Integer;
reconsider k' as Element of INT.Group by Def4,INT_1:12
;
h|^j1 = (h|^k)" by A3,GROUP_1:71
.= (k')" by A1,Th38 .= -@'k' by Th37 .= j1 by A3,Def7;
hence thesis;
end;
hence thesis;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Definition of cyclic group ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Lm5:
ex a being Element of INT.Group
st the HGrStr of INT.Group = gr {a}
proof
reconsider h = 1 as Element of INT by INT_1:12;
reconsider h as Element of INT.Group by Def4;
take h;
{h} c= the carrier of (Omega).INT.Group &
(for G1 being strict Subgroup of INT.Group
st {h} c= the carrier of G1 holds
(Omega).INT.Group is Subgroup of G1 )
proof
A1: {h} c= the carrier of INT.Group;
for G1 st {h} c= the carrier of G1 holds (Omega).
INT.Group is Subgroup of G1
proof
let G1;
assume A2:{h} c= the carrier of G1;
the carrier of (Omega).INT.Group c= the carrier of G1
proof
let x;
assume that A3: x in the carrier of (Omega).INT.Group and
A4: not x in the carrier of G1;
x in (Omega).INT.Group by A3,RLVECT_1:def 1;
then x in INT.Group by GROUP_2:def 8;
then x in INT by Def4,RLVECT_1:def 1;
then reconsider x'=x as Integer by INT_1:12;
h in {h} by TARSKI:def 1;
then reconsider h''=h as Element of G1 by A2;
A5: (h'')|^x' in the carrier of G1;
(h'')|^x'=h|^x' by GROUP_4:4;
hence contradiction by A4,A5,Th39;
end;
hence thesis by GROUP_2:66;
end;
hence thesis by A1,GROUP_2:def 8;
end;
then (Omega).INT.Group = gr {h} by GROUP_4:def 5;
hence thesis by GROUP_2:def 8;
end;
definition let IT be Group;
attr IT is cyclic means
:Def9: ex a being Element of IT st the HGrStr of IT=gr {a};
end;
definition
cluster strict cyclic Group;
existence
proof INT.Group is cyclic by Def9,Lm5;
hence thesis;
end;
end;
theorem Th40:
(1).G is cyclic
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;
{PG} c= the carrier of (Omega).(1).G &
( for G1 being strict Subgroup of (1).G st {PG} c= the carrier of G1 holds
(Omega).(1).G is Subgroup of G1 )
proof
A1: {PG} = the carrier of (1).G by GROUP_2:def 7;
( 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 A2:{PG} c= the carrier of G1;
the carrier of (Omega).(1).G =the carrier of (1).G by GROUP_2:def 8;
then the carrier of (Omega).
(1).G c=the carrier of G1 by A2,GROUP_2:def 7;
hence thesis by GROUP_2:66;
end;
hence thesis by A1,GROUP_2:def 8;
end;
then (Omega).(1).G = gr {PG} by GROUP_4:def 5;
hence thesis by GROUP_2:def 8;
end;
theorem Th41:
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 HGrStr of G = gr {a} by Def9;
take a;
for b being Element of G ex j1 st b=a|^j1
proof
let b be Element of G;
b in gr {a} by A1,RLVECT_1:def 1;
hence thesis by Th25;
end;
hence thesis;
end;
thus (ex a being Element of G st
for b being Element of G
ex j1 st b = a|^j1) implies G is cyclic Group
proof
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 Th25;
end;
then the HGrStr of G = gr {a} by GROUP_2:71;
hence thesis by Def9;
end;
end;
theorem Th42:
G is finite implies (G is cyclic Group iff
ex a being Element of G st
for b being Element of G ex n st b=a|^n)
proof
assume A1: G is finite;
thus G is cyclic Group 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 Group;
then consider a being Element of G such that
A2: for b being Element of G ex j2 st b=a|^j2
by Th41;
take a;
let b be Element of G;
consider j2 such that A3: b = a|^j2 by A2;
consider n such that A4:j2=n or j2=-n by INT_1:8;
per cases by A4;
suppose j2=n; hence thesis by A3;
suppose A5:j2=-n;
ord G >=1 by A1,GROUP_1:90;
then ord G > 0 by AXIOMS:22;
then n mod ord G <=ord G by NAT_1:46;
then reconsider q'=ord G -( n mod ord G) as Nat by INT_1:18;
take q';
b=(a|^n)" by A3,A5,GROUP_1:71
.= a|^q' by A1,Th30;
hence thesis;
end;
given a being Element of G such that
A6: 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 A7:b=a|^n by A6;
reconsider n as Integer;
take n;
thus thesis by A7;
end;
hence thesis by Th41;
end;
theorem Th43:
for G being strict Group holds
G is finite implies
( G is cyclic Group iff
ex a being Element of G st ord a =ord G )
proof let G be strict Group;
assume A1: G is finite;
thus G is cyclic Group implies
ex a being Element of G st ord a =ord G
proof
assume G is cyclic Group;
then consider a being Element of G such that
A2: G = gr {a} by Def9;
take a;
thus thesis by A1,A2,Th27;
end;
given a being Element of G such that A3:ord a =ord G;
ex a being Element of G st G = gr {a}
proof
consider a being Element of G such that
A4: ord a = ord G by A3;
take a;
ord gr {a} = ord G by A1,A4,Th27;
hence thesis by A1,GROUP_2:85;
end;
hence thesis by Def9;
end;
theorem
for H being strict Subgroup of G holds
G is finite & G is cyclic Group implies
H is cyclic Group
proof let H be strict Subgroup of G;
assume that A1: G is finite and A2:G is cyclic Group;
consider a such that
A3: for b being Element of G ex n st b = a|^n by A1,A2,Th42;
A4: H is finite by A1,GROUP_2:48;
then A5: ord H >= 1 by GROUP_1:90;
per cases by A5,REAL_1:def 5;
suppose ord H =1;
then H = (1).G by A4,GROUP_2:82;
hence thesis by Th40;
suppose ord H > 1;
then consider h being Element of H such that
A6:h <>1.H by Th31;
defpred P[Nat] means
$1 > 0 & a|^$1 is Element of H;
h is Element of G by GROUP_2:51;
then consider n such that A7: h = a|^n by A3;
n <> 0
proof
assume n = 0;
then h = 1.G by A7,GROUP_1:59 .= 1.H by GROUP_2:53;
hence contradiction by A6;
end;
then n > 0 by NAT_1:19;
then A8: ex n st P[n] by A7;
ex h1 being Element of H st
for b being Element of H ex s st b = h1|^s
proof
ex k st P[k] & for n st P[n] holds k <= n from Min(A8); then
consider n such that
A9: (n>0 & a|^n is Element of H) and
A10: for k st
(k>0 & a|^k is Element of H) holds n <= k;
consider h1 being Element of H such that
A11: h1 = a|^n by A9;
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:51;
then consider p such that A12: b = a|^p by A3;
consider s,r such that A13: p = (n*s) + r and
A14:r < n by A9,NAT_1:42;
A15: r =0
proof
assume r<>0;
then A16: r >0 by NAT_1:19;
A17: a|^p = a|^(n*s) * (a|^r) by A13,GROUP_1:48;
h1|^s=a|^n|^s by A11,GROUP_4:3;
then (h1|^s)"=(a|^n|^s)" by GROUP_2:57 .= (a|^(n * s ))" by GROUP_1:50;
then reconsider g= (a|^(n*s))" as Element of H;
reconsider b=a|^p as Element of H by A12;
(a|^(n*s))" * (a|^p)
= ((a|^(n*s))" *(a|^(n*s)))*(a|^r) by A17,VECTSP_1:def 16
.= 1.G *(a|^r) by GROUP_1:def 5 .= a|^ r by GROUP_1:def 4;
then g*b = a|^r by GROUP_2:52;
hence contradiction by A10,A14,A16;
end;
take s;
a|^p = a|^n|^s by A13,A15,GROUP_1:50 .= h1|^s by A11,GROUP_4:3;
hence thesis by A12;
end;
hence thesis;
end;
hence thesis by A4,Th42;
end;
theorem
for G being strict Group holds
G is finite & ord (G) = p & p is prime implies
G is cyclic Group
proof let G be strict Group;
assume that A1: G is finite and A2: ord (G) = p and
A3: p is prime;
ex a being Element of G st ord a = p
proof
assume A4: for a being Element of G holds ord a <> p;
A5: now let a be Element of G;
ord a divides p by A1,A2,Th28;
then ord a = 1 or ord a = p by A3,INT_2:def 5;
hence ord a = 1 by A4;
end;
A6:the carrier of G c= the carrier of (1).G
proof
for x being set holds x in the carrier of G implies
x in the carrier of (1).G
proof
let x be set;
assume x in the carrier of G;
then reconsider x'=x as Element of G;
ord x' = 1 by A5;
then x' = 1.G by GROUP_1:85;
then x' in {1.G} by TARSKI:def 1;
hence thesis by GROUP_2:def 7;
end;
hence thesis by TARSKI:def 3;
end;
the carrier of (1).G c= the carrier of G by GROUP_2:def 5;
then the carrier of G = the carrier of (1).G by A6,XBOOLE_0:def 10;
then G = (1).G by GROUP_2:70;
then ord G = 1 by GROUP_2:81;
hence contradiction by A2,A3,INT_2:def 5;
end;
hence thesis by A1,A2,Th43;
end;
theorem Th46:
for n st n>0 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;
assume A1:n>0;
then A2: INT.Group(n) = HGrStr(#Segm(n),addint(n)#) by Def6;
A3: now let h,g be Element of INT.Group(n),
A,B be Element of Segm(n);
assume h = A & g = B;
hence h * g = (addint(n)).(A,B) by A2,VECTSP_1:def 10
.= (A + B) mod n by A1,Def5;
end;
0 +1 < n+1 by A1,REAL_1:53;
then A4:n >=1 by NAT_1:38;
now per cases by A4,REAL_1:def 5;
suppose n=1;
then the carrier of INT.Group(n) = {1.INT.Group(n)} by A2,Th13,Th36
.= the carrier of (1).INT.Group(n) by GROUP_2:def 7;
then INT.Group(n) = (1).INT.Group(n) by GROUP_2:70;
then INT.Group(n) is cyclic Group by Th40;
hence thesis by Th41;
suppose n>1;
then reconsider g'= 1 as Element of Segm(n) by A1,Th10;
reconsider g=g' as Element of INT.Group(n) by A2;
for b being Element of INT.Group(n) ex j1 st b = g|^j1
proof
let b be Element of INT.Group(n);
reconsider b'=b as Nat by A1,A2,Lm1;
defpred P[Nat] means g|^$1 = $1 mod n;
g|^0 = 1.INT.Group(n) by GROUP_1:43 .= 0 by A1,Th36
.= 0 mod n by Th6; then
A5:P[0];
A6: for k st P[k] holds P[k+1]
proof
let k;
k mod n < n by A1,NAT_1:46;
then reconsider e=(k mod n) as Element of Segm(n) by A1,Th10;
assume A7: g|^k = k mod n;
g|^(k+1) =g|^k*(g|^1) by GROUP_1:48 .=g|^k*g by GROUP_1:44
.= (e +g') mod n by A3,A7 .=(k+1) mod n by Th2;
hence thesis;
end;
A8: for k holds P[k] from Ind(A5,A6);
A9: b'<n by A1,A2,Th10;
A10: g|^b'=b' mod n by A8 .= b by A9,Th4;
reconsider b' as Integer;
take b';
thus thesis by A10;
end;
hence thesis;
end;
hence thesis;
end;
definition
cluster cyclic -> commutative 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,Th41;
take e;
A3:ex j2 st a=e|^j2 by A2;
ex j3 st b=e|^j3 by A2;
hence thesis by A3;
end;
then consider e being Element of G,j2,j3 such that
A4:( a = e|^j2 & b = e|^j3);
a * b = e |^(j3 + j2) by A4,GROUP_1:63 .= b * a by A4,GROUP_1:63;
hence thesis;
end;
hence thesis by VECTSP_1:def 17;
end;
end;
canceled;
theorem Th48:
INT.Group is cyclic
proof
reconsider h = 1 as Element of INT by INT_1:12;
reconsider h as Element of INT.Group by Def4;
take h;
{h} c= the carrier of (Omega).INT.Group &
( for G1 being strict Subgroup of INT.Group st {h} c= the carrier of G1 holds
(Omega).INT.Group is Subgroup of G1 )
proof
A1: {h} c= the carrier of (Omega).INT.Group
proof
{h} c= the carrier of INT.Group;
hence thesis by GROUP_2:def 8;
end;
for G1 st {h} c= the carrier of G1 holds (Omega).INT.Group is Subgroup of
G1
proof
let G1;
assume A2:{h} c= the carrier of G1;
the carrier of (Omega).INT.Group c= the carrier of G1
proof
for x holds x in the carrier of (Omega).INT.Group implies x in
the carrier of G1
proof
let x;
assume that A3: x in the carrier of (Omega).INT.Group and
A4: not x in the carrier of G1;
x in (Omega).INT.Group by A3,RLVECT_1:def 1;
then x in INT.Group by GROUP_2:def 8;
then x in INT by Def4,RLVECT_1:def 1;
then reconsider x'=x as Integer by INT_1:12;
h in {h} by TARSKI:def 1;
then reconsider h''=h as Element of G1 by A2;
A5: (h'')|^x' in the carrier of G1;
(h'')|^x'=h|^x' by GROUP_4:4;
hence contradiction by A4,A5,Th39;
end;
hence the carrier of (Omega).
INT.Group c= the carrier of G1 by TARSKI:def 3;
thus thesis;
end;
hence thesis by GROUP_2:66;
end;
hence thesis by A1;
end;
then (Omega).INT.Group = gr {h} by GROUP_4:def 5;
hence thesis by GROUP_2:def 8;
end;
theorem Th49:
for n st n > 0 holds INT.Group(n) is cyclic Group
proof
let n;
assume n > 0;
then ex g being Element of INT.Group(n) st
for b being Element of INT.Group(n) ex j1 st b = g|^j1 by Th46;
hence thesis by Th41;
end;
theorem
INT.Group is commutative Group
proof
INT.Group is cyclic Group by Th48;
hence thesis;
end;
theorem
for n st n>0 holds INT.Group(n) is commutative Group by Th49;