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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grplinvd.p	⊢ + = ( +g ‘ 𝐺 )
	grplinvd.u	⊢ 0 = ( 0g ‘ 𝐺 )
	grplinvd.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
	grplinvd.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	grplinvd.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	grplinvd	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) + 𝑋 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		grplinvd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grplinvd.p	⊢ + = ( +g ‘ 𝐺 )
3		grplinvd.u	⊢ 0 = ( 0g ‘ 𝐺 )
4		grplinvd.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
5		grplinvd.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
6		grplinvd.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7	1 2 3 4	grplinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑋 ) + 𝑋 ) = 0 )
8	5 6 7	syl2anc	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) + 𝑋 ) = 0 )