let p be prime Nat; 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; ( 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
; H is p -commutative-group-like
let h1, h2 be Element of H; GROUPP_1:def 3 (h1 * h2) |^ p = (h1 |^ p) * (h2 |^ p)
consider h being Homomorphism of G,H such that
A3:
h is bijective
by A1;
consider a being Element of G such that
A4:
h . a = h1
by A3, GROUP_6:58;
consider b being Element of G such that
A5:
h . b = h2
by A3, GROUP_6:58;
h1 * h2 = h . (a * b)
by A4, A5, GROUP_6:def 6;
then (h1 * h2) |^ p =
h . ((a * b) |^ p)
by GROUP_6:37
.=
h . ((a |^ p) * (b |^ p))
by A2
.=
(h . (a |^ p)) * (h . (b |^ p))
by GROUP_6:def 6
.=
((h . a) |^ p) * (h . (b |^ p))
by GROUP_6:37
.=
(h1 |^ p) * (h2 |^ p)
by A4, A5, GROUP_6:37
;
hence
(h1 * h2) |^ p = (h1 |^ p) * (h2 |^ p)
; verum