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 ⊢ X = Base G
eqgabl.n ⊢ - ˙ = - G
eqgabl.r ⊢ ∼ ˙ = G ~ QG S
Assertion eqgabl ⊢ G ∈ Abel ∧ S ⊆ X → A ∼ ˙ B ↔ A ∈ X ∧ B ∈ X ∧ B - ˙ A ∈ S

Proof

Step Hyp Ref Expression
1 eqgabl.x ⊢ X = Base G
2 eqgabl.n ⊢ - ˙ = - G
3 eqgabl.r ⊢ ∼ ˙ = G ~ QG S
4 eqid ⊢ inv g ⁡ G = inv g ⁡ G
5 eqid ⊢ + G = + G
6 1 4 5 3 eqgval ⊢ G ∈ Abel ∧ S ⊆ X → A ∼ ˙ B ↔ A ∈ X ∧ B ∈ X ∧ inv g ⁡ G ⁡ A + G B ∈ S
7 simpll ⊢ G ∈ Abel ∧ S ⊆ X ∧ A ∈ X ∧ B ∈ X → G ∈ Abel
8 ablgrp ⊢ G ∈ Abel → G ∈ Grp
9 8 ad2antrr ⊢ G ∈ Abel ∧ S ⊆ X ∧ A ∈ X ∧ B ∈ X → G ∈ Grp
10 simprl ⊢ G ∈ Abel ∧ S ⊆ X ∧ A ∈ X ∧ B ∈ X → A ∈ X
11 1 4 grpinvcl ⊢ G ∈ Grp ∧ A ∈ X → inv g ⁡ G ⁡ A ∈ X
12 9 10 11 syl2anc ⊢ G ∈ Abel ∧ S ⊆ X ∧ A ∈ X ∧ B ∈ X → inv g ⁡ G ⁡ A ∈ X
13 simprr ⊢ G ∈ Abel ∧ S ⊆ X ∧ A ∈ X ∧ B ∈ X → B ∈ X
14 1 5 ablcom ⊢ G ∈ Abel ∧ inv g ⁡ G ⁡ A ∈ X ∧ B ∈ X → inv g ⁡ G ⁡ A + G B = B + G inv g ⁡ G ⁡ A
15 7 12 13 14 syl3anc ⊢ G ∈ Abel ∧ S ⊆ X ∧ A ∈ X ∧ B ∈ X → inv g ⁡ G ⁡ A + G B = B + G inv g ⁡ G ⁡ A
16 1 5 4 2 grpsubval ⊢ B ∈ X ∧ A ∈ X → B - ˙ A = B + G inv g ⁡ G ⁡ A
17 13 10 16 syl2anc ⊢ G ∈ Abel ∧ S ⊆ X ∧ A ∈ X ∧ B ∈ X → B - ˙ A = B + G inv g ⁡ G ⁡ A
18 15 17 eqtr4d ⊢ G ∈ Abel ∧ S ⊆ X ∧ A ∈ X ∧ B ∈ X → inv g ⁡ G ⁡ A + G B = B - ˙ A
19 18 eleq1d ⊢ G ∈ Abel ∧ S ⊆ X ∧ A ∈ X ∧ B ∈ X → inv g ⁡ G ⁡ A + G B ∈ S ↔ B - ˙ A ∈ S
20 19 pm5.32da ⊢ G ∈ Abel ∧ S ⊆ X → A ∈ X ∧ B ∈ X ∧ inv g ⁡ G ⁡ A + G B ∈ S ↔ A ∈ X ∧ B ∈ X ∧ B - ˙ A ∈ S
21 df-3an ⊢ A ∈ X ∧ B ∈ X ∧ inv g ⁡ G ⁡ A + G B ∈ S ↔ A ∈ X ∧ B ∈ X ∧ inv g ⁡ G ⁡ A + G B ∈ S
22 df-3an ⊢ A ∈ X ∧ B ∈ X ∧ B - ˙ A ∈ S ↔ A ∈ X ∧ B ∈ X ∧ B - ˙ A ∈ S
23 20 21 22 3bitr4g ⊢ G ∈ Abel ∧ S ⊆ X → A ∈ X ∧ B ∈ X ∧ inv g ⁡ G ⁡ A + G B ∈ S ↔ A ∈ X ∧ B ∈ X ∧ B - ˙ A ∈ S
24 6 23 bitrd ⊢ G ∈ Abel ∧ S ⊆ X → A ∼ ˙ B ↔ A ∈ X ∧ B ∈ X ∧ B - ˙ A ∈ S