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 ) |