Metamath Proof Explorer


Theorem qusabl

Description: If Y is a subgroup of the abelian group G , then H = G / Y is an abelian group. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypothesis qusabl.h H = G / 𝑠 G ~ QG S
Assertion qusabl G Abel S SubGrp G H Abel

Proof

Step Hyp Ref Expression
1 qusabl.h H = G / 𝑠 G ~ QG S
2 ablnsg G Abel NrmSGrp G = SubGrp G
3 2 eleq2d G Abel S NrmSGrp G S SubGrp G
4 3 biimpar G Abel S SubGrp G S NrmSGrp G
5 1 qusgrp S NrmSGrp G H Grp
6 4 5 syl G Abel S SubGrp G H Grp
7 vex x V
8 7 elqs x Base G / G ~ QG S a Base G x = a G ~ QG S
9 1 a1i G Abel S SubGrp G H = G / 𝑠 G ~ QG S
10 eqidd G Abel S SubGrp G Base G = Base G
11 ovexd G Abel S SubGrp G G ~ QG S V
12 simpl G Abel S SubGrp G G Abel
13 9 10 11 12 qusbas G Abel S SubGrp G Base G / G ~ QG S = Base H
14 13 eleq2d G Abel S SubGrp G x Base G / G ~ QG S x Base H
15 8 14 bitr3id G Abel S SubGrp G a Base G x = a G ~ QG S x Base H
16 vex y V
17 16 elqs y Base G / G ~ QG S b Base G y = b G ~ QG S
18 13 eleq2d G Abel S SubGrp G y Base G / G ~ QG S y Base H
19 17 18 bitr3id G Abel S SubGrp G b Base G y = b G ~ QG S y Base H
20 15 19 anbi12d G Abel S SubGrp G a Base G x = a G ~ QG S b Base G y = b G ~ QG S x Base H y Base H
21 reeanv a Base G b Base G x = a G ~ QG S y = b G ~ QG S a Base G x = a G ~ QG S b Base G y = b G ~ QG S
22 eqid Base G = Base G
23 eqid + G = + G
24 22 23 ablcom G Abel a Base G b Base G a + G b = b + G a
25 24 3expb G Abel a Base G b Base G a + G b = b + G a
26 25 adantlr G Abel S SubGrp G a Base G b Base G a + G b = b + G a
27 26 eceq1d G Abel S SubGrp G a Base G b Base G a + G b G ~ QG S = b + G a G ~ QG S
28 4 adantr G Abel S SubGrp G a Base G b Base G S NrmSGrp G
29 simprl G Abel S SubGrp G a Base G b Base G a Base G
30 simprr G Abel S SubGrp G a Base G b Base G b Base G
31 eqid + H = + H
32 1 22 23 31 qusadd S NrmSGrp G a Base G b Base G a G ~ QG S + H b G ~ QG S = a + G b G ~ QG S
33 28 29 30 32 syl3anc G Abel S SubGrp G a Base G b Base G a G ~ QG S + H b G ~ QG S = a + G b G ~ QG S
34 1 22 23 31 qusadd S NrmSGrp G b Base G a Base G b G ~ QG S + H a G ~ QG S = b + G a G ~ QG S
35 28 30 29 34 syl3anc G Abel S SubGrp G a Base G b Base G b G ~ QG S + H a G ~ QG S = b + G a G ~ QG S
36 27 33 35 3eqtr4d G Abel S SubGrp G a Base G b Base G a G ~ QG S + H b G ~ QG S = b G ~ QG S + H a G ~ QG S
37 oveq12 x = a G ~ QG S y = b G ~ QG S x + H y = a G ~ QG S + H b G ~ QG S
38 oveq12 y = b G ~ QG S x = a G ~ QG S y + H x = b G ~ QG S + H a G ~ QG S
39 38 ancoms x = a G ~ QG S y = b G ~ QG S y + H x = b G ~ QG S + H a G ~ QG S
40 37 39 eqeq12d x = a G ~ QG S y = b G ~ QG S x + H y = y + H x a G ~ QG S + H b G ~ QG S = b G ~ QG S + H a G ~ QG S
41 36 40 syl5ibrcom G Abel S SubGrp G a Base G b Base G x = a G ~ QG S y = b G ~ QG S x + H y = y + H x
42 41 rexlimdvva G Abel S SubGrp G a Base G b Base G x = a G ~ QG S y = b G ~ QG S x + H y = y + H x
43 21 42 syl5bir G Abel S SubGrp G a Base G x = a G ~ QG S b Base G y = b G ~ QG S x + H y = y + H x
44 20 43 sylbird G Abel S SubGrp G x Base H y Base H x + H y = y + H x
45 44 ralrimivv G Abel S SubGrp G x Base H y Base H x + H y = y + H x
46 eqid Base H = Base H
47 46 31 isabl2 H Abel H Grp x Base H y Base H x + H y = y + H x
48 6 45 47 sylanbrc G Abel S SubGrp G H Abel