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