let p be prime Nat; for G being finite Group
for H being Subgroup of G
for N being strict normal Subgroup of G st N is Subgroup of center G & H is p -commutative-group & N is p -commutative-group holds
ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -commutative-group )
let G be finite Group; for H being Subgroup of G
for N being strict normal Subgroup of G st N is Subgroup of center G & H is p -commutative-group & N is p -commutative-group holds
ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -commutative-group )
let H be Subgroup of G; for N being strict normal Subgroup of G st N is Subgroup of center G & H is p -commutative-group & N is p -commutative-group holds
ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -commutative-group )
let N be strict normal Subgroup of G; ( N is Subgroup of center G & H is p -commutative-group & N is p -commutative-group implies ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -commutative-group ) )
assume that
A1:
N is Subgroup of center G
and
A2:
( H is p -commutative-group & N is p -commutative-group )
; ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -commutative-group )
consider P being strict Subgroup of G such that
A3:
( the carrier of P = H * N & P is p -group )
by A2, Th20;
set P1 = P;
for a, b being Element of P holds (a * b) |^ p = (a |^ p) * (b |^ p)
proof
let a,
b be
Element of
P;
(a * b) |^ p = (a |^ p) * (b |^ p)
A4:
(
a in H * N &
b in H * N )
by A3;
then consider a1,
a2 being
Element of
G such that A5:
(
a = a1 * a2 &
a1 in H &
a2 in N )
by GROUP_11:6;
A6:
a2 in center G
by A1, A5, GROUP_2:40;
consider b1,
b2 being
Element of
G such that A7:
(
b = b1 * b2 &
b1 in H &
b2 in N )
by A4, GROUP_11:6;
A8:
b2 in center G
by A1, A7, GROUP_2:40;
then
(
a2 * b2 in center G &
b2 * a2 in center G )
by A6, GROUP_2:50;
then A9:
(a1 * b1) * (b2 * a2) = (b2 * a2) * (a1 * b1)
by GROUP_5:77;
reconsider c1 =
a1,
d1 =
b1 as
Element of
H by A5, A7;
A10:
(
a1 |^ p = c1 |^ p &
b1 |^ p = d1 |^ p )
by GROUP_4:2;
a1 * b1 = c1 * d1
by GROUP_2:43;
then A11:
(a1 * b1) |^ p =
(c1 * d1) |^ p
by GROUP_8:4
.=
(c1 |^ p) * (d1 |^ p)
by A2, Def3
.=
(a1 |^ p) * (b1 |^ p)
by A10, GROUP_2:43
;
reconsider c2 =
a2,
d2 =
b2 as
Element of
N by A5, A7;
A12:
(
a2 |^ p = c2 |^ p &
b2 |^ p = d2 |^ p )
by GROUP_4:2;
b2 * a2 = d2 * c2
by GROUP_2:43;
then A13:
(b2 * a2) |^ p =
(d2 * c2) |^ p
by GROUP_8:4
.=
(d2 |^ p) * (c2 |^ p)
by A2, Def3
.=
(b2 |^ p) * (a2 |^ p)
by A12, GROUP_2:43
;
A14:
a2 |^ p in center G
by A6, GROUP_4:4;
A15:
a1 * a2 = a2 * a1
by A6, GROUP_5:77;
A16:
b1 * b2 = b2 * b1
by A8, GROUP_5:77;
a * b = (a1 * a2) * (b1 * b2)
by A5, A7, GROUP_2:43;
then A17:
(a * b) |^ p =
((a1 * a2) * (b1 * b2)) |^ p
by GROUP_8:4
.=
(a1 * (a2 * (b1 * b2))) |^ p
by GROUP_1:def 3
.=
(a1 * ((b1 * b2) * a2)) |^ p
by A6, GROUP_5:77
.=
(a1 * (b1 * (b2 * a2))) |^ p
by GROUP_1:def 3
.=
((a1 * b1) * (b2 * a2)) |^ p
by GROUP_1:def 3
.=
((a1 * b1) |^ p) * ((b2 * a2) |^ p)
by A9, GROUP_1:38
.=
((a1 |^ p) * (b1 |^ p)) * ((a2 |^ p) * (b2 |^ p))
by A11, A13, A14, GROUP_5:77
.=
(a1 |^ p) * ((b1 |^ p) * ((a2 |^ p) * (b2 |^ p)))
by GROUP_1:def 3
.=
(a1 |^ p) * (((b1 |^ p) * (a2 |^ p)) * (b2 |^ p))
by GROUP_1:def 3
.=
(a1 |^ p) * (((a2 |^ p) * (b1 |^ p)) * (b2 |^ p))
by A14, GROUP_5:77
.=
((a1 |^ p) * ((a2 |^ p) * (b1 |^ p))) * (b2 |^ p)
by GROUP_1:def 3
.=
(((a1 |^ p) * (a2 |^ p)) * (b1 |^ p)) * (b2 |^ p)
by GROUP_1:def 3
.=
((a1 |^ p) * (a2 |^ p)) * ((b1 |^ p) * (b2 |^ p))
by GROUP_1:def 3
.=
((a1 * a2) |^ p) * ((b1 |^ p) * (b2 |^ p))
by A15, GROUP_1:38
.=
((a1 * a2) |^ p) * ((b1 * b2) |^ p)
by A16, GROUP_1:38
;
A18:
a |^ p = (a1 * a2) |^ p
by A5, GROUP_4:2;
b |^ p = (b1 * b2) |^ p
by A7, GROUP_4:2;
hence
(a * b) |^ p = (a |^ p) * (b |^ p)
by A17, A18, GROUP_2:43;
verum
end;
then
P is p -commutative-group-like
;
hence
ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -commutative-group )
by A3; verum