let O be set ; :: thesis: for G, H being GroupWithOperators of O
for N being StableSubgroup of G
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f holds
ex H9 being strict StableSubgroup of H st
( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )
let G, H be GroupWithOperators of O; :: thesis: for N being StableSubgroup of G
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f holds
ex H9 being strict StableSubgroup of H st
( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )
let N be StableSubgroup of G; :: thesis: for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f holds
ex H9 being strict StableSubgroup of H st
( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )
reconsider N9 = multMagma(# the carrier of N, the multF of N #) as strict Subgroup of G by Lm15;
let G9 be strict StableSubgroup of G; :: thesis: for f being Homomorphism of G,H st N = Ker f holds
ex H9 being strict StableSubgroup of H st
( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )
reconsider G99 = multMagma(# the carrier of G9, the multF of G9 #) as strict Subgroup of G by Lm15;
let f be Homomorphism of G,H; :: thesis: ( N = Ker f implies ex H9 being strict StableSubgroup of H st
( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) ) )
set A = { (f . g) where g is Element of G : g in G99 } ;
A1: ( G99 * N9 = G9 * N & N9 * G99 = N * G9 ) ;
1_ G in G99 by GROUP_2:46;
then f . (1_ G) in { (f . g) where g is Element of G : g in G99 } ;
then reconsider A = { (f . g) where g is Element of G : g in G99 } as non empty set ;
now :: thesis: for x being object st x in A holds
x in the carrier of H
let x be object ; :: thesis: ( x in A implies x in the carrier of H )
assume x in A ; :: thesis: x in the carrier of H
then ex g being Element of G st
( x = f . g & g in G99 ) ;
hence x in the carrier of H ; :: thesis: verum
end;
then reconsider A = A as Subset of H by TARSKI:def 3;
A2: now :: thesis: for h1, h2 being Element of H st h1 in A & h2 in A holds
h1 * h2 in A
let h1, h2 be Element of H; :: thesis: ( h1 in A & h2 in A implies h1 * h2 in A )
assume that
A3: h1 in A and
A4: h2 in A ; :: thesis: h1 * h2 in A
consider a being Element of G such that
A5: ( h1 = f . a & a in G99 ) by A3;
consider b being Element of G such that
A6: ( h2 = f . b & b in G99 ) by A4;
( f . (a * b) = h1 * h2 & a * b in G99 ) by A5, A6, GROUP_2:50, GROUP_6:def 6;
hence h1 * h2 in A ; :: thesis: verum
end;
A7: now :: thesis: for o being Element of O
for h being Element of H st h in A holds
(H ^ o) . h in A
let o be Element of O; :: thesis: for h being Element of H st h in A holds
(H ^ o) . h in A
let h be Element of H; :: thesis: ( h in A implies (H ^ o) . h in A )
assume h in A ; :: thesis: (H ^ o) . h in A
then consider g being Element of G such that
A8: h = f . g and
A9: g in G99 ;
g in the carrier of G99 by A9, STRUCT_0:def 5;
then g in G9 by STRUCT_0:def 5;
then (G ^ o) . g in G9 by Lm9;
then (G ^ o) . g in the carrier of G9 by STRUCT_0:def 5;
then A10: (G ^ o) . g in G99 by STRUCT_0:def 5;
(H ^ o) . h = f . ((G ^ o) . g) by A8, Def18;
hence (H ^ o) . h in A by A10; :: thesis: verum
end;
now :: thesis: for h being Element of H st h in A holds
h " in A
let h be Element of H; :: thesis: ( h in A implies h " in A )
assume h in A ; :: thesis: h " in A
then consider g being Element of G such that
A11: ( h = f . g & g in G99 ) ;
( g " in G99 & h " = f . (g ") ) by A11, Lm13, GROUP_2:51;
hence h " in A ; :: thesis: verum
end;
then consider H99 being strict StableSubgroup of H such that
A12: the carrier of H99 = A by A2, A7, Lm14;
assume A13: N = Ker f ; :: thesis: ex H9 being strict StableSubgroup of H st
( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )
then N9 is normal by Def10;
then A14: (carr G99) * N9 = N9 * (carr G99) by GROUP_3:120;
reconsider H9 = multMagma(# the carrier of H99, the multF of H99 #) as strict Subgroup of H by Lm15;
take H99 ; :: thesis: ( the carrier of H99 = f .: the carrier of G9 & f " the carrier of H99 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H99 is normal ) )
A15: now :: thesis: for h being Element of H holds
( ( h in A implies h in f .: the carrier of G9 ) & ( h in f .: the carrier of G9 implies h in A ) )
reconsider R = f as Relation of the carrier of G, the carrier of H ;
let h be Element of H; :: thesis: ( ( h in A implies h in f .: the carrier of G9 ) & ( h in f .: the carrier of G9 implies h in A ) )
hereby :: thesis: ( h in f .: the carrier of G9 implies h in A )
assume h in A ; :: thesis: h in f .: the carrier of G9
then consider g being Element of G such that
A16: h = f . g and
A17: g in G99 ;
A18: g in the carrier of G9 by A17, STRUCT_0:def 5;
dom f = the carrier of G by FUNCT_2:def 1;
then [g,h] in f by A16, FUNCT_1:1;
hence h in f .: the carrier of G9 by A18, RELSET_1:29; :: thesis: verum
end;
assume h in f .: the carrier of G9 ; :: thesis: h in A
then consider g being Element of G such that
A19: ( [g,h] in R & g in the carrier of G9 ) by RELSET_1:29;
( f . g = h & g in G99 ) by A19, FUNCT_1:1, STRUCT_0:def 5;
hence h in A ; :: thesis: verum
end;
hence A20: the carrier of H99 = f .: the carrier of G9 by A12, SUBSET_1:3; :: thesis: ( f " the carrier of H99 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H99 is normal ) )
A21: now :: thesis: for x being object st x in f " the carrier of H9 holds
x in G99 * N9
let x be object ; :: thesis: ( x in f " the carrier of H9 implies x in G99 * N9 )
assume A22: x in f " the carrier of H9 ; :: thesis: x in G99 * N9
then f . x in the carrier of H9 by FUNCT_1:def 7;
then consider g1 being object such that
A23: g1 in dom f and
A24: g1 in the carrier of G9 and
A25: f . g1 = f . x by A20, FUNCT_1:def 6;
reconsider g1 = g1, g2 = x as Element of G by A22, A23;
consider g3 being Element of G such that
A26: g2 = g1 * g3 by GROUP_1:15;
f . g2 = (f . g2) * (f . g3) by A25, A26, GROUP_6:def 6;
then f . g3 = 1_ H by GROUP_1:7;
then g3 in Ker f by Th47;
then g3 in the carrier of N by A13, STRUCT_0:def 5;
hence x in G99 * N9 by A24, A26; :: thesis: verum
end;
A27: dom f = the carrier of G by FUNCT_2:def 1;
now :: thesis: for x being object st x in G99 * N9 holds
x in f " the carrier of H9
let x be object ; :: thesis: ( x in G99 * N9 implies x in f " the carrier of H9 )
assume A28: x in G99 * N9 ; :: thesis: x in f " the carrier of H9
then consider g1, g2 being Element of G such that
A29: x = g1 * g2 and
A30: g1 in carr G9 and
A31: g2 in carr N9 ;
A32: g2 in Ker f by A13, A31, STRUCT_0:def 5;
f . x = (f . g1) * (f . g2) by A29, GROUP_6:def 6
.= (f . g1) * (1_ H) by A32, Th47
.= f . g1 by GROUP_1:def 4 ;
then f . x in f .: the carrier of G9 by A27, A30, FUNCT_1:def 6;
then x in f " (f .: the carrier of G9) by A27, A28, FUNCT_1:def 7;
hence x in f " the carrier of H9 by A12, A15, SUBSET_1:3; :: thesis: verum
end;
then f " the carrier of H9 = (carr G9) * (carr N) by A21, TARSKI:2;
hence f " the carrier of H99 = the carrier of (G9 "\/" N) by A14, A1, Th30; :: thesis: ( f is onto & G9 is normal implies H99 is normal )
now :: thesis: ( f is onto & G9 is normal implies H99 is normal )
assume that
A33: f is onto and
A34: G9 is normal ; :: thesis: H99 is normal
A35: G99 is normal by A34;
now :: thesis: for h1 being Element of H holds h1 * H9 c= H9 * h1
let h1 be Element of H; :: thesis: h1 * H9 c= H9 * h1
now :: thesis: for x being object st x in h1 * H9 holds
x in H9 * h1
let x be object ; :: thesis: ( x in h1 * H9 implies x in H9 * h1 )
assume x in h1 * H9 ; :: thesis: x in H9 * h1
then consider h2 being Element of H such that
A36: x = h1 * h2 and
A37: h2 in A by A12, GROUP_2:27;
set h29 = (h1 * h2) * (h1 ");
h2 in f .: the carrier of G9 by A15, A37;
then consider g2 being object such that
A38: g2 in dom f and
A39: g2 in the carrier of G99 and
A40: f . g2 = h2 by FUNCT_1:def 6;
rng f = the carrier of H by A33;
then consider g1 being object such that
A41: g1 in dom f and
A42: h1 = f . g1 by FUNCT_1:def 3;
reconsider g1 = g1, g2 = g2 as Element of G by A38, A41;
set g29 = (g1 * g2) * (g1 ");
(g1 * g2) * (g1 ") = (((g1 ") ") * g2) * (g1 ") ;
then A43: (g1 * g2) * (g1 ") = g2 |^ (g1 ") by GROUP_3:def 2;
g2 in G99 by A39, STRUCT_0:def 5;
then (g1 * g2) * (g1 ") in G99 |^ (g1 ") by A43, GROUP_3:58;
then A44: (g1 * g2) * (g1 ") in the carrier of (G99 |^ (g1 ")) by STRUCT_0:def 5;
G99 |^ (g1 ") is Subgroup of G99 by A35, GROUP_3:122;
then A45: the carrier of (G99 |^ (g1 ")) c= the carrier of G99 by GROUP_2:def 5;
(h1 * h2) * (h1 ") = ((f . g1) * (f . g2)) * (f . (g1 ")) by A40, A42, Lm13
.= (f . (g1 * g2)) * (f . (g1 ")) by GROUP_6:def 6
.= f . ((g1 * g2) * (g1 ")) by GROUP_6:def 6 ;
then (h1 * h2) * (h1 ") in f .: the carrier of G99 by A27, A44, A45, FUNCT_1:def 6;
then A46: (h1 * h2) * (h1 ") in A by A15;
((h1 * h2) * (h1 ")) * h1 = (h1 * h2) * ((h1 ") * h1) by GROUP_1:def 3
.= (h1 * h2) * (1_ H) by GROUP_1:def 5
.= x by A36, GROUP_1:def 4 ;
hence x in H9 * h1 by A12, A46, GROUP_2:28; :: thesis: verum
end;
hence h1 * H9 c= H9 * h1 ; :: thesis: verum
end;
then for H1 being strict Subgroup of H st H1 = multMagma(# the carrier of H99, the multF of H99 #) holds
H1 is normal by GROUP_3:118;
hence H99 is normal ; :: thesis: verum
end;
hence ( f is onto & G9 is normal implies H99 is normal ) ; :: thesis: verum