Theorem rrgeq0

Description: Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	rrgval.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	rrgval.b	$$⊢B={\mathrm{Base}}_R$$
	rrgval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rrgval.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	rrgeq0	$$⊢\left(R\in \mathrm{Ring}\wedge X\in E\wedge Y\in B\right)\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrgval.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
2		rrgval.b	$$⊢B={\mathrm{Base}}_R$$
3		rrgval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		rrgval.z	$$⊢\underset{\dot{}}{0}=0_R$$
5	1 2 3 4	rrgeq0i	$$⊢\left(X\in E\wedge Y\in B\right)\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to Y=\underset{\dot{}}{0}\right)$$
6	5	3adant1	$$⊢\left(R\in \mathrm{Ring}\wedge X\in E\wedge Y\in B\right)\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to Y=\underset{\dot{}}{0}\right)$$
7		simp1	$$⊢\left(R\in \mathrm{Ring}\wedge X\in E\wedge Y\in B\right)\to R\in \mathrm{Ring}$$
8	1 2 3 4	rrgval	$$⊢E=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right\}$$
9	8	ssrab3	$$⊢E\subseteq B$$
10		simp2	$$⊢\left(R\in \mathrm{Ring}\wedge X\in E\wedge Y\in B\right)\to X\in E$$
11	9 10	sseldi	$$⊢\left(R\in \mathrm{Ring}\wedge X\in E\wedge Y\in B\right)\to X\in B$$
12	2 3 4	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
13	7 11 12	syl2anc	$$⊢\left(R\in \mathrm{Ring}\wedge X\in E\wedge Y\in B\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
14		oveq2	$$⊢Y=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}\underset{\dot{}}{0}$$
15	14	eqeq1d	$$⊢Y=\underset{\dot{}}{0}\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
16	13 15	syl5ibrcom	$$⊢\left(R\in \mathrm{Ring}\wedge X\in E\wedge Y\in B\right)\to \left(Y=\underset{\dot{}}{0}\to X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
17	6 16	impbid	$$⊢\left(R\in \mathrm{Ring}\wedge X\in E\wedge Y\in B\right)\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$