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 )