This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ringlidm

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

	Ref	Expression
Hypotheses	ringidm.b	$⊢ B = {Base}_{R}$
	ringidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringidm.u	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	ringlidm	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{1} \underset{˙}{\cdot} X = X$

Step	Hyp	Ref	Expression
1		ringidm.b	$⊢ B = {Base}_{R}$
2		ringidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ringidm.u	$⊢ \underset{˙}{1} = 1_{R}$
4	1 2 3	ringidmlem	$⊢ (R \in Ring \land X \in B) \to (\underset{˙}{1} \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} \underset{˙}{1} = X)$
5	4	simpld	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{1} \underset{˙}{\cdot} X = X$