Metamath Proof Explorer

Theorem eqgabl

Description: Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses eqgabl.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
eqgabl.n ⊢ − = ( -g ‘ 𝐺 )
eqgabl.r ⊢ ∼ = ( 𝐺 ~QG 𝑆 )
Assertion eqgabl ( ( 𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐵 − 𝐴 ) ∈ 𝑆 ) ) )

Proof

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 ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐵 − 𝐴 ) ∈ 𝑆 ) ) )