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 " );
A1:
a * H2 <> {}
by Th130;
consider x being Element of a * H2;
reconsider x = x as Element of G by A1, Lm1;
A2:
x * (a " ) in (a * H2) * (a " )
by A1, Th34;
A3:
now 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 A4:
g1 in (a * H2) * (a " )
and A5:
g2 in (a * H2) * (a " )
;
:: thesis: g1 * g2 in (a * H2) * (a " )consider g being
Element of
G such that A6:
g1 = g * (a " )
and A7:
g in a * H2
by A4, Th34;
(a * H2) * (a " ) = a * (H2 * (a " ))
by Th14;
then consider b being
Element of
G such that A8:
g2 = a * b
and A9:
b in H2 * (a " )
by A5, Th33;
consider h being
Element of
G such that A10:
g = a * h
and A11:
h in H2
by A7, Th125;
consider c being
Element of
G such that A12:
b = c * (a " )
and A13:
c in H2
by A9, Th126;
A14:
g1 * g2 =
(a * h) * ((a " ) * (a * (c * (a " ))))
by A6, A8, A10, A12, GROUP_1:def 4
.=
(a * h) * (((a " ) * a) * (c * (a " )))
by GROUP_1:def 4
.=
(a * h) * ((1_ G) * (c * (a " )))
by GROUP_1:def 6
.=
(a * h) * (c * (a " ))
by GROUP_1:def 5
.=
((a * h) * c) * (a " )
by GROUP_1:def 4
.=
(a * (h * c)) * (a " )
by GROUP_1:def 4
;
h * c in H2
by A11, A13, Th59;
then
a * (h * c) in a * H2
by Th125;
hence
g1 * g2 in (a * H2) * (a " )
by A14, Th34;
:: thesis: verum end;
hence
ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a " )
by A2, A3, Th61; :: thesis: verum