Theorem dvdsr02

Description: Only zero is divisible by zero. (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	dvdsr02	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{\parallel }X\leftrightarrow X=\underset{\dot{}}{0}\right)$$

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	4	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \underset{\dot{}}{0}\in B$$
6		eqid	$$⊢{\cdot }_R={\cdot }_R$$
7	1 2 6	dvdsr2	$$⊢\underset{\dot{}}{0}\in B\to \left(\underset{\dot{}}{0}\underset{\dot{}}{\parallel }X\leftrightarrow \exists x\in Bx{\cdot }_R\underset{\dot{}}{0}=X\right)$$
8	5 7	syl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{\parallel }X\leftrightarrow \exists x\in Bx{\cdot }_R\underset{\dot{}}{0}=X\right)$$
9	1 6 3	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\right)\to x{\cdot }_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
10	9	eqeq1d	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\right)\to \left(x{\cdot }_R\underset{\dot{}}{0}=X\leftrightarrow \underset{\dot{}}{0}=X\right)$$
11		eqcom	$$⊢\underset{\dot{}}{0}=X\leftrightarrow X=\underset{\dot{}}{0}$$
12	10 11	syl6bb	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\right)\to \left(x{\cdot }_R\underset{\dot{}}{0}=X\leftrightarrow X=\underset{\dot{}}{0}\right)$$
13	12	rexbidva	$$⊢R\in \mathrm{Ring}\to \left(\exists x\in Bx{\cdot }_R\underset{\dot{}}{0}=X\leftrightarrow \exists x\in BX=\underset{\dot{}}{0}\right)$$
14		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
15	1	grpbn0	$$⊢R\in \mathrm{Grp}\to B\ne \varnothing$$
16		r19.9rzv	$$⊢B\ne \varnothing \to \left(X=\underset{\dot{}}{0}\leftrightarrow \exists x\in BX=\underset{\dot{}}{0}\right)$$
17	14 15 16	3syl	$$⊢R\in \mathrm{Ring}\to \left(X=\underset{\dot{}}{0}\leftrightarrow \exists x\in BX=\underset{\dot{}}{0}\right)$$
18	13 17	bitr4d	$$⊢R\in \mathrm{Ring}\to \left(\exists x\in Bx{\cdot }_R\underset{\dot{}}{0}=X\leftrightarrow X=\underset{\dot{}}{0}\right)$$
19	18	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(\exists x\in Bx{\cdot }_R\underset{\dot{}}{0}=X\leftrightarrow X=\underset{\dot{}}{0}\right)$$
20	8 19	bitrd	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{\parallel }X\leftrightarrow X=\underset{\dot{}}{0}\right)$$