let O be set ; :: thesis: for G, H being strict GroupWithOperators of O
for N, L, G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f & L is strict normal StableSubgroup of G9 holds
( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )
let G, H be strict GroupWithOperators of O; :: thesis: for N, L, G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f & L is strict normal StableSubgroup of G9 holds
( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )
let N, L, G9 be strict StableSubgroup of G; :: thesis: for f being Homomorphism of G,H st N = Ker f & L is strict normal StableSubgroup of G9 holds
( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )
reconsider N9 = G9 /\ N as StableSubgroup of G9 by Lm33;
reconsider Gs9 = 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 & L is strict normal StableSubgroup of G9 implies ( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) ) )
reconsider L99 = L as Subgroup of G by Def7;
assume A1: N = Ker f ; :: thesis: ( not L is strict normal StableSubgroup of G9 or ( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) ) )
then consider H9 being strict StableSubgroup of H such that
A2: the carrier of H9 = f .: the carrier of G9 and
A3: f " the carrier of H9 = the carrier of (G9 "\/" N) and
( f is onto & G9 is normal implies H9 is normal ) by Th79;
reconsider f99 = f | the carrier of (G9 "\/" N) as Homomorphism of (G9 "\/" N),H9 by A3, Th89;
reconsider Ns = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by A1, Lm6;
(carr Gs9) * Ns = Ns * (carr Gs9) by GROUP_3:120;
then A4: G9 * N = N * G9 ;
A5: now :: thesis: for y being object st y in f .: the carrier of G9 holds
y in f .: (G9 * N)
let y be object ; :: thesis: ( y in f .: the carrier of G9 implies y in f .: (G9 * N) )
assume y in f .: the carrier of G9 ; :: thesis: y in f .: (G9 * N)
then consider x being object such that
A6: x in dom f and
A7: x in the carrier of G9 and
A8: y = f . x by FUNCT_1:def 6;
reconsider x = x as Element of G by A6;
consider x9 being set such that
A9: x9 = x * (1_ G) ;
A10: x9 in dom f by A6, A9, GROUP_1:def 4;
A11: y = (f . x) * (1_ H) by A8, GROUP_1:def 4
.= (f . x) * (f . (1_ G)) by Lm12
.= f . x9 by A9, GROUP_6:def 6 ;
f . (1_ G) = 1_ H by Lm12;
then 1_ G in Ker f by Th47;
then 1_ G in carr N by A1, STRUCT_0:def 5;
then x9 in G9 * N by A7, A9;
hence y in f .: (G9 * N) by A10, A11, FUNCT_1:def 6; :: thesis: verum
end;
A12: dom f = the carrier of G by FUNCT_2:def 1;
now :: thesis: for y being object st y in f .: (G9 * N) holds
y in f .: the carrier of G9
let y be object ; :: thesis: ( y in f .: (G9 * N) implies y in f .: the carrier of G9 )
assume y in f .: (G9 * N) ; :: thesis: y in f .: the carrier of G9
then consider x being object such that
A13: x in dom f and
A14: x in G9 * N and
A15: y = f . x by FUNCT_1:def 6;
reconsider x = x as Element of G by A13;
consider g1, g2 being Element of G such that
A16: x = g1 * g2 and
A17: g1 in carr G9 and
A18: g2 in carr N by A14;
A19: g2 in N by A18, STRUCT_0:def 5;
y = (f . g1) * (f . g2) by A15, A16, GROUP_6:def 6
.= (f . g1) * (1_ H) by A1, A19, Th47
.= f . g1 by GROUP_1:def 4 ;
hence y in f .: the carrier of G9 by A12, A17, FUNCT_1:def 6; :: thesis: verum
end;
then f .: the carrier of G9 = f .: (G9 * N) by A5, TARSKI:2;
then A20: ( f99 .: the carrier of (G9 "\/" N) = f .: the carrier of (G9 "\/" N) & the carrier of H9 = f .: the carrier of (G9 "\/" N) ) by A2, A4, Th30, RELAT_1:129;
A21: now :: thesis: for x being object st x in f99 " (f .: the carrier of L) holds
x in L * N
let x be object ; :: thesis: ( x in f99 " (f .: the carrier of L) implies x in L * N )
assume x in f99 " (f .: the carrier of L) ; :: thesis: x in L * N
then A22: x in the carrier of (G9 "\/" N) /\ (f " (f .: the carrier of L)) by FUNCT_1:70;
then x in f " (f .: the carrier of L) by XBOOLE_0:def 4;
then f . x in f .: the carrier of L by FUNCT_1:def 7;
then consider g1 being object such that
A23: g1 in dom f and
A24: g1 in the carrier of L and
A25: f . x = f . g1 by 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 A1, STRUCT_0:def 5;
hence x in L * N by A24, A26; :: thesis: verum
end;
reconsider f9 = f | the carrier of G9 as Homomorphism of G9,H9 by A2, Th89;
A27: now :: thesis: for x being object st x in the carrier of N9 holds
x in { a where a is Element of G9 : f9 . a = 1_ H9 }
let x be object ; :: thesis: ( x in the carrier of N9 implies x in { a where a is Element of G9 : f9 . a = 1_ H9 } )
assume x in the carrier of N9 ; :: thesis: x in { a where a is Element of G9 : f9 . a = 1_ H9 }
then A28: x in (carr G9) /\ (carr N) by Def25;
then reconsider a9 = x as Element of G9 by XBOOLE_0:def 4;
reconsider a99 = a9 as Element of G by Th2;
x in carr N by A28, XBOOLE_0:def 4;
then x in N by STRUCT_0:def 5;
then f . a99 = 1_ H by A1, Th47;
then f . a9 = 1_ H9 by Th4;
then f9 . a9 = 1_ H9 by FUNCT_1:49;
hence x in { a where a is Element of G9 : f9 . a = 1_ H9 } ; :: thesis: verum
end;
assume A29: L is strict normal StableSubgroup of G9 ; :: thesis: ( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )
then reconsider L9 = L as strict StableSubgroup of G9 ;
reconsider N1 = L "\/" N as StableSubgroup of G9 "\/" N by A29, Th38;
(carr L99) * Ns = Ns * (carr L99) by GROUP_3:120;
then A30: L * N = N * L ;
now :: thesis: for x being object st x in { a where a is Element of G9 : f9 . a = 1_ H9 } holds
x in the carrier of N9
let x be object ; :: thesis: ( x in { a where a is Element of G9 : f9 . a = 1_ H9 } implies x in the carrier of N9 )
assume x in { a where a is Element of G9 : f9 . a = 1_ H9 } ; :: thesis: x in the carrier of N9
then consider a being Element of G9 such that
A31: x = a and
A32: f9 . a = 1_ H9 ;
reconsider a = a as Element of G by Th2;
f . a = 1_ H9 by A32, FUNCT_1:49;
then f . a = 1_ H by Th4;
then x in N by A1, A31, Th47;
then x in carr N by STRUCT_0:def 5;
then x in (carr G9) /\ (carr N) by A31, XBOOLE_0:def 4;
hence x in the carrier of N9 by Def25; :: thesis: verum
end;
then the carrier of N9 = { a where a is Element of G9 : f9 . a = 1_ H9 } by A27, TARSKI:2;
then A33: N9 = Ker f9 by Def21;
then consider H99 being strict StableSubgroup of H9 such that
A34: the carrier of H99 = f9 .: the carrier of L9 and
A35: f9 " the carrier of H99 = the carrier of (L9 "\/" N9) and
A36: ( f9 is onto & L9 is normal implies H99 is normal ) by Th79;
consider N2 being strict StableSubgroup of G9 such that
A37: the carrier of N2 = f9 " the carrier of H99 and
A38: ( H99 is normal implies ( N9 is normal StableSubgroup of N2 & N2 is normal ) ) by A33, Th78;
( f9 .: the carrier of G9 = f .: the carrier of G9 & H9 is strict StableSubgroup of H9 ) by Lm3, RELAT_1:129;
then Image f9 = H9 by A2, Def22;
then A39: rng f9 = the carrier of H9 by Th49;
then reconsider H99 = H99 as normal StableSubgroup of H9 by A29, A36;
A40: N2 = L9 "\/" N9 by A35, A37, Lm4;
hence L "\/" (G9 /\ N) is normal StableSubgroup of G9 by A29, A36, A38, A39, Th86; :: thesis: ( L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )
set l = nat_hom H99;
set f1 = (nat_hom H99) * f99;
A41: N2 = L "\/" (G9 /\ N) by A40, Th86;
A42: L "\/" N is StableSubgroup of G9 "\/" N by A29, Th38;
A43: now :: thesis: for x being object st x in L * N holds
x in f99 " (f .: the carrier of L)
let x be object ; :: thesis: ( x in L * N implies x in f99 " (f .: the carrier of L) )
assume A44: x in L * N ; :: thesis: x in f99 " (f .: the carrier of L)
then consider g1, g2 being Element of G such that
A45: x = g1 * g2 and
A46: g1 in carr L and
A47: g2 in carr N ;
A48: g2 in N by A47, STRUCT_0:def 5;
f . x = (f . g1) * (f . g2) by A45, GROUP_6:def 6
.= (f . g1) * (1_ H) by A1, A48, Th47
.= f . g1 by GROUP_1:def 4 ;
then A49: f . x in f .: the carrier of L by A12, A46, FUNCT_1:def 6;
L "\/" N is Subgroup of G9 "\/" N by A42, Def7;
then A50: the carrier of (L "\/" N) c= the carrier of (G9 "\/" N) by GROUP_2:def 5;
A51: x in the carrier of (L "\/" N) by A30, A44, Th30;
then x in G9 "\/" N by A50, STRUCT_0:def 5;
then x in G by Th1;
then x in dom f by A12, STRUCT_0:def 5;
then x in f " (f .: the carrier of L) by A49, FUNCT_1:def 7;
then x in the carrier of (G9 "\/" N) /\ (f " (f .: the carrier of L)) by A51, A50, XBOOLE_0:def 4;
hence x in f99 " (f .: the carrier of L) by FUNCT_1:70; :: thesis: verum
end;
L is Subgroup of G9 by A29, Def7;
then the carrier of L c= the carrier of G9 by GROUP_2:def 5;
then f9 .: the carrier of L = f .: the carrier of L by RELAT_1:129;
then f99 " (f9 .: the carrier of L) = L * N by A21, A43, TARSKI:2;
then A52: f99 " the carrier of H99 = the carrier of N1 by A34, A30, Th30;
A53: f99 " the carrier of (Ker (nat_hom H99)) = f99 " the carrier of H99 by Th48;
then the carrier of (Ker ((nat_hom H99) * f99)) = the carrier of N1 by A52, Th88;
hence L "\/" N is normal StableSubgroup of G9 "\/" N by Lm4; :: thesis: for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic
A54: Ker ((nat_hom H99) * f99) = N1 by A52, A53, Lm4, Th88;
now :: thesis: for N19 being strict normal StableSubgroup of G9 "\/" N
for N29 being strict normal StableSubgroup of G9 st N19 = L "\/" N & N29 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic
set f2 = (nat_hom H99) * f9;
let N19 be strict normal StableSubgroup of G9 "\/" N; :: thesis: for N29 being strict normal StableSubgroup of G9 st N19 = L "\/" N & N29 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic
let N29 be strict normal StableSubgroup of G9; :: thesis: ( N19 = L "\/" N & N29 = L "\/" (G9 /\ N) implies (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic )
assume A55: N19 = L "\/" N ; :: thesis: ( N29 = L "\/" (G9 /\ N) implies (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic )
( f99 .: the carrier of (G9 "\/" N) = f9 .: the carrier of G9 & ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) = (nat_hom H99) .: (f99 .: the carrier of (G9 "\/" N)) ) by A2, A20, RELAT_1:126, RELAT_1:129;
then A56: ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) = ((nat_hom H99) * f9) .: the carrier of G9 by RELAT_1:126;
A57: f9 " the carrier of (Ker (nat_hom H99)) = f9 " the carrier of H99 by Th48;
assume N29 = L "\/" (G9 /\ N) ; :: thesis: (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic
then A58: N29 = Ker ((nat_hom H99) * f9) by A37, A41, A57, Lm4, Th88;
the carrier of (Image ((nat_hom H99) * f99)) = ((nat_hom H99) * f99) .: the carrier of (G9 "\/" N) by Def22
.= the carrier of (Image ((nat_hom H99) * f9)) by A56, Def22 ;
then A59: Image ((nat_hom H99) * f99) = Image ((nat_hom H99) * f9) by Lm4;
( (G9 "\/" N) ./. (Ker ((nat_hom H99) * f99)), Image ((nat_hom H99) * f99) are_isomorphic & Image ((nat_hom H99) * f9),G9 ./. (Ker ((nat_hom H99) * f9)) are_isomorphic ) by Th59;
hence (G9 "\/" N) ./. N19,G9 ./. N29 are_isomorphic by A54, A55, A59, A58, Th55; :: thesis: verum
end;
hence for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ; :: thesis: verum