This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusecsub

Description: Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025)

Ref Expression
Hypotheses qusecsub.x ⊢ B = Base G
qusecsub.n ⊢ - ˙ = - G
qusecsub.r ⊢ ∼ ˙ = G ~ QG S
Assertion qusecsub ⊢ G ∈ Abel ∧ S ∈ SubGrp ⁡ G ∧ X ∈ B ∧ Y ∈ B → X ∼ ˙ = Y ∼ ˙ ↔ Y - ˙ X ∈ S

Proof

Step Hyp Ref Expression
1 qusecsub.x ⊢ B = Base G
2 qusecsub.n ⊢ - ˙ = - G
3 qusecsub.r ⊢ ∼ ˙ = G ~ QG S
4 1 subgss ⊢ S ∈ SubGrp ⁡ G → S ⊆ B
5 4 anim2i ⊢ G ∈ Abel ∧ S ∈ SubGrp ⁡ G → G ∈ Abel ∧ S ⊆ B
6 5 adantr ⊢ G ∈ Abel ∧ S ∈ SubGrp ⁡ G ∧ X ∈ B ∧ Y ∈ B → G ∈ Abel ∧ S ⊆ B
7 1 2 3 eqgabl ⊢ G ∈ Abel ∧ S ⊆ B → X ∼ ˙ Y ↔ X ∈ B ∧ Y ∈ B ∧ Y - ˙ X ∈ S
8 6 7 syl ⊢ G ∈ Abel ∧ S ∈ SubGrp ⁡ G ∧ X ∈ B ∧ Y ∈ B → X ∼ ˙ Y ↔ X ∈ B ∧ Y ∈ B ∧ Y - ˙ X ∈ S
9 1 3 eqger ⊢ S ∈ SubGrp ⁡ G → ∼ ˙ Er B
10 9 ad2antlr ⊢ G ∈ Abel ∧ S ∈ SubGrp ⁡ G ∧ X ∈ B ∧ Y ∈ B → ∼ ˙ Er B
11 simprl ⊢ G ∈ Abel ∧ S ∈ SubGrp ⁡ G ∧ X ∈ B ∧ Y ∈ B → X ∈ B
12 10 11 erth ⊢ G ∈ Abel ∧ S ∈ SubGrp ⁡ G ∧ X ∈ B ∧ Y ∈ B → X ∼ ˙ Y ↔ X ∼ ˙ = Y ∼ ˙
13 df-3an ⊢ X ∈ B ∧ Y ∈ B ∧ Y - ˙ X ∈ S ↔ X ∈ B ∧ Y ∈ B ∧ Y - ˙ X ∈ S
14 ibar ⊢ X ∈ B ∧ Y ∈ B → Y - ˙ X ∈ S ↔ X ∈ B ∧ Y ∈ B ∧ Y - ˙ X ∈ S
15 14 adantl ⊢ G ∈ Abel ∧ S ∈ SubGrp ⁡ G ∧ X ∈ B ∧ Y ∈ B → Y - ˙ X ∈ S ↔ X ∈ B ∧ Y ∈ B ∧ Y - ˙ X ∈ S
16 13 15 bitr4id ⊢ G ∈ Abel ∧ S ∈ SubGrp ⁡ G ∧ X ∈ B ∧ Y ∈ B → X ∈ B ∧ Y ∈ B ∧ Y - ˙ X ∈ S ↔ Y - ˙ X ∈ S
17 8 12 16 3bitr3d ⊢ G ∈ Abel ∧ S ∈ SubGrp ⁡ G ∧ X ∈ B ∧ Y ∈ B → X ∼ ˙ = Y ∼ ˙ ↔ Y - ˙ X ∈ S