let p be prime Nat; for G being finite Group
for H, N being Subgroup of G st N is normal Subgroup of G & H is p -group & N is p -group holds
ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -group )
let G be finite Group; for H, N being Subgroup of G st N is normal Subgroup of G & H is p -group & N is p -group holds
ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -group )
let H, N be Subgroup of G; ( N is normal Subgroup of G & H is p -group & N is p -group implies ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -group ) )
assume that
A1:
N is normal Subgroup of G
and
A2:
( H is p -group & N is p -group )
; ex P being strict Subgroup of G st
( the carrier of P = H * N & P is p -group )
H * N = N * H
by A1, GROUP_5:8;
then consider P being strict Subgroup of G such that
A3:
the carrier of P = H * N
by GROUP_2:78;
A4:
for a being Element of P holds a is p -power
proof
let a be
Element of
P;
a is p -power
a in H * N
by A3;
then consider b,
c being
Element of
G such that A5:
(
a = b * c &
b in H &
c in N )
by GROUP_11:6;
b is
p -power
by A5, A2, Th15;
then consider n being
Nat such that A6:
ord b = p |^ n
;
A7:
b |^ (p |^ n) = 1_ G
by A6, GROUP_1:41;
consider d being
Element of
G such that A8:
(
d in N &
(b * c) |^ (p |^ n) = (b |^ (p |^ n)) * d )
by A1, A5, Th7;
d is
p -power
by A2, A8, Th15;
then consider m being
Nat such that A9:
ord d = p |^ m
;
A10:
d |^ (p |^ m) = 1_ G
by A9, GROUP_1:41;
A11:
a |^ (p |^ (n + m)) =
(b * c) |^ (p |^ (n + m))
by A5, GROUP_8:4
.=
(b * c) |^ ((p |^ n) * (p |^ m))
by NEWTON:8
.=
((b * c) |^ (p |^ n)) |^ (p |^ m)
by GROUP_1:35
.=
1_ G
by A7, A8, A10, GROUP_1:def 4
;
reconsider a1 =
a as
Element of
G by GROUP_2:42;
a1 |^ (p |^ (n + m)) = 1_ G
by A11, GROUP_8:4;
then consider r being
Nat such that A12:
(
ord a1 = p |^ r &
r <= n + m )
by Th2, GROUP_1:44;
ord a = p |^ r
by A12, GROUP_8:5;
hence
a is
p -power
;
verum
end;
take
P
; ( the carrier of P = H * N & P is p -group )
thus
( the carrier of P = H * N & P is p -group )
by A3, A4, Th17; verum