defpred S1[ Nat] means for G being finite strict commutative Group
for p being Prime
for g being Element of G st card G = p |^ $1 & ord g = upper_bound (Ordset G) holds
ex K being strict normal Subgroup of G st
( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st
( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) );
P0:
S1[ 0 ]
PN:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume AS1:
S1[
k]
;
S1[k + 1]
let G be
finite strict commutative Group;
for p being Prime
for g being Element of G st card G = p |^ (k + 1) & ord g = upper_bound (Ordset G) holds
ex K being strict normal Subgroup of G st
( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st
( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )let p be
Prime;
for g being Element of G st card G = p |^ (k + 1) & ord g = upper_bound (Ordset G) holds
ex K being strict normal Subgroup of G st
( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st
( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )let a be
Element of
G;
( card G = p |^ (k + 1) & ord a = upper_bound (Ordset G) implies ex K being strict normal Subgroup of G st
( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st
( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) ) )
assume A1:
(
card G = p |^ (k + 1) &
ord a = upper_bound (Ordset G) )
;
ex K being strict normal Subgroup of G st
( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st
( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) )
deffunc H1(
finite Group)
-> Subset of
NAT =
Ordset $1;
per cases
( card (gr {a}) = card G or card (gr {a}) <> card G )
;
suppose B2:
card (gr {a}) <> card G
;
ex K being strict normal Subgroup of G st
( the carrier of K /\ the carrier of (gr {a}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st
( b1 in K & a1 in gr {a} & x = b1 * a1 ) ) )reconsider Gra =
gr {a} as
strict normal Subgroup of
G by GROUP_3:116;
reconsider G1 =
G ./. Gra as
finite strict commutative Group by GROUP630;
A5:
ord a = card (gr {a})
by GR_CY_1:7;
A6:
card G = (ord a) * (index Gra)
by A5, GROUP_2:147;
consider n1 being
Nat such that A8:
(
card Gra = p |^ n1 &
n1 <= k + 1 )
by GROUPP_1:2, GROUP_2:148, A1;
(k + 1) - n1 in NAT
by A8, XREAL_1:48, INT_1:3;
then reconsider mn1 =
(k + 1) - n1 as
Nat ;
A9:
ord a = p |^ n1
by A8, GR_CY_1:7;
A10:
ord a <> 0
by A8, GR_CY_1:7;
A10A:
0 < ord a
by A8, GR_CY_1:7;
index Gra =
(p |^ (mn1 + n1)) / (p |^ n1)
by A6, XCMPLX_1:89, A1, A9
.=
((p |^ mn1) * (p |^ n1)) / (p |^ n1)
by NEWTON:8
.=
p |^ mn1
by XCMPLX_1:89
;
then A11:
card (G ./. Gra) = p |^ mn1
by GROUP_6:27;
consider b being
Element of
G such that A20:
not
b in Gra
by B2, GROUPP_1:12;
reconsider bga =
b * Gra as
Element of
G1 by GROUP_2:def 15;
reconsider Grbga =
gr {bga} as
strict normal Subgroup of
G1 by GROUP_3:116;
consider s being
Nat such that A18:
(
card Grbga = p |^ s &
s <= mn1 )
by GROUPP_1:2, GROUP_2:148, A11;
A19:
ord bga = p |^ s
by A18, GR_CY_1:7;
ord bga <> 1
then
s <> 0
by A19, NEWTON:4;
then
0 <= s - 1
by NAT_1:14, XREAL_1:48;
then
s - 1
in NAT
by INT_1:3;
then reconsider s1 =
s - 1 as
Nat ;
reconsider c =
b |^ (p |^ s1) as
Element of
G ;
reconsider cga =
c * Gra as
Element of
G1 by GROUP_2:def 15;
A21:
(p |^ s1) * p =
p |^ (s1 + 1)
by NEWTON:6
.=
p |^ s
;
XN1:
(
p |^ s is
Element of
NAT &
p |^ s1 is
Element of
NAT &
p is
Element of
NAT )
by ORDINAL1:def 12;
A24:
ord (bga |^ (p |^ s1)) = p
by XN1, GRCY28, A21, A18;
A23:
ord cga = p
by A24, GROUPP_1:8;
A26:
not
c in Gra
A24:
cga |^ p = 1_ G1
by A23, GROUP_1:41;
A25:
cga |^ p = (c |^ p) * Gra
by GROUPP_1:8;
(c |^ p) * (1_ G) in (c |^ p) * Gra
by GROUP_2:46, GROUP_2:103;
then
c |^ p in (c |^ p) * Gra
by GROUP_1:def 4;
then
c |^ p in gr {a}
by A24, A25, GROUP_6:24;
then consider j being
Element of
NAT such that A26B:
c |^ p = a |^ j
by GRCY26;
p divides j
proof
assume
not
p divides j
;
contradiction
then A27Z:
j gcd (ord a) = 1
by A8, LM204K, GR_CY_1:7;
A272:
ord (c |^ p) = ord a
by A26B, A27Z, GRCY212A;
A273:
ord c = p * (ord (c |^ p))
proof
ord (c |^ p) <> 0
by A10, A26B, A27Z, GRCY212A;
then A274:
ord c <= p * (ord (c |^ p))
by XN1, GRCY211, NAT_D:7;
c <> 1_ G
by A26, GROUP_2:46;
then consider k being
Nat such that A2750:
ord c = p |^ (k + 1)
by A1, LM204I;
A275B:
p * (p |^ k) = ord c
by A2750, NEWTON:6;
A275:
(ord c) / p = p |^ k
by A275B, XCMPLX_1:89;
(c |^ p) |^ (p |^ k) =
c |^ (p * (p |^ k))
by GROUP_1:35
.=
1_ G
by A275B, GROUP_1:41
;
then
ord (c |^ p) <= (ord c) / p
by A275, NAT_D:7, GROUP_1:44;
then
p * (ord (c |^ p)) <= ord c
by XREAL_1:83;
hence
ord c = p * (ord (c |^ p))
by A274, XXREAL_0:1;
verum
end;
XXX0:
1
* (ord a) < p * (ord a)
by A10A, XREAL_1:68, INT_2:def 4;
ord c in Ordset G
;
hence
contradiction
by XXX0, A1, A272, A273, SEQ_4:def 1;
verum
end; then consider j1 being
Nat such that A28:
j = p * j1
by NAT_D:def 3;
A28A:
j1 is
Element of
NAT
by ORDINAL1:def 12;
set d =
c * (a |^ (- j1));
A30:
(c * (a |^ (- j1))) |^ p =
(c |^ p) * ((a |^ (- j1)) |^ p)
by GROUP_1:38
.=
(c |^ p) * (a |^ ((- j1) * p))
by GROUP_1:35
.=
(c |^ p) * (a |^ (- j))
by A28
.=
(c |^ p) * ((a |^ j) ")
by GROUP_1:36
.=
1_ G
by A26B, GROUP_1:def 5
;
ord (c * (a |^ (- j1))) <> 1
then A32:
ord (c * (a |^ (- j1))) = p
by A30, INT_2:def 4, GROUP_1:44;
A33:
not
c * (a |^ (- j1)) in gr {a}
A3Z:
for
x being
object holds
(
x in the
carrier of
(gr {(c * (a |^ (- j1)))}) /\ the
carrier of
(gr {a}) iff
x in {(1_ G)} )
then A33:
the
carrier of
(gr {(c * (a |^ (- j1)))}) /\ the
carrier of
(gr {a}) = {(1_ G)}
by TARSKI:2;
reconsider Grd =
gr {(c * (a |^ (- j1)))} as
strict normal Subgroup of
G by GROUP_3:116;
reconsider G2 =
G ./. Grd as
finite strict commutative Group by GROUP630;
D5:
ord (c * (a |^ (- j1))) = card (gr {(c * (a |^ (- j1)))})
by GR_CY_1:7;
D6:
card G = (ord (c * (a |^ (- j1)))) * (index Grd)
by D5, GROUP_2:147;
index Grd =
(card G) / (ord (c * (a |^ (- j1))))
by A32, D6, XCMPLX_1:89
.=
((p |^ k) * p) / p
by A1, A32, NEWTON:6
.=
p |^ k
by XCMPLX_1:89
;
then D11:
card (G ./. Grd) = p |^ k
by GROUP_6:27;
set Ordset1 =
Ordset G2;
set Pd =
nat_hom Grd;
D130:
nat_hom Grd is
onto
by GROUP_6:59;
reconsider gd =
(nat_hom Grd) . a as
Element of
G2 ;
set H =
(nat_hom Grd) | the
carrier of
Gra;
D14:
(nat_hom Grd) | the
carrier of
Gra is
one-to-one
by A3Z, LM204D, TARSKI:2;
D14B:
for
r being
Real st
r in Ordset G2 holds
r <= ord gd
XU1:
upper_bound (Ordset G2) <= ord gd
by SEQ_4:45, D14B;
ord gd in Ordset G2
;
then
ord gd <= upper_bound (Ordset G2)
by SEQ_4:def 1;
then
ord gd = upper_bound (Ordset G2)
by XXREAL_0:1, XU1;
then consider K2 being
strict normal Subgroup of
G2 such that D17:
( the
carrier of
K2 /\ the
carrier of
(gr {gd}) = {(1_ G2)} & ( for
g2 being
Element of
G2 ex
b2,
a2 being
Element of
G2 st
(
b2 in K2 &
a2 in gr {gd} &
g2 = b2 * a2 ) ) )
by AS1, D11;
consider K being
strict Subgroup of
G such that D19:
the
carrier of
K = (nat_hom Grd) " the
carrier of
K2
by GROUP252INV;
reconsider K =
K as
strict normal Subgroup of
G by GROUP_3:116;
D20:
for
x being
Element of
G st
x in the
carrier of
K /\ the
carrier of
(gr {a}) holds
(nat_hom Grd) . x in the
carrier of
K2 /\ the
carrier of
(gr {((nat_hom Grd) . a)})
D22:
for
x being
Element of
G st
x in the
carrier of
K /\ the
carrier of
(gr {a}) holds
x in the
carrier of
(Ker (nat_hom Grd)) /\ the
carrier of
(gr {a})
D23A:
the
carrier of
K /\ the
carrier of
(gr {a}) c= {(1_ G)}
(
1_ G in the
carrier of
(gr {a}) &
1_ G in the
carrier of
K )
by STRUCT_0:def 5, GROUP_2:46;
then
1_ G in the
carrier of
K /\ the
carrier of
(gr {a})
by XBOOLE_0:def 4;
then D23B:
{(1_ G)} c= the
carrier of
K /\ the
carrier of
(gr {a})
by ZFMISC_1:31;
for
g being
Element of
G ex
b1,
a1 being
Element of
G st
(
b1 in K &
a1 in gr {a} &
g = b1 * a1 )
proof
let g be
Element of
G;
ex b1, a1 being Element of G st
( b1 in K & a1 in gr {a} & g = b1 * a1 )
reconsider g2 =
(nat_hom Grd) . g as
Element of
G2 ;
consider b2,
a2 being
Element of
G2 such that D231:
(
b2 in K2 &
a2 in gr {gd} &
g2 = b2 * a2 )
by D17;
consider i being
Element of
NAT such that D231A:
a2 = gd |^ i
by GRCY26, D231;
rng (nat_hom Grd) = the
carrier of
G2
by D130, FUNCT_2:def 3;
then consider b1 being
Element of the
carrier of
G such that D232:
b2 = (nat_hom Grd) . b1
by FUNCT_2:113;
D234:
(nat_hom Grd) . ((a |^ i) * b1) =
((nat_hom Grd) . (a |^ i)) * ((nat_hom Grd) . b1)
by GROUP_6:def 6
.=
(nat_hom Grd) . g
by D231A, D231, D232, GROUP_6:37
;
D235:
((a |^ i) * b1) * (gr {(c * (a |^ (- j1)))}) =
(nat_hom Grd) . ((a |^ i) * b1)
by GROUP_6:def 8
.=
g * (gr {(c * (a |^ (- j1)))})
by D234, GROUP_6:def 8
;
g * (1_ G) in g * (gr {(c * (a |^ (- j1)))})
by GROUP_2:46, GROUP_2:103;
then
g in ((a |^ i) * b1) * (gr {(c * (a |^ (- j1)))})
by D235, GROUP_1:def 4;
then consider y being
Element of
G such that D236:
(
g = ((a |^ i) * b1) * y &
y in gr {(c * (a |^ (- j1)))} )
by GROUP_2:103;
D236A:
g = (a |^ i) * (b1 * y)
by D236, GROUP_1:def 3;
consider j being
Element of
NAT such that D237:
y = (c * (a |^ (- j1))) |^ j
by GRCY26, D236;
D238:
(nat_hom Grd) . (c * (a |^ (- j1))) =
(c * (a |^ (- j1))) * (gr {(c * (a |^ (- j1)))})
by GROUP_6:def 8
.=
carr (gr {(c * (a |^ (- j1)))})
by GR_CY_2:2, GROUP_2:113
.=
1_ G2
by GROUP_6:24
;
D239:
(nat_hom Grd) . y =
((nat_hom Grd) . (c * (a |^ (- j1)))) |^ j
by D237, GROUP_6:37
.=
1_ G2
by D238, GROUP_1:31
;
1_ G2 in the
carrier of
K2
by GROUP_2:46, STRUCT_0:def 5;
then
(
b1 in K &
y in K )
by D19, D231, D232, D239, FUNCT_2:38;
then
b1 * y in K
by GROUP_2:50;
hence
ex
b1,
a1 being
Element of
G st
(
b1 in K &
a1 in gr {a} &
g = b1 * a1 )
by D236A, GRCY26;
verum
end; hence
ex
K being
strict normal Subgroup of
G st
( the
carrier of
K /\ the
carrier of
(gr {a}) = {(1_ G)} & ( for
x being
Element of
G ex
b1,
a1 being
Element of
G st
(
b1 in K &
a1 in gr {a} &
x = b1 * a1 ) ) )
by D23A, D23B, XBOOLE_0:def 10;
verum end;
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(P0, PN);
hence
for G being finite strict commutative Group
for p being Prime
for m being Nat
for g being Element of G st card G = p |^ m & ord g = upper_bound (Ordset G) holds
ex K being strict normal Subgroup of G st
( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st
( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )
; verum