let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for x, e being Element of (semidirect_product (G,A,phi)) st e = <*(1_ G),(1_ A)*> holds
( x * e = x & e * x = x )
let phi be Homomorphism of A,(AutGroup G); :: thesis: for x, e being Element of (semidirect_product (G,A,phi)) st e = <*(1_ G),(1_ A)*> holds
( x * e = x & e * x = x )
let x, e be Element of (semidirect_product (G,A,phi)); :: thesis: ( e = <*(1_ G),(1_ A)*> implies ( x * e = x & e * x = x ) )
assume A1: e = <*(1_ G),(1_ A)*> ; :: thesis: ( x * e = x & e * x = x )
consider g being Element of G, a being Element of A such that
A2: x = <*g,a*> by Th12;
reconsider phi1 = phi . (1_ A), phia = phi . a as Homomorphism of G,G by AUTGROUP:def 1;
A3: (phi1 . g) * (1_ G) = g * (1_ G) by Th15
.= g by GROUP_1:def 4 ;
thus x * e = <*(g * (phia . (1_ G))),(a * (1_ A))*> by A1, A2, Th14
.= <*(g * (phia . (1_ G))),a*> by GROUP_1:def 4
.= <*(g * (1_ G)),a*> by GROUP_6:31
.= x by A2, GROUP_1:def 4 ; :: thesis: e * x = x
thus e * x = <*((1_ G) * (phi1 . g)),((1_ A) * a)*> by A1, A2, Th14
.= <*((1_ G) * (phi1 . g)),a*> by GROUP_1:def 4
.= <*((1_ G) * g),a*> by A3, GROUP_1:def 4
.= x by A2, GROUP_1:def 4 ; :: thesis: verum