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={\mathrm{Base}}_G$$
	grplinvd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grplinvd.u	$$⊢\underset{\dot{}}{0}=0_G$$
	grplinvd.n	$$⊢N={inv}_g\left(G\right)$$
	grplinvd.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	grplinvd.1	$$⊢\phi \to X\in B$$
Assertion	grplinvd	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		grplinvd.b	$$⊢B={\mathrm{Base}}_G$$
2		grplinvd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grplinvd.u	$$⊢\underset{\dot{}}{0}=0_G$$
4		grplinvd.n	$$⊢N={inv}_g\left(G\right)$$
5		grplinvd.g	$$⊢\phi \to G\in \mathrm{Grp}$$
6		grplinvd.1	$$⊢\phi \to X\in B$$
7	1 2 3 4	grplinv	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to N\left(X\right)\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$
8	5 6 7	syl2anc	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$