let G be Group; :: thesis: for H being Subgroup of G
for N being normal Subgroup of G st H,N are_complements_in G holds
ex phi being Homomorphism of H,(G ./. N) st
( ( for h being Element of H
for g being Element of G st g = h holds
phi . h = g * N ) & phi is bijective )
let H be Subgroup of G; :: thesis: for N being normal Subgroup of G st H,N are_complements_in G holds
ex phi being Homomorphism of H,(G ./. N) st
( ( for h being Element of H
for g being Element of G st g = h holds
phi . h = g * N ) & phi is bijective )
let N be normal Subgroup of G; :: thesis: ( H,N are_complements_in G implies ex phi being Homomorphism of H,(G ./. N) st
( ( for h being Element of H
for g being Element of G st g = h holds
phi . h = g * N ) & phi is bijective ) )
assume H,N are_complements_in G ; :: thesis: ex phi being Homomorphism of H,(G ./. N) st
( ( for h being Element of H
for g being Element of G st g = h holds
phi . h = g * N ) & phi is bijective )
then A2: ( H * N = the carrier of G & H /\ N = (1). G ) ;
defpred S₁[ Element of H, Element of (G ./. N)] means ex g being Element of G st
( g = $1 & $2 = g * N );
A3: for x being Element of H ex y being Element of (G ./. N) st S₁[x,y]

proof

let x be Element of H; :: thesis: ex y being Element of (G ./. N) st S₁[x,y]
reconsider g = x as Element of G by GROUP_2:42;
take y = (nat_hom N) . g; :: thesis: S₁[x,y]
y = g * N by GROUP_6:def 8;
hence S₁[x,y] ; :: thesis: verum

end;

consider phi being Function of H,(G ./. N) such that
A4: for x being Element of H holds S₁[x,phi . x] from FUNCT_2:sch 3(A3);
A5: for h being Element of H
for g being Element of G st g = h holds
phi . h = g * N

proof

let h be Element of H; :: thesis: for g being Element of G st g = h holds
phi . h = g * N
let g be Element of G; :: thesis: ( g = h implies phi . h = g * N )
assume B1: g = h ; :: thesis: phi . h = g * N
S₁[h,phi . h] by A4;
hence phi . h = g * N by B1; :: thesis: verum

end;

for a, b being Element of H holds phi . (a * b) = (phi . a) * (phi . b)

proof

let a, b be Element of H; :: thesis: phi . (a * b) = (phi . a) * (phi . b)
reconsider g1 = a, g2 = b as Element of G by GROUP_2:42;
B1: phi . a = g1 * N by A5
.= (nat_hom N) . g1 by GROUP_6:def 8 ;
B2: phi . b = g2 * N by A5
.= (nat_hom N) . g2 by GROUP_6:def 8 ;
a * b = g1 * g2 by GROUP_2:43;
then phi . (a * b) = (g1 * g2) * N by A5
.= (nat_hom N) . (g1 * g2) by GROUP_6:def 8 ;
hence phi . (a * b) = (phi . a) * (phi . b) by B1, B2, GROUP_6:def 6; :: thesis: verum

end;

then reconsider phi = phi as Homomorphism of H,(G ./. N) by GROUP_6:def 6;
take phi ; :: thesis: ( ( for h being Element of H
for g being Element of G st g = h holds
phi . h = g * N ) & phi is bijective )
thus for h being Element of H
for g being Element of G st g = h holds
phi . h = g * N by A5; :: thesis: phi is bijective
for y being Element of (G ./. N) ex x being Element of H st phi . x = y

proof

let y be Element of (G ./. N); :: thesis: ex x being Element of H st phi . x = y
y in G ./. N ;
then consider g being Element of G such that
Z1: ( y = g * N & y = N * g ) by GROUP_6:23;
consider h, n being Element of G such that
Z2: ( g = h * n & h in H & n in N ) by A2, GROUP_5:4;
reconsider x = h as Element of H by Z2;
take x ; :: thesis: phi . x = y
g * N = h * (n * N) by Z2, GROUP_2:105
.= h * N by Z2, GROUP_2:113 ;
hence phi . x = y by A5, Z1; :: thesis: verum

end;

then A3: phi is onto by GROUP_6:58;
for a, b being Element of H st phi . a = phi . b holds
a = b

proof

let a, b be Element of H; :: thesis: ( phi . a = phi . b implies a = b )
assume Z1: phi . a = phi . b ; :: thesis: a = b
reconsider ga = a, gb = b as Element of G by GROUP_2:42;
ga * N = phi . a by A5
.= gb * N by Z1, A5 ;
then Z2: (gb ") * ga in N by GROUP_2:114;
gb in H ;
then ( gb " in H & ga in H ) by GROUP_2:51;
then (gb ") * ga in H by GROUP_2:50;
then (gb ") * ga = 1_ G by A2, Z2, GROUP_2:82, GROUP_5:1;
then ga = gb * (1_ G) by GROUP_1:13
.= gb by GROUP_1:def 4 ;
hence a = b ; :: thesis: verum

end;

then phi is one-to-one by GROUP_6:1;
hence phi is bijective by A3; :: thesis: verum