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

Metamath Proof Explorer

Theorem srgridm

Description: The unity element of a semiring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011) (Revised by Thierry Arnoux, 1-Apr-2018)

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

Proof

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