Metamath Proof Explorer

Theorem grpsubrcan

Description: Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014)

Ref Expression
Hypotheses grpsubcl.b ⊢ B = Base G
grpsubcl.m ⊢ - ˙ = - G
Assertion grpsubrcan ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X - ˙ Z = Y - ˙ Z ↔ X = Y

Proof

Step Hyp Ref Expression
1 grpsubcl.b ⊢ B = Base G
2 grpsubcl.m ⊢ - ˙ = - G
3 eqid ⊢ + G = + G
4 eqid ⊢ inv g ⁡ G = inv g ⁡ G
5 1 3 4 2 grpsubval ⊢ X ∈ B ∧ Z ∈ B → X - ˙ Z = X + G inv g ⁡ G ⁡ Z
6 5 3adant2 ⊢ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X - ˙ Z = X + G inv g ⁡ G ⁡ Z
7 1 3 4 2 grpsubval ⊢ Y ∈ B ∧ Z ∈ B → Y - ˙ Z = Y + G inv g ⁡ G ⁡ Z
8 7 3adant1 ⊢ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y - ˙ Z = Y + G inv g ⁡ G ⁡ Z
9 6 8 eqeq12d ⊢ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X - ˙ Z = Y - ˙ Z ↔ X + G inv g ⁡ G ⁡ Z = Y + G inv g ⁡ G ⁡ Z
10 9 adantl ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X - ˙ Z = Y - ˙ Z ↔ X + G inv g ⁡ G ⁡ Z = Y + G inv g ⁡ G ⁡ Z
11 simpl ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → G ∈ Grp
12 simpr1 ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
13 simpr2 ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B
14 1 4 grpinvcl ⊢ G ∈ Grp ∧ Z ∈ B → inv g ⁡ G ⁡ Z ∈ B
15 14 3ad2antr3 ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → inv g ⁡ G ⁡ Z ∈ B
16 1 3 grprcan ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B ∧ inv g ⁡ G ⁡ Z ∈ B → X + G inv g ⁡ G ⁡ Z = Y + G inv g ⁡ G ⁡ Z ↔ X = Y
17 11 12 13 15 16 syl13anc ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X + G inv g ⁡ G ⁡ Z = Y + G inv g ⁡ G ⁡ Z ↔ X = Y
18 10 17 bitrd ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X - ˙ Z = Y - ˙ Z ↔ X = Y