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

Metamath Proof Explorer

Theorem ringridmd

Description: The unity element of a ring is a right multiplicative identity. (Contributed by SN, 14-Aug-2024)

	Ref	Expression
Hypotheses	ringlidmd.b	$⊢ B = {Base}_{R}$
	ringlidmd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringlidmd.u	$⊢ \underset{˙}{1} = 1_{R}$
	ringlidmd.r	$⊢ φ \to R \in Ring$
	ringlidmd.x	$⊢ φ \to X \in B$
Assertion	ringridmd	$⊢ φ \to X \underset{˙}{\cdot} \underset{˙}{1} = X$

Step	Hyp	Ref	Expression
1		ringlidmd.b	$⊢ B = {Base}_{R}$
2		ringlidmd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ringlidmd.u	$⊢ \underset{˙}{1} = 1_{R}$
4		ringlidmd.r	$⊢ φ \to R \in Ring$
5		ringlidmd.x	$⊢ φ \to X \in B$
6	1 2 3	ringridm	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{1} = X$
7	4 5 6	syl2anc	$⊢ φ \to X \underset{˙}{\cdot} \underset{˙}{1} = X$