let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for x, y being Element of (semidirect_product (G,A,phi))
for a being Element of A
for g being Element of G st x = <*g,a*> & y = <*((phi . (a ")) . (g ")),(a ")*> holds
( x * y = 1_ (semidirect_product (G,A,phi)) & y * x = 1_ (semidirect_product (G,A,phi)) )
let phi be Homomorphism of A,(AutGroup G); :: thesis: for x, y being Element of (semidirect_product (G,A,phi))
for a being Element of A
for g being Element of G st x = <*g,a*> & y = <*((phi . (a ")) . (g ")),(a ")*> holds
( x * y = 1_ (semidirect_product (G,A,phi)) & y * x = 1_ (semidirect_product (G,A,phi)) )
let x, y be Element of (semidirect_product (G,A,phi)); :: thesis: for a being Element of A
for g being Element of G st x = <*g,a*> & y = <*((phi . (a ")) . (g ")),(a ")*> holds
( x * y = 1_ (semidirect_product (G,A,phi)) & y * x = 1_ (semidirect_product (G,A,phi)) )
let a be Element of A; :: thesis: for g being Element of G st x = <*g,a*> & y = <*((phi . (a ")) . (g ")),(a ")*> holds
( x * y = 1_ (semidirect_product (G,A,phi)) & y * x = 1_ (semidirect_product (G,A,phi)) )
let g be Element of G; :: thesis: ( x = <*g,a*> & y = <*((phi . (a ")) . (g ")),(a ")*> implies ( x * y = 1_ (semidirect_product (G,A,phi)) & y * x = 1_ (semidirect_product (G,A,phi)) ) )
assume A1: x = <*g,a*> ; :: thesis: ( not y = <*((phi . (a ")) . (g ")),(a ")*> or ( x * y = 1_ (semidirect_product (G,A,phi)) & y * x = 1_ (semidirect_product (G,A,phi)) ) )
assume A2: y = <*((phi . (a ")) . (g ")),(a ")*> ; :: thesis: ( x * y = 1_ (semidirect_product (G,A,phi)) & y * x = 1_ (semidirect_product (G,A,phi)) )
reconsider phi1 = phi . (a "), phi2 = phi . a as Homomorphism of G,G by AUTGROUP:def 1;
A3: (phi1 . (g ")) * (phi1 . g) = phi1 . ((g ") * g) by GROUP_6:def 6
.= phi1 . (1_ G) by GROUP_1:def 5
.= 1_ G by GROUP_6:31 ;
A4: phi2 . (phi1 . (g ")) = g " by Th19;
thus x * y = <*(g * (phi2 . (phi1 . (g ")))),(a * (a "))*> by A1, A2, Th14
.= <*(1_ G),(a * (a "))*> by A4, GROUP_1:def 5
.= <*(1_ G),(1_ A)*> by GROUP_1:def 5
.= 1_ (semidirect_product (G,A,phi)) by Th17 ; :: thesis: y * x = 1_ (semidirect_product (G,A,phi))
thus y * x = <*((phi1 . (g ")) * (phi1 . g)),((a ") * a)*> by A1, A2, Th14
.= <*(1_ G),(1_ A)*> by A3, GROUP_1:def 5
.= 1_ (semidirect_product (G,A,phi)) by Th17 ; :: thesis: verum