let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G) holds Image (incl1 (G,A,phi)) is normal Subgroup of semidirect_product (G,A,phi)
let phi be Homomorphism of A,(AutGroup G); :: thesis: Image (incl1 (G,A,phi)) is normal Subgroup of semidirect_product (G,A,phi)
for x, g being Element of (semidirect_product (G,A,phi)) st g is Element of (Image (incl1 (G,A,phi))) holds
g |^ x in Image (incl1 (G,A,phi))

proof

let x, g be Element of (semidirect_product (G,A,phi)); :: thesis: ( g is Element of (Image (incl1 (G,A,phi))) implies g |^ x in Image (incl1 (G,A,phi)) )
assume g is Element of (Image (incl1 (G,A,phi))) ; :: thesis: g |^ x in Image (incl1 (G,A,phi))
then g in Image (incl1 (G,A,phi)) ;
then consider g0 being Element of G such that
A1: g = (incl1 (G,A,phi)) . g0 by GROUP_6:45;
A2: g = <*g0,(1_ A)*> by A1, Def2;
consider x1 being Element of G, x2 being Element of A such that
A3: x = <*x1,x2*> by Th12;
reconsider phi2 = phi . (x2 ") as Homomorphism of G,G by AUTGROUP:def 1;
x " = <*(phi2 . (x1 ")),(x2 ")*> by A3, Th22;
then (x ") * g = <*((phi2 . (x1 ")) * (phi2 . g0)),((x2 ") * (1_ A))*> by A2, Th14
.= <*((phi2 . (x1 ")) * (phi2 . g0)),(x2 ")*> by GROUP_1:def 4
.= <*(phi2 . ((x1 ") * g0)),(x2 ")*> by GROUP_6:def 6 ;
then A4: ((x ") * g) * x = <*((phi2 . ((x1 ") * g0)) * (phi2 . x1)),((x2 ") * x2)*> by A3, Th14
.= <*((phi2 . ((x1 ") * g0)) * (phi2 . x1)),(1_ A)*> by GROUP_1:def 5
.= <*(phi2 . (((x1 ") * g0) * x1)),(1_ A)*> by GROUP_6:def 6
.= <*(phi2 . (g0 |^ x1)),(1_ A)*> by GROUP_3:def 2 ;
g |^ x = ((x ") * g) * x by GROUP_3:def 2
.= (incl1 (G,A,phi)) . (phi2 . (g0 |^ x1)) by A4, Def2 ;
hence g |^ x in Image (incl1 (G,A,phi)) by GROUP_6:45; :: thesis: verum

end;

hence Image (incl1 (G,A,phi)) is normal Subgroup of semidirect_product (G,A,phi) by AUTGROUP:1; :: thesis: verum