let G be Group; :: thesis: for H being Subgroup of G
for a being Element of G
for f being inner Automorphism of G st a is_inner_wrt f holds
Image (f | H) = H |^ a
let H be Subgroup of G; :: thesis: for a being Element of G
for f being inner Automorphism of G st a is_inner_wrt f holds
Image (f | H) = H |^ a
let a be Element of G; :: thesis: for f being inner Automorphism of G st a is_inner_wrt f holds
Image (f | H) = H |^ a
let f be inner Automorphism of G; :: thesis: ( a is_inner_wrt f implies Image (f | H) = H |^ a )
assume A1: for x being Element of G holds f . x = x |^ a ; :: according to GROUP_22:def 2 :: thesis: Image (f | H) = H |^ a
A2: for h being Element of G st h in H holds
(f | H) . h = h |^ a

proof

let h be Element of G; :: thesis: ( h in H implies (f | H) . h = h |^ a )
assume h in H ; :: thesis: (f | H) . h = h |^ a
hence (f | H) . h = f . h by Th1
.= h |^ a by A1 ;
:: thesis: verum

end;

C2: for y being Element of G st y in Image (f | H) holds
y in H |^ a

proof

let y be Element of G; :: thesis: ( y in Image (f | H) implies y in H |^ a )
assume y in Image (f | H) ; :: thesis: y in H |^ a
then consider h being Element of H such that
B1: (f | H) . h = y by GROUP_6:45;
reconsider h = h as Element of G by GROUP_2:42;
B2: h in H ;
then h |^ a = (f | H) . h by A2
.= y by B1 ;
hence y in H |^ a by B2, GROUP_3:58; :: thesis: verum

end;

for y being Element of G st y in H |^ a holds
y in Image (f | H)

proof

let y be Element of G; :: thesis: ( y in H |^ a implies y in Image (f | H) )
assume y in H |^ a ; :: thesis: y in Image (f | H)
then consider g being Element of G such that
B1: y = g |^ a and
B2: g in H by GROUP_3:58;
(f | H) . g = f . g by Th1, B2
.= g |^ a by A1
.= y by B1 ;
hence y in Image (f | H) by B2, GROUP_6:45; :: thesis: verum

end;

hence H |^ a = Image (f | H) by C2; :: thesis: verum