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 ` G )
	grplinvd.u	|- .0. = ( 0g ` G )
	grplinvd.n	|- N = ( invg ` G )
	grplinvd.g	|- ( ph -> G e. Grp )
	grplinvd.1	|- ( ph -> X e. B )
Assertion	grplinvd	|- ( ph -> ( ( N ` X ) .+ X ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		grplinvd.b	|- B = ( Base ` G )
2		grplinvd.p	|- .+ = ( +g ` G )
3		grplinvd.u	|- .0. = ( 0g ` G )
4		grplinvd.n	|- N = ( invg ` G )
5		grplinvd.g	|- ( ph -> G e. Grp )
6		grplinvd.1	|- ( ph -> X e. B )
7	1 2 3 4	grplinv	|- ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) .+ X ) = .0. )
8	5 6 7	syl2anc	|- ( ph -> ( ( N ` X ) .+ X ) = .0. )