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

Metamath Proof Explorer

Theorem grpasscan2d

Description: An associative cancellation law for groups. (Contributed by SN, 29-Jan-2025)

Ref Expression
Hypotheses grpasscan2d.b ⊢ B = Base G
grpasscan2d.p ⊢ + ˙ = + G
grpasscan2d.n ⊢ N = inv g ⁡ G
grpasscan2d.g ⊢ φ → G ∈ Grp
grpasscan2d.1 ⊢ φ → X ∈ B
grpasscan2d.2 ⊢ φ → Y ∈ B
Assertion grpasscan2d ⊢ φ → X + ˙ N ⁡ Y + ˙ Y = X

Proof

Step Hyp Ref Expression
1 grpasscan2d.b ⊢ B = Base G
2 grpasscan2d.p ⊢ + ˙ = + G
3 grpasscan2d.n ⊢ N = inv g ⁡ G
4 grpasscan2d.g ⊢ φ → G ∈ Grp
5 grpasscan2d.1 ⊢ φ → X ∈ B
6 grpasscan2d.2 ⊢ φ → Y ∈ B
7 1 2 3 grpasscan2 ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → X + ˙ N ⁡ Y + ˙ Y = X
8 4 5 6 7 syl3anc ⊢ φ → X + ˙ N ⁡ Y + ˙ Y = X