let G be finite commutative Group; :: thesis: for m being Nat
for A being Subset of G st A = { x where x is Element of G : x |^ m = 1_ G } holds
ex H being finite strict Subgroup of G st
( the carrier of H = A & H is commutative & H is normal )
let m be Nat; :: thesis: for A being Subset of G st A = { x where x is Element of G : x |^ m = 1_ G } holds
ex H being finite strict Subgroup of G st
( the carrier of H = A & H is commutative & H is normal )
let A be Subset of G; :: thesis: ( A = { x where x is Element of G : x |^ m = 1_ G } implies ex H being finite strict Subgroup of G st
( the carrier of H = A & H is commutative & H is normal ) )
assume A = { x where x is Element of G : x |^ m = 1_ G } ; :: thesis: ex H being finite strict Subgroup of G st
( the carrier of H = A & H is commutative & H is normal )
then ( A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) ) by Th13;
then consider H being strict Subgroup of G such that
A1: the carrier of H = A by GROUP_2:52;
H is normal by GROUP_3:116;
hence ex H being finite strict Subgroup of G st
( the carrier of H = A & H is commutative & H is normal ) by A1; :: thesis: verum