Theorem ringlidm

Description: The unit element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011)

	Ref	Expression
Hypotheses	rngidm.b	$$⊢B={\mathrm{Base}}_R$$
	rngidm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rngidm.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$

Proof

Step	Hyp	Ref	Expression
1		rngidm.b	$$⊢B={\mathrm{Base}}_R$$
2		rngidm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		rngidm.u	$$⊢\underset{\dot{}}{1}=1_R$$
4	1 2 3	ringidmlem	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}X=X\wedge X\underset{\dot{}}{·}\underset{\dot{}}{1}=X\right)$$
5	4	simpld	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$