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

Metamath Proof Explorer

Theorem ringlzd

Description: The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025)

	Ref	Expression
Hypotheses	ringz.b	$⊢ B = {Base}_{R}$
	ringz.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringz.z	$⊢ \underset{˙}{0} = 0_{R}$
	ringlzd.r	$⊢ φ \to R \in Ring$
	ringlzd.x	$⊢ φ \to X \in B$
Assertion	ringlzd	$⊢ φ \to \underset{˙}{0} \underset{˙}{\cdot} X = \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		ringlzd.r	$⊢ φ \to R \in Ring$
5		ringlzd.x	$⊢ φ \to X \in B$
6	1 2 3	ringlz	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0}$
7	4 5 6	syl2anc	$⊢ φ \to \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0}$