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 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
Assertion qusabl ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ Abel )

Proof

Step Hyp Ref Expression
1 qusabl.h 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
2 ablnsg ( 𝐺 ∈ Abel → ( NrmSGrp ‘ 𝐺 ) = ( SubGrp ‘ 𝐺 ) )
3 2 eleq2d ( 𝐺 ∈ Abel → ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) )
4 3 biimpar ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) )
5 1 qusgrp ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
6 4 5 syl ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ Grp )
7 vex 𝑥 ∈ V
8 7 elqs ( 𝑥 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑆 ) ) ↔ ∃ 𝑎 ∈ ( Base ‘ 𝐺 ) 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) )
9 1 a1i ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) ) )
10 eqidd ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
11 ovexd ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ~QG 𝑆 ) ∈ V )
12 simpl ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐺 ∈ Abel )
13 9 10 11 12 qusbas ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑆 ) ) = ( Base ‘ 𝐻 ) )
14 13 eleq2d ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑆 ) ) ↔ 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
15 8 14 bitr3id ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ∃ 𝑎 ∈ ( Base ‘ 𝐺 ) 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ↔ 𝑥 ∈ ( Base ‘ 𝐻 ) ) )
16 vex 𝑦 ∈ V
17 16 elqs ( 𝑦 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑆 ) ) ↔ ∃ 𝑏 ∈ ( Base ‘ 𝐺 ) 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) )
18 13 eleq2d ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑦 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑆 ) ) ↔ 𝑦 ∈ ( Base ‘ 𝐻 ) ) )
19 17 18 bitr3id ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ∃ 𝑏 ∈ ( Base ‘ 𝐺 ) 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ↔ 𝑦 ∈ ( Base ‘ 𝐻 ) ) )
20 15 19 anbi12d ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ∃ 𝑎 ∈ ( Base ‘ 𝐺 ) 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ∧ ∃ 𝑏 ∈ ( Base ‘ 𝐺 ) 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) ) )
21 reeanv ( ∃ 𝑎 ∈ ( Base ‘ 𝐺 ) ∃ 𝑏 ∈ ( Base ‘ 𝐺 ) ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) ↔ ( ∃ 𝑎 ∈ ( Base ‘ 𝐺 ) 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ∧ ∃ 𝑏 ∈ ( Base ‘ 𝐺 ) 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) )
22 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
23 eqid ( +g𝐺 ) = ( +g𝐺 )
24 22 23 ablcom ( ( 𝐺 ∈ Abel ∧ 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑎 ( +g𝐺 ) 𝑏 ) = ( 𝑏 ( +g𝐺 ) 𝑎 ) )
25 24 3expb ( ( 𝐺 ∈ Abel ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑎 ( +g𝐺 ) 𝑏 ) = ( 𝑏 ( +g𝐺 ) 𝑎 ) )
26 25 adantlr ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑎 ( +g𝐺 ) 𝑏 ) = ( 𝑏 ( +g𝐺 ) 𝑎 ) )
27 26 eceq1d ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → [ ( 𝑎 ( +g𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑆 ) = [ ( 𝑏 ( +g𝐺 ) 𝑎 ) ] ( 𝐺 ~QG 𝑆 ) )
28 4 adantr ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) )
29 simprl ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑎 ∈ ( Base ‘ 𝐺 ) )
30 simprr ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → 𝑏 ∈ ( Base ‘ 𝐺 ) )
31 eqid ( +g𝐻 ) = ( +g𝐻 )
32 1 22 23 31 qusadd ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) → ( [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑎 ( +g𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑆 ) )
33 28 29 30 32 syl3anc ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑎 ( +g𝐺 ) 𝑏 ) ] ( 𝐺 ~QG 𝑆 ) )
34 1 22 23 31 qusadd ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ∧ 𝑎 ∈ ( Base ‘ 𝐺 ) ) → ( [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑏 ( +g𝐺 ) 𝑎 ) ] ( 𝐺 ~QG 𝑆 ) )
35 28 30 29 34 syl3anc ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑏 ( +g𝐺 ) 𝑎 ) ] ( 𝐺 ~QG 𝑆 ) )
36 27 33 35 3eqtr4d ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) = ( [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ) )
37 oveq12 ( ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) → ( 𝑥 ( +g𝐻 ) 𝑦 ) = ( [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) )
38 oveq12 ( ( 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ∧ 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ) → ( 𝑦 ( +g𝐻 ) 𝑥 ) = ( [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ) )
39 38 ancoms ( ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) → ( 𝑦 ( +g𝐻 ) 𝑥 ) = ( [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ) )
40 37 39 eqeq12d ( ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) → ( ( 𝑥 ( +g𝐻 ) 𝑦 ) = ( 𝑦 ( +g𝐻 ) 𝑥 ) ↔ ( [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) = ( [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ( +g𝐻 ) [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ) ) )
41 36 40 syl5ibrcom ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) → ( 𝑥 ( +g𝐻 ) 𝑦 ) = ( 𝑦 ( +g𝐻 ) 𝑥 ) ) )
42 41 rexlimdvva ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ∃ 𝑎 ∈ ( Base ‘ 𝐺 ) ∃ 𝑏 ∈ ( Base ‘ 𝐺 ) ( 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ∧ 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) → ( 𝑥 ( +g𝐻 ) 𝑦 ) = ( 𝑦 ( +g𝐻 ) 𝑥 ) ) )
43 21 42 syl5bir ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ∃ 𝑎 ∈ ( Base ‘ 𝐺 ) 𝑥 = [ 𝑎 ] ( 𝐺 ~QG 𝑆 ) ∧ ∃ 𝑏 ∈ ( Base ‘ 𝐺 ) 𝑦 = [ 𝑏 ] ( 𝐺 ~QG 𝑆 ) ) → ( 𝑥 ( +g𝐻 ) 𝑦 ) = ( 𝑦 ( +g𝐻 ) 𝑥 ) ) )
44 20 43 sylbird ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐻 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) → ( 𝑥 ( +g𝐻 ) 𝑦 ) = ( 𝑦 ( +g𝐻 ) 𝑥 ) ) )
45 44 ralrimivv ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g𝐻 ) 𝑦 ) = ( 𝑦 ( +g𝐻 ) 𝑥 ) )
46 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
47 46 31 isabl2 ( 𝐻 ∈ Abel ↔ ( 𝐻 ∈ Grp ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐻 ) ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ( 𝑥 ( +g𝐻 ) 𝑦 ) = ( 𝑦 ( +g𝐻 ) 𝑥 ) ) )
48 6 45 47 sylanbrc ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ Abel )