let p be natural prime number ; :: thesis: for G, H being Group st G,H are_isomorphic & G is p -commutative-group-like holds
H is p -commutative-group-like
let G, H be Group; :: thesis: ( G,H are_isomorphic & G is p -commutative-group-like implies H is p -commutative-group-like )
assume that
A1: G,H are_isomorphic and
A2: G is p -commutative-group-like ; :: thesis: H is p -commutative-group-like
let h1, h2 be Element of H; :: according to GROUPP_1:def 3 :: thesis: (h1 * h2) |^ p = (h1 |^ p) * (h2 |^ p)
consider h being Homomorphism of G,H such that
A5: h is bijective by A1, GROUP_6:def 15;
consider a being Element of G such that
A6: h . a = h1 by A5, GROUP_6:68;
consider b being Element of G such that
A7: h . b = h2 by A5, GROUP_6:68;
h1 * h2 = h . (a * b) by A6, A7, GROUP_6:def 7;
then (h1 * h2) |^ p = h . ((a * b) |^ p) by GROUP_6:46
.= h . ((a |^ p) * (b |^ p)) by A2, def3
.= (h . (a |^ p)) * (h . (b |^ p)) by GROUP_6:def 7
.= ((h . a) |^ p) * (h . (b |^ p)) by GROUP_6:46
.= (h1 |^ p) * (h2 |^ p) by A6, A7, GROUP_6:46 ;
hence (h1 * h2) |^ p = (h1 |^ p) * (h2 |^ p) ; :: thesis: verum