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={\mathrm{Base}}_G$$
	grplid.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grplid.o	$$⊢\underset{\dot{}}{0}=0_G$$
	grplidd.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	grplidd.1	$$⊢\phi \to X\in B$$
Assertion	grplidd	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{+}X=X$$

Proof

Step	Hyp	Ref	Expression
1		grpbn0.b	$$⊢B={\mathrm{Base}}_G$$
2		grplid.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grplid.o	$$⊢\underset{\dot{}}{0}=0_G$$
4		grplidd.g	$$⊢\phi \to G\in \mathrm{Grp}$$
5		grplidd.1	$$⊢\phi \to X\in B$$
6	1 2 3	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}X=X$$
7	4 5 6	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{+}X=X$$