let G be Group; :: thesis: for N being strict normal Subgroup of G
for phi being Automorphism of G st Image (phi | N) = N holds
ex sigma being Automorphism of (G ./. N) st
for x being Element of G holds sigma . (x * N) = (phi . x) * N
let N be strict normal Subgroup of G; :: thesis: for phi being Automorphism of G st Image (phi | N) = N holds
ex sigma being Automorphism of (G ./. N) st
for x being Element of G holds sigma . (x * N) = (phi . x) * N
let phi be Automorphism of G; :: thesis: ( Image (phi | N) = N implies ex sigma being Automorphism of (G ./. N) st
for x being Element of G holds sigma . (x * N) = (phi . x) * N )
assume A1: Image (phi | N) = N ; :: thesis: ex sigma being Automorphism of (G ./. N) st
for x being Element of G holds sigma . (x * N) = (phi . x) * N
defpred S₁[ set , set ] means ex a being Element of G st
( $1 = a * N & $2 = (phi . a) * N );
A2: for x being Element of (G ./. N) ex y being Element of (G ./. N) st S₁[x,y]

proof

let x be Element of (G ./. N); :: thesis: ex y being Element of (G ./. N) st S₁[x,y]
x in Cosets N ;
then consider a being Element of G such that
B1: x = a * N by GROUP_2:def 15;
(phi . a) * N in Cosets N by GROUP_2:def 15;
then consider y being Element of (G ./. N) such that
B2: y = (phi . a) * N ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by B1, B2; :: thesis: verum

end;

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

proof

let a be Element of G; :: thesis: sigma . (a * N) = (phi . a) * N
a * N in Cosets N by GROUP_2:def 15;
then consider x being Element of (G ./. N) such that
B1: x = a * N ;
consider b being Element of G such that
B2: ( x = b * N & sigma . x = (phi . b) * N ) by A3;
consider n being Element of G such that
B3: ( n = (b ") * a & n in N ) by B1, B2, GROUP_2:114;
B4: b * n = b * ((b ") * a) by B3
.= (b * (b ")) * a by GROUP_1:def 3
.= (1_ G) * a by GROUP_1:def 5
.= a by GROUP_1:def 4 ;
( dom phi = the carrier of G & n in N ) by B3, FUNCT_2:def 1;
then phi . n in phi .: the carrier of N by FUNCT_1:def 6;
then phi . n in the carrier of (phi .: N) by GRSOLV_1:8;
then B5: phi . n in N by A1, GRSOLV_1:def 3;
(phi . a) * N = (phi . (b * n)) * N by B4
.= ((phi . b) * (phi . n)) * N by GROUP_6:def 6
.= (phi . b) * ((phi . n) * N) by GROUP_2:105
.= (phi . b) * N by B5, GROUP_2:113
.= sigma . x by B2 ;
hence sigma . (a * N) = (phi . a) * N by B1; :: thesis: verum

end;

for x, y being Element of (G ./. N) holds sigma . (x * y) = (sigma . x) * (sigma . y)

proof

let x, y be Element of (G ./. N); :: thesis: sigma . (x * y) = (sigma . x) * (sigma . y)
consider a being Element of G such that
B1: ( x = a * N & sigma . x = (phi . a) * N ) by A3;
consider b being Element of G such that
B2: ( y = b * N & sigma . y = (phi . b) * N ) by A3;
B3: for g1, g2 being Element of G holds (g1 * N) * (g2 * N) = (g1 * g2) * N

proof

let g1, g2 be Element of G; :: thesis: (g1 * N) * (g2 * N) = (g1 * g2) * N
(g1 * N) * (g2 * N) = (g1 * N) * (N * g2) by GROUP_3:117
.= ((g1 * N) * N) * g2 by GROUP_3:11
.= (g1 * (N * N)) * g2 by GROUP_4:45
.= (g1 * N) * g2 by GROUP_2:76
.= g1 * (N * g2) by GROUP_2:106
.= g1 * (g2 * N) by GROUP_3:117
.= (g1 * g2) * N by GROUP_2:105 ;
hence (g1 * N) * (g2 * N) = (g1 * g2) * N ; :: thesis: verum

end;

B4: x * y = (@ x) * (@ y) by GROUP_6:def 3
.= (a * N) * (b * N) by B1, B2
.= (a * b) * N by B3 ;
B5: (sigma . x) * (sigma . y) = (phi . (a * b)) * N

proof

(sigma . x) * (sigma . y) = (@ (sigma . x)) * (@ (sigma . y)) by GROUP_6:def 3
.= ((phi . a) * N) * ((phi . b) * N) by B1, B2
.= ((phi . a) * (phi . b)) * N by B3
.= (phi . (a * b)) * N by GROUP_6:def 6 ;
hence (sigma . x) * (sigma . y) = (phi . (a * b)) * N ; :: thesis: verum

end;

sigma . (x * y) = sigma . ((a * b) * N) by B4
.= (phi . (a * b)) * N by A4
.= (sigma . x) * (sigma . y) by B5 ;
hence sigma . (x * y) = (sigma . x) * (sigma . y) ; :: thesis: verum

end;

then reconsider sigma = sigma as Homomorphism of (G ./. N),(G ./. N) by GROUP_6:def 6;
sigma is bijective

proof

B1: for x being Element of G holds
( x * N in Ker sigma iff x in N )

proof

let x be Element of G; :: thesis: ( x * N in Ker sigma iff x in N )
reconsider z = x * N as Element of (G ./. N) by GROUP_2:def 15;
C1: (phi ") . (phi . x) = x by FUNCT_2:26;
thus ( x * N in Ker sigma implies x in N ) :: thesis: ( x in N implies x * N in Ker sigma )

proof

assume x * N in Ker sigma ; :: thesis: x in N
then D1: sigma . z = 1_ (G ./. N) by GROUP_6:41;
(phi . x) * N = sigma . (x * N) by A4
.= carr N by D1, GROUP_6:24 ;
then phi . x in Image (phi | N) by A1, GROUP_2:113;
then D2: phi . x in phi .: N by GRSOLV_1:def 3;
consider psi being Automorphism of G such that
D3: psi = phi " and
Image (phi | (Image (psi | N))) = multMagma(# the carrier of N, the multF of N #) by Th17;
reconsider i = id the carrier of G as Automorphism of G by GROUP_6:38;
( the carrier of G <> {} & phi is onto ) ;
then D4: psi * phi = id the carrier of G by D3, FUNCT_2:29;
dom psi = the carrier of G by FUNCT_2:def 1;
then psi . (phi . x) in psi .: the carrier of (phi .: N) by D2, FUNCT_1:def 6;
then psi . (phi . x) in the carrier of (psi .: (phi .: N)) by GRSOLV_1:8;
then x in i .: N by C1, D3, D4, Th72;
then D5: x in (id the carrier of G) .: the carrier of N by GRSOLV_1:8;
the carrier of N is Subset of the carrier of G by GROUP_2:def 5;
hence x in N by D5; :: thesis: verum

end;

thus ( x in N implies x * N in Ker sigma ) :: thesis: verum

proof

assume x in N ; :: thesis: x * N in Ker sigma
then D1: x * N = carr N by GROUP_2:113
.= 1_ (G ./. N) by GROUP_6:24 ;
then sigma . (x * N) = 1_ (G ./. N) by GROUP_6:31;
hence x * N in Ker sigma by D1, GROUP_6:41; :: thesis: verum

end;

end;

for x being Element of (G ./. N) holds
( x in Ker sigma iff x in (1). (G ./. N) )

proof

let x be Element of (G ./. N); :: thesis: ( x in Ker sigma iff x in (1). (G ./. N) )
thus ( x in Ker sigma implies x in (1). (G ./. N) ) :: thesis: ( x in (1). (G ./. N) implies x in Ker sigma )

proof

assume C1: x in Ker sigma ; :: thesis: x in (1). (G ./. N)
x in G ./. N ;
then consider g being Element of G such that
C2: x = g * N by GROUP_2:def 15;
g * N = carr N by B1, C1, C2, GROUP_2:113;
then g * N = 1_ (G ./. N) by GROUP_6:24;
then g * N in {(1_ (G ./. N))} by TARSKI:def 1;
hence x in (1). (G ./. N) by C2, GROUP_2:def 7; :: thesis: verum

end;

thus ( x in (1). (G ./. N) implies x in Ker sigma ) :: thesis: verum

proof

assume x in (1). (G ./. N) ; :: thesis: x in Ker sigma
then x in {(1_ (G ./. N))} by GROUP_2:def 7;
then x = 1_ (G ./. N) by TARSKI:def 1;
then sigma . x = 1_ (G ./. N) by GROUP_6:31;
hence x in Ker sigma by GROUP_6:41; :: thesis: verum

end;

end;

then Ker sigma = (1). (G ./. N) ;
hence sigma is one-to-one by GROUP_6:56; :: according to FUNCT_2:def 4 :: thesis: sigma is onto
for y being Element of (G ./. N) holds y in Image sigma

proof

let y be Element of (G ./. N); :: thesis: y in Image sigma
y in G ./. N ;
then consider b being Element of G such that
C1: y = b * N by GROUP_2:def 15;
reconsider psi = phi " as Automorphism of G by GROUP_6:62;
consider a being Element of G such that
C2: a = psi . b ;
a * N in G ./. N by GROUP_2:def 15;
then consider x being Element of (G ./. N) such that
C3: x = a * N ;
C4: phi . a = phi . ((phi ") . b) by C2
.= b by Th4 ;
sigma . x = sigma . (a * N) by C3
.= (phi . a) * N by A4
.= b * N by C4
.= y by C1 ;
hence y in Image sigma by GROUP_6:45; :: thesis: verum

end;

hence sigma is onto by GROUP_2:62, GROUP_6:57; :: thesis: verum

end;

then reconsider sigma = sigma as Automorphism of (G ./. N) ;
take sigma ; :: thesis: for x being Element of G holds sigma . (x * N) = (phi . x) * N
let x be Element of G; :: thesis: sigma . (x * N) = (phi . x) * N
thus sigma . (x * N) = (phi . x) * N by A4; :: thesis: verum