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