let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G
for x being Element of (semidirect_product (G,A,phi)) st x = <*g,a*> holds
x " = <*((phi . (a ")) . (g ")),(a ")*>
let phi be Homomorphism of A,(AutGroup G); :: thesis: for a being Element of A
for g being Element of G
for x being Element of (semidirect_product (G,A,phi)) st x = <*g,a*> holds
x " = <*((phi . (a ")) . (g ")),(a ")*>
set S = semidirect_product (G,A,phi);
let a be Element of A; :: thesis: for g being Element of G
for x being Element of (semidirect_product (G,A,phi)) st x = <*g,a*> holds
x " = <*((phi . (a ")) . (g ")),(a ")*>
let g be Element of G; :: thesis: for x being Element of (semidirect_product (G,A,phi)) st x = <*g,a*> holds
x " = <*((phi . (a ")) . (g ")),(a ")*>
let x be Element of (semidirect_product (G,A,phi)); :: thesis: ( x = <*g,a*> implies x " = <*((phi . (a ")) . (g ")),(a ")*> )
assume A1: x = <*g,a*> ; :: thesis: x " = <*((phi . (a ")) . (g ")),(a ")*>
reconsider phi1 = phi . (a ") as Homomorphism of G,G by AUTGROUP:def 1;
reconsider y = <*(phi1 . (g ")),(a ")*> as Element of (semidirect_product (G,A,phi)) by Th9;
( x * y = 1_ (semidirect_product (G,A,phi)) & y * x = 1_ (semidirect_product (G,A,phi)) ) by A1, Th20;
hence x " = <*((phi . (a ")) . (g ")),(a ")*> by GROUP_1:5; :: thesis: verum