Step |
Hyp |
Ref |
Expression |
1 |
|
eqgabl.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
eqgabl.n |
⊢ − = ( -g ‘ 𝐺 ) |
3 |
|
eqgabl.r |
⊢ ∼ = ( 𝐺 ~QG 𝑆 ) |
4 |
|
eqid |
⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 ) |
5 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
6 |
1 4 5 3
|
eqgval |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐵 ) ∈ 𝑆 ) ) ) |
7 |
|
simpll |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐺 ∈ Abel ) |
8 |
|
ablgrp |
⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp ) |
9 |
8
|
ad2antrr |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐺 ∈ Grp ) |
10 |
|
simprl |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 ) |
11 |
1 4
|
grpinvcl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ) |
12 |
9 10 11
|
syl2anc |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ) |
13 |
|
simprr |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 ) |
14 |
1 5
|
ablcom |
⊢ ( ( 𝐺 ∈ Abel ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
15 |
7 12 13 14
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
16 |
1 5 4 2
|
grpsubval |
⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 − 𝐴 ) = ( 𝐵 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
17 |
13 10 16
|
syl2anc |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 − 𝐴 ) = ( 𝐵 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
18 |
15 17
|
eqtr4d |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐵 ) = ( 𝐵 − 𝐴 ) ) |
19 |
18
|
eleq1d |
⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 − 𝐴 ) ∈ 𝑆 ) ) |
20 |
19
|
pm5.32da |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐵 ) ∈ 𝑆 ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐵 − 𝐴 ) ∈ 𝑆 ) ) ) |
21 |
|
df-3an |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐵 ) ∈ 𝑆 ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐵 ) ∈ 𝑆 ) ) |
22 |
|
df-3an |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐵 − 𝐴 ) ∈ 𝑆 ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐵 − 𝐴 ) ∈ 𝑆 ) ) |
23 |
20 21 22
|
3bitr4g |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐵 ) ∈ 𝑆 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐵 − 𝐴 ) ∈ 𝑆 ) ) ) |
24 |
6 23
|
bitrd |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐵 − 𝐴 ) ∈ 𝑆 ) ) ) |