Theorem grplidd

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

	Ref	Expression
Hypotheses	grpbn0.b	|- B = ( Base ` G )
	grplid.p	|- .+ = ( +g ` G )
	grplid.o	|- .0. = ( 0g ` G )
	grplidd.g	|- ( ph -> G e. Grp )
	grplidd.1	|- ( ph -> X e. B )
Assertion	grplidd	|- ( ph -> ( .0. .+ X ) = X )

Proof

Step	Hyp	Ref	Expression
1		grpbn0.b	|- B = ( Base ` G )
2		grplid.p	|- .+ = ( +g ` G )
3		grplid.o	|- .0. = ( 0g ` G )
4		grplidd.g	|- ( ph -> G e. Grp )
5		grplidd.1	|- ( ph -> X e. B )
6	1 2 3	grplid	|- ( ( G e. Grp /\ X e. B ) -> ( .0. .+ X ) = X )
7	4 5 6	syl2anc	|- ( ph -> ( .0. .+ X ) = X )