let G be Group; :: thesis: for H, F2 being Subgroup of G
for F1 being normal Subgroup of F2
for G2 being Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
let H, F2 be Subgroup of G; :: thesis: for F1 being normal Subgroup of F2
for G2 being Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
let F1 be normal Subgroup of F2; :: thesis: for G2 being Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
reconsider G2 = H /\ F2 as strict Subgroup of G ;
consider f being Function such that
A1: f = (nat_hom F1) | the carrier of H ;
reconsider f1 = nat_hom F1 as Function of the carrier of F2, the carrier of (F2 ./. F1) ;
A2: ( the carrier of F2 = carr F2 & the carrier of H = carr H ) ;
dom f1 = the carrier of F2 by FUNCT_2:def 1;
then A3: dom f = the carrier of F2 /\ the carrier of H by A1, RELAT_1:61
.= carr (F2 /\ H) by A2, GROUP_2:81
.= the carrier of (H /\ F2) ;
rng ((nat_hom F1) | the carrier of H) c= rng (nat_hom F1) by RELAT_1:70;
then reconsider f = f as Function of the carrier of (H /\ F2), the carrier of (F2 ./. F1) by A1, A3, FUNCT_2:2;
for a, b being Element of (H /\ F2) holds f . (a * b) = (f . a) * (f . b)
proof
let a, b be Element of (H /\ F2); :: thesis: f . (a * b) = (f . a) * (f . b)
A4: the carrier of (H /\ F2) = (carr H) /\ (carr F2) by GROUP_2:def 10;
then reconsider a9 = a, b9 = b as Element of F2 by XBOOLE_0:def 4;
b in carr H by A4, XBOOLE_0:def 4;
then A5: ((nat_hom F1) | the carrier of H) . b = (nat_hom F1) . b by FUNCT_1:49;
a * b in carr H by A4, XBOOLE_0:def 4;
then A6: ((nat_hom F1) | the carrier of H) . (a * b) = (nat_hom F1) . (a * b) by FUNCT_1:49;
H /\ F2 is Subgroup of F2 by GROUP_2:88;
then A7: a * b = a9 * b9 by GROUP_2:43;
a in carr H by A4, XBOOLE_0:def 4;
then ((nat_hom F1) | the carrier of H) . a = (nat_hom F1) . a by FUNCT_1:49;
hence f . (a * b) = (f . a) * (f . b) by A1, A7, A5, A6, GROUP_6:def 6; :: thesis: verum
end;
then reconsider f = f as Homomorphism of (H /\ F2),(F2 ./. F1) by GROUP_6:def 6;
A8: the carrier of H /\ the carrier of F2 = carr (H /\ F2) by A2, GROUP_2:81
.= the carrier of (H /\ F2) ;
A9: Ker f = H /\ F1
proof
reconsider L = Ker f as Subgroup of G by GROUP_2:56;
for g being Element of G holds
( g in L iff g in H /\ F1 )
proof
let x be Element of G; :: thesis: ( x in L iff x in H /\ F1 )
thus ( x in L implies x in H /\ F1 ) :: thesis: ( x in H /\ F1 implies x in L )
proof
assume A10: x in L ; :: thesis: x in H /\ F1
then x in carr (Ker f) by STRUCT_0:def 5;
then reconsider a = x as Element of (H /\ F2) ;
A11: the carrier of (H /\ F2) = (carr H) /\ (carr F2) by GROUP_2:def 10;
then reconsider a9 = a as Element of F2 by XBOOLE_0:def 4;
A12: a in carr H by A11, XBOOLE_0:def 4;
then A13: a in H by STRUCT_0:def 5;
((nat_hom F1) | the carrier of H) . a = (nat_hom F1) . a by A12, FUNCT_1:49;
then A14: f . a = a9 * F1 by A1, GROUP_6:def 8;
f . a = 1_ (F2 ./. F1) by A10, GROUP_6:41
.= carr F1 by GROUP_6:24 ;
then a9 in F1 by A14, GROUP_2:113;
hence x in H /\ F1 by A13, GROUP_2:82; :: thesis: verum
end;
thus ( x in H /\ F1 implies x in L ) :: thesis: verum
proof
reconsider F19 = F1 as Subgroup of G ;
A15: the carrier of H /\ the carrier of F1 = (carr H) /\ (carr F19)
.= the carrier of (H /\ F1) by GROUP_2:def 10 ;
assume x in H /\ F1 ; :: thesis: x in L
then A16: x in carr (H /\ F1) by STRUCT_0:def 5;
the carrier of F1 c= the carrier of F2 by GROUP_2:def 5;
then the carrier of (H /\ F1) c= the carrier of (H /\ F2) by A8, A15, XBOOLE_1:26;
then reconsider a = x as Element of (H /\ F2) by A16;
x in the carrier of F1 by A16, A15, XBOOLE_0:def 4;
then A17: a in F1 by STRUCT_0:def 5;
A18: the carrier of (H /\ F2) = (carr H) /\ (carr F2) by GROUP_2:def 10;
then reconsider a9 = a as Element of F2 by XBOOLE_0:def 4;
a in carr H by A18, XBOOLE_0:def 4;
then ((nat_hom F1) | the carrier of H) . a = (nat_hom F1) . a by FUNCT_1:49;
then f . a = a9 * F1 by A1, GROUP_6:def 8
.= carr F1 by A17, GROUP_2:113
.= 1_ (F2 ./. F1) by GROUP_6:24 ;
hence x in L by GROUP_6:41; :: thesis: verum
end;
end;
hence Ker f = H /\ F1 by GROUP_2:def 6; :: thesis: verum
end;
reconsider G1 = Ker f as normal Subgroup of G2 ;
G2 ./. G1, Image f are_isomorphic by GROUP_6:78;
hence for G2 being Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic by A9; :: thesis: verum