let G be finite strict commutative Group; :: thesis: for p being Prime
for m being Nat st card G = p |^ m holds
ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st
( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st
( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds
F . <*a,b*> = a * b ) ) )
let p be Prime; :: thesis: for m being Nat st card G = p |^ m holds
ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st
( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st
( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds
F . <*a,b*> = a * b ) ) )
let m be Nat; :: thesis: ( card G = p |^ m implies ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st
( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st
( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds
F . <*a,b*> = a * b ) ) ) )
assume AS: card G = p |^ m ; :: thesis: ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st
( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st
( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds
F . <*a,b*> = a * b ) ) )
consider g being Element of G such that
A0: ord g = upper_bound (Ordset G) by LM202;
consider K being strict normal Subgroup of G such that
P1: ( 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 ) ) ) by AS, A0, LM204A;
consider n being Nat such that
Q4: ( card (gr {g}) = p |^ n & n <= m ) by AS, GROUPP_1:2, GROUP_2:148;
m - n in NAT by Q4, INT_1:3, XREAL_1:48;
then reconsider k = m - n as Nat ;
gr {g} is normal Subgroup of G by GROUP_3:116;
then consider F being Homomorphism of (product <*K,(gr {g})*>),G such that
P5: ( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds
F . <*a,b*> = a * b ) ) by P1, GROUP_17:12;
set s = card K;
set t = card (gr {g});
( F is one-to-one & dom F = the carrier of (product <*K,(gr {g})*>) & rng F = the carrier of G ) by P5, FUNCT_2:def 1, FUNCT_2:def 3;
then X6: card (product <*K,(gr {g})*>) = card G by CARD_1:5, WELLORD2:def 4;
(card K) * (p |^ n) = p |^ (k + n) by X6, Q4, AS, GROUP_17:17
.= (p |^ k) * (p |^ n) by NEWTON:8 ;
then card K = p |^ k by XCMPLX_1:5;
hence ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st
( ord g = upper_bound (Ordset G) & K is finite & K is commutative & 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 ) ) & ord g = p |^ n & k = m - n & n <= m & card K = p |^ k & ex F being Homomorphism of (product <*K,(gr {g})*>),G st
( F is bijective & ( for a, b being Element of G st a in K & b in gr {g} holds
F . <*a,b*> = a * b ) ) ) by A0, P1, P5, Q4, GR_CY_1:7; :: thesis: verum