let p be Prime; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: 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 ; :: thesis: verum

end;

take P ; :: thesis: ( 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; :: thesis: verum