Theorem dvdsr01

Description: In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg .) (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	dvdsr0.b	$$⊢B={\mathrm{Base}}_R$$
	dvdsr0.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	dvdsr0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	dvdsr01	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{\parallel }\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		dvdsr0.b	$$⊢B={\mathrm{Base}}_R$$
2		dvdsr0.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		dvdsr0.z	$$⊢\underset{\dot{}}{0}=0_R$$
4	1 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in B$$
5		eqid	$$⊢{\cdot }_R={\cdot }_R$$
6	1 5 3	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \underset{\dot{}}{0}{\cdot }_{R}X=\underset{\dot{}}{0}$$
7		oveq1	$$⊢x=\underset{\dot{}}{0}\to x{\cdot }_{R}X=\underset{\dot{}}{0}{\cdot }_{R}X$$
8	7	eqeq1d	$$⊢x=\underset{\dot{}}{0}\to \left(x{\cdot }_{R}X=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{0}{\cdot }_{R}X=\underset{\dot{}}{0}\right)$$
9	8	rspcev	$$⊢\left(\underset{\dot{}}{0}\in B\wedge \underset{\dot{}}{0}{\cdot }_{R}X=\underset{\dot{}}{0}\right)\to \exists x\in Bx{\cdot }_{R}X=\underset{\dot{}}{0}$$
10	4 6 9	syl2an2r	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \exists x\in Bx{\cdot }_{R}X=\underset{\dot{}}{0}$$
11	1 2 5	dvdsr2	$$⊢X\in B\to \left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{0}\leftrightarrow \exists x\in Bx{\cdot }_{R}X=\underset{\dot{}}{0}\right)$$
12	11	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(X\underset{\dot{}}{\parallel }\underset{\dot{}}{0}\leftrightarrow \exists x\in Bx{\cdot }_{R}X=\underset{\dot{}}{0}\right)$$
13	10 12	mpbird	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{\parallel }\underset{\dot{}}{0}$$