Theorem dvdsrcl2

Description: Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014)

	Ref	Expression
Hypotheses	dvdsr.1	$$⊢B={\mathrm{Base}}_R$$
	dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
Assertion	dvdsrcl2	$$⊢\left(R\in \mathrm{Ring}\wedge X\underset{\dot{}}{\parallel }Y\right)\to Y\in B$$

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	$$⊢B={\mathrm{Base}}_R$$
2		dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		eqid	$$⊢{\cdot }_R={\cdot }_R$$
4	1 2 3	dvdsr	$$⊢X\underset{\dot{}}{\parallel }Y\leftrightarrow \left(X\in B\wedge \exists x\in Bx{\cdot }_{R}X=Y\right)$$
5	1 3	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\wedge X\in B\right)\to x{\cdot }_{R}X\in B$$
6	5	3expa	$$⊢\left(\left(R\in \mathrm{Ring}\wedge x\in B\right)\wedge X\in B\right)\to x{\cdot }_{R}X\in B$$
7	6	an32s	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge x\in B\right)\to x{\cdot }_{R}X\in B$$
8		eleq1	$$⊢x{\cdot }_{R}X=Y\to \left(x{\cdot }_{R}X\in B\leftrightarrow Y\in B\right)$$
9	7 8	syl5ibcom	$$⊢\left(\left(R\in \mathrm{Ring}\wedge X\in B\right)\wedge x\in B\right)\to \left(x{\cdot }_{R}X=Y\to Y\in B\right)$$
10	9	rexlimdva	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(\exists x\in Bx{\cdot }_{R}X=Y\to Y\in B\right)$$
11	10	impr	$$⊢\left(R\in \mathrm{Ring}\wedge \left(X\in B\wedge \exists x\in Bx{\cdot }_{R}X=Y\right)\right)\to Y\in B$$
12	4 11	sylan2b	$$⊢\left(R\in \mathrm{Ring}\wedge X\underset{\dot{}}{\parallel }Y\right)\to Y\in B$$