Theorem ringlzd

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

	Ref	Expression
Hypotheses	ringlzd.b	$$⊢B={\mathrm{Base}}_R$$
	ringlzd.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	ringlzd.z	$$⊢\underset{\dot{}}{0}=0_R$$
	ringlzd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	ringlzd.x	$$⊢\phi \to X\in B$$
Assertion	ringlzd	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		ringlzd.b	$$⊢B={\mathrm{Base}}_R$$
2		ringlzd.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		ringlzd.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		ringlzd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		ringlzd.x	$$⊢\phi \to X\in B$$
6	1 2 3	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
7	4 5 6	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$