Metamath Proof Explorer


Theorem grplinvd

Description: The left inverse of a group element. Deduction associated with grplinv . (Contributed by SN, 29-Jan-2025)

Ref Expression
Hypotheses grplinvd.b B = Base G
grplinvd.p + ˙ = + G
grplinvd.u 0 ˙ = 0 G
grplinvd.n N = inv g G
grplinvd.g φ G Grp
grplinvd.1 φ X B
Assertion grplinvd φ N X + ˙ X = 0 ˙

Proof

Step Hyp Ref Expression
1 grplinvd.b B = Base G
2 grplinvd.p + ˙ = + G
3 grplinvd.u 0 ˙ = 0 G
4 grplinvd.n N = inv g G
5 grplinvd.g φ G Grp
6 grplinvd.1 φ X B
7 1 2 3 4 grplinv G Grp X B N X + ˙ X = 0 ˙
8 5 6 7 syl2anc φ N X + ˙ X = 0 ˙