Theorem rrgeq0i

Description: Property of a left-regular element. (Contributed by Stefan O'Rear, 22-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	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)$$

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	isrrg	$$⊢X\in E\leftrightarrow \left(X\in B\wedge \forall y\in B\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\right)$$
6	5	simprbi	$$⊢X\in E\to \forall y\in B\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)$$
7		oveq2	$$⊢y=Y\to X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y$$
8	7	eqeq1d	$$⊢y=Y\to \left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
9		eqeq1	$$⊢y=Y\to \left(y=\underset{\dot{}}{0}\leftrightarrow Y=\underset{\dot{}}{0}\right)$$
10	8 9	imbi12d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\leftrightarrow \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to Y=\underset{\dot{}}{0}\right)\right)$$
11	10	rspcv	$$⊢Y\in B\to \left(\forall y\in B\left(X\underset{\dot{}}{·}y=\underset{\dot{}}{0}\to y=\underset{\dot{}}{0}\right)\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to Y=\underset{\dot{}}{0}\right)\right)$$
12	6 11	mpan9	$$⊢\left(X\in E\wedge Y\in B\right)\to \left(X\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\to Y=\underset{\dot{}}{0}\right)$$