let G be Group; :: thesis: for N being strict normal Subgroup of G
for H being Subgroup of G st H,N are_complements_in G holds
for alpha being Homomorphism of H,(AutGroup N) st ( for h, n being Element of G st h in H & n in N holds
for a being Homomorphism of N,N st a = alpha . h holds
a . n = n |^ (h ") ) holds
ex beta being Homomorphism of (semidirect_product (N,H,alpha)),G st
( ( for gh, gn being Element of G
for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh ) & beta is bijective )
let N be strict normal Subgroup of G; :: thesis: for H being Subgroup of G st H,N are_complements_in G holds
for alpha being Homomorphism of H,(AutGroup N) st ( for h, n being Element of G st h in H & n in N holds
for a being Homomorphism of N,N st a = alpha . h holds
a . n = n |^ (h ") ) holds
ex beta being Homomorphism of (semidirect_product (N,H,alpha)),G st
( ( for gh, gn being Element of G
for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh ) & beta is bijective )
let H be Subgroup of G; :: thesis: ( H,N are_complements_in G implies for alpha being Homomorphism of H,(AutGroup N) st ( for h, n being Element of G st h in H & n in N holds
for a being Homomorphism of N,N st a = alpha . h holds
a . n = n |^ (h ") ) holds
ex beta being Homomorphism of (semidirect_product (N,H,alpha)),G st
( ( for gh, gn being Element of G
for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh ) & beta is bijective ) )
assume A1: H,N are_complements_in G ; :: thesis: for alpha being Homomorphism of H,(AutGroup N) st ( for h, n being Element of G st h in H & n in N holds
for a being Homomorphism of N,N st a = alpha . h holds
a . n = n |^ (h ") ) holds
ex beta being Homomorphism of (semidirect_product (N,H,alpha)),G st
( ( for gh, gn being Element of G
for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh ) & beta is bijective )
let alpha be Homomorphism of H,(AutGroup N); :: thesis: ( ( for h, n being Element of G st h in H & n in N holds
for a being Homomorphism of N,N st a = alpha . h holds
a . n = n |^ (h ") ) implies ex beta being Homomorphism of (semidirect_product (N,H,alpha)),G st
( ( for gh, gn being Element of G
for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh ) & beta is bijective ) )
assume A2: for h, n being Element of G st h in H & n in N holds
for a being Homomorphism of N,N st a = alpha . h holds
a . n = n |^ (h ") ; :: thesis: ex beta being Homomorphism of (semidirect_product (N,H,alpha)),G st
( ( for gh, gn being Element of G
for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh ) & beta is bijective )
set S = semidirect_product (N,H,alpha);
consider beta being Function of (semidirect_product (N,H,alpha)),G such that
A3: ( ( for n, h being Element of G st n in N & h in H holds
beta . <*n,h*> = n * h ) & ( beta is one-to-one implies N /\ H = (1). G ) & ( N /\ H = (1). G implies beta is one-to-one ) ) by Th60;
for x, y being Element of (semidirect_product (N,H,alpha)) holds beta . (x * y) = (beta . x) * (beta . y)

proof

let x, y be Element of (semidirect_product (N,H,alpha)); :: thesis: beta . (x * y) = (beta . x) * (beta . y)
consider n1 being Element of N, a1 being Element of H such that
B1: x = <*n1,a1*> by Th12;
reconsider ga1 = a1, gn1 = n1 as Element of G by GROUP_2:42;
consider n2 being Element of N, a2 being Element of H such that
B2: y = <*n2,a2*> by Th12;
reconsider ga2 = a2, gn2 = n2 as Element of G by GROUP_2:42;
B6: ( ga1 in H & gn1 in N & ga2 in H & gn2 in N ) ;
alpha . ga1 in AutGroup N by FUNCT_2:5;
then reconsider alphaga1 = alpha . ga1 as Homomorphism of N,N by AUTGROUP:def 1;
B7: gn2 |^ (ga1 ") = (((ga1 ") ") * gn2) * (ga1 ") by GROUP_3:def 2
.= (ga1 * gn2) * (ga1 ") ;
( beta . x = gn1 * ga1 & beta . y = gn2 * ga2 ) by A3, B2, B1, B6;
then B5: (beta . x) * (beta . y) = ((gn1 * ga1) * gn2) * ga2 by GROUP_1:def 3
.= (((gn1 * ga1) * gn2) * (1_ G)) * ga2 by GROUP_1:def 4
.= (((gn1 * ga1) * gn2) * ((ga1 ") * ga1)) * ga2 by GROUP_1:def 5
.= ((((gn1 * ga1) * gn2) * (ga1 ")) * ga1) * ga2 by GROUP_1:def 3
.= (((gn1 * (ga1 * gn2)) * (ga1 ")) * ga1) * ga2 by GROUP_1:def 3
.= ((gn1 * (gn2 |^ (ga1 "))) * ga1) * ga2 by B7, GROUP_1:def 3 ;
B4: ( alphaga1 . gn2 = gn2 |^ (ga1 ") & gn2 |^ (ga1 ") in N ) by A2, B6, AUTGROUP:1;
then B10: ( ga1 * ga2 in H & gn1 * (gn2 |^ (ga1 ")) in N ) by B6, GROUP_2:50;
reconsider alphaa1 = alpha . a1 as Homomorphism of N,N by AUTGROUP:def 1;
B11: n1 * (alphaa1 . n2) = the multF of G . (gn1,(alphaga1 . gn2))

proof

alphaa1 . n2 = alphaga1 . gn2 ;
then alphaga1 . gn2 in N ;
then alphaga1 . gn2 in G by GROUP_2:40;
then reconsider y = alphaga1 . gn2 as Element of G ;
reconsider x = alphaa1 . n2 as Element of N ;
gn1 * y = the multF of G . (gn1,(alphaga1 . gn2)) ;
hence n1 * (alphaa1 . n2) = the multF of G . (gn1,(alphaga1 . gn2)) by GROUP_2:43; :: thesis: verum

end;

x * y = <*(n1 * (alphaa1 . n2)),(a1 * a2)*> by B1, B2, Th14
.= <*(gn1 * (gn2 |^ (ga1 "))),(ga1 * ga2)*> by B4, B11, GROUP_2:43 ;
then beta . (x * y) = (gn1 * (gn2 |^ (ga1 "))) * (ga1 * ga2) by A3, B10
.= (beta . x) * (beta . y) by B5, GROUP_1:def 3 ;
hence beta . (x * y) = (beta . x) * (beta . y) ; :: thesis: verum

end;

then reconsider beta = beta as Homomorphism of (semidirect_product (N,H,alpha)),G by GROUP_6:def 6;
take beta ; :: thesis: ( ( for gh, gn being Element of G
for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh ) & beta is bijective )
thus for gh, gn being Element of G
for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh :: thesis: beta is bijective

proof

let gh, gn be Element of G; :: thesis: for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh
let h be Element of H; :: thesis: for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh
let n be Element of N; :: thesis: ( gh = h & gn = n implies beta . <*n,h*> = gn * gh )
assume B1: ( gh = h & gn = n ) ; :: thesis: beta . <*n,h*> = gn * gh
then ( gh in H & gn in N ) ;
hence beta . <*n,h*> = gn * gh by B1, A3; :: thesis: verum

end;

for y being Element of G ex x being Element of (semidirect_product (N,H,alpha)) st beta . x = y

proof

let y be Element of G; :: thesis: ex x being Element of (semidirect_product (N,H,alpha)) st beta . x = y
y in the carrier of G ;
then y in N * H by A1, Th64;
then consider n, h being Element of G such that
B1: ( y = n * h & n in N & h in H ) by GROUP_5:4;
reconsider h1 = h as Element of H by B1;
reconsider n1 = n as Element of N by B1;
reconsider x = <*n1,h1*> as Element of (semidirect_product (N,H,alpha)) by Th9;
take x ; :: thesis: beta . x = y
thus beta . x = y by B1, A3; :: thesis: verum

end;

then beta is onto by GROUP_6:58;
hence beta is bijective by A1, A3; :: thesis: verum