let G be Group; :: thesis: for a being Element of G
for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")
let a be Element of G; :: thesis: for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")
let H2 be Subgroup of G; :: thesis: ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")
set A = (a * H2) * (a ");
set x = the Element of a * H2;
A1: a * H2 <> {} by Th108;
then reconsider x = the Element of a * H2 as Element of G by Lm1;
A2: now :: thesis: for g being Element of G st g in (a * H2) * (a ") holds
g " in (a * H2) * (a ")
let g be Element of G; :: thesis: ( g in (a * H2) * (a ") implies g " in (a * H2) * (a ") )
assume g in (a * H2) * (a ") ; :: thesis: g " in (a * H2) * (a ")
then consider g1 being Element of G such that
A3: g = g1 * (a ") and
A4: g1 in a * H2 by Th28;
consider g2 being Element of G such that
A5: g1 = a * g2 and
A6: g2 in H2 by A4, Th103;
g2 " in H2 by A6, Th51;
then A7: (g2 ") * (a ") in H2 * (a ") by Th104;
g " = ((a ") ") * ((a * g2) ") by A3, A5, GROUP_1:17
.= a * ((g2 ") * (a ")) by GROUP_1:17 ;
then g " in a * (H2 * (a ")) by A7, Th27;
hence g " in (a * H2) * (a ") by Th10; :: thesis: verum
end;
A8: now :: thesis: for g1, g2 being Element of G st g1 in (a * H2) * (a ") & g2 in (a * H2) * (a ") holds
g1 * g2 in (a * H2) * (a ")
let g1, g2 be Element of G; :: thesis: ( g1 in (a * H2) * (a ") & g2 in (a * H2) * (a ") implies g1 * g2 in (a * H2) * (a ") )
assume that
A9: g1 in (a * H2) * (a ") and
A10: g2 in (a * H2) * (a ") ; :: thesis: g1 * g2 in (a * H2) * (a ")
consider g being Element of G such that
A11: g1 = g * (a ") and
A12: g in a * H2 by A9, Th28;
consider h being Element of G such that
A13: g = a * h and
A14: h in H2 by A12, Th103;
(a * H2) * (a ") = a * (H2 * (a ")) by Th10;
then consider b being Element of G such that
A15: g2 = a * b and
A16: b in H2 * (a ") by A10, Th27;
consider c being Element of G such that
A17: b = c * (a ") and
A18: c in H2 by A16, Th104;
h * c in H2 by A14, A18, Th50;
then A19: a * (h * c) in a * H2 by Th103;
g1 * g2 = (a * h) * ((a ") * (a * (c * (a ")))) by A11, A15, A13, A17, GROUP_1:def 3
.= (a * h) * (((a ") * a) * (c * (a "))) by GROUP_1:def 3
.= (a * h) * ((1_ G) * (c * (a "))) by GROUP_1:def 5
.= (a * h) * (c * (a ")) by GROUP_1:def 4
.= ((a * h) * c) * (a ") by GROUP_1:def 3
.= (a * (h * c)) * (a ") by GROUP_1:def 3 ;
hence g1 * g2 in (a * H2) * (a ") by A19, Th28; :: thesis: verum
end;
x * (a ") in (a * H2) * (a ") by A1, Th28;
hence ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ") by A8, A2, Th52; :: thesis: verum