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

Metamath Proof Explorer

Theorem ringrz

Description: The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009) (Proof shortened by AV, 30-Mar-2025)

	Ref	Expression
Hypotheses	ringz.b	$⊢ B = {Base}_{R}$
	ringz.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringz.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	ringrz	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		ringz.b	$⊢ B = {Base}_{R}$
2		ringz.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ringz.z	$⊢ \underset{˙}{0} = 0_{R}$
4		ringrng	$⊢ R \in Ring \to R \in Rng$
5	1 2 3	rngrz	$⊢ (R \in Rng \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
6	4 5	sylan	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$