let G be addGroup; :: 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;
A7: (- g2) + (- a) in H2 + (- a) by A6, Th51, Th104;
- g = - (g1 + (- a)) by A3
.= (- (- a)) + (- (a + g2)) by A5, Th16
.= a + ((- g2) + (- a)) by Th16 ;
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;
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; :: 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