let G be addGroup; 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; 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; 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;
A8:
now 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;
( 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)
;
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;
A19:
a + (h + c) in a + H2
by A14, A18, Th50, Th103;
g1 + g2 =
(a + h) + ((- a) + (a + (c + (- a))))
by A11, A15, A13, A17, RLVECT_1:def 3
.=
(a + h) + (((- a) + a) + (c + (- a)))
by RLVECT_1:def 3
.=
(a + h) + ((0_ G) + (c + (- a)))
by Def5
.=
(a + h) + (c + (- a))
by Def4
.=
((a + h) + c) + (- a)
by RLVECT_1:def 3
.=
(a + (h + c)) + (- a)
by RLVECT_1:def 3
;
hence
g1 + g2 in (a + H2) + (- a)
by A19, Th28;
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; verum