let G be Group; :: thesis: for H being strict Subgroup of G holds
( H is characteristic iff for phi being Automorphism of G
for x being Element of G st x in H holds
phi . x in H )
let H be strict Subgroup of G; :: thesis: ( H is characteristic iff for phi being Automorphism of G
for x being Element of G st x in H holds
phi . x in H )
thus ( H is characteristic implies for phi being Automorphism of G
for x being Element of G st x in H holds
phi . x in H ) :: thesis: ( ( for phi being Automorphism of G
for x being Element of G st x in H holds
phi . x in H ) implies H is characteristic )

proof

assume B1: H is characteristic ; :: thesis: for phi being Automorphism of G
for x being Element of G st x in H holds
phi . x in H
let phi be Automorphism of G; :: thesis: for x being Element of G st x in H holds
phi . x in H
let x be Element of G; :: thesis: ( x in H implies phi . x in H )
assume B2: x in H ; :: thesis: phi . x in H
B3: H = Image (phi | H) by B1
.= phi .: H by GRSOLV_1:def 3 ;
dom phi = the carrier of G by FUNCT_2:def 1;
then phi . x in phi .: the carrier of H by B2, FUNCT_1:def 6;
hence phi . x in H by B3, GRSOLV_1:8; :: thesis: verum

end;

thus ( ( for phi being Automorphism of G
for x being Element of G st x in H holds
phi . x in H ) implies H is characteristic ) :: thesis: verum

proof

assume B1: for phi being Automorphism of G
for x being Element of G st x in H holds
phi . x in H ; :: thesis: H is characteristic
for phi being Automorphism of G holds Image (phi | H) is Subgroup of H

proof

let phi be Automorphism of G; :: thesis: Image (phi | H) is Subgroup of H
for x being Element of H holds phi . x in H

proof

let x be Element of H; :: thesis: phi . x in H
reconsider g = x as Element of G by GROUP_2:42;
g in H ;
hence phi . x in H by B1; :: thesis: verum

end;

hence Image (phi | H) is Subgroup of H by Th44; :: thesis: verum

end;

hence H is characteristic by Th40; :: thesis: verum

end;