Theorem dvdsrmul

Description: A left-multiple of X is divisible by X . (Contributed by Mario Carneiro, 1-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	$$⊢B={\mathrm{Base}}_R$$
2		dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		dvdsr.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		simpl	$$⊢\left(X\in B\wedge Y\in B\right)\to X\in B$$
5		simpr	$$⊢\left(X\in B\wedge Y\in B\right)\to Y\in B$$
6		eqid	$$⊢Y\underset{\dot{}}{·}X=Y\underset{\dot{}}{·}X$$
7		oveq1	$$⊢z=Y\to z\underset{\dot{}}{·}X=Y\underset{\dot{}}{·}X$$
8	7	eqeq1d	$$⊢z=Y\to \left(z\underset{\dot{}}{·}X=Y\underset{\dot{}}{·}X\leftrightarrow Y\underset{\dot{}}{·}X=Y\underset{\dot{}}{·}X\right)$$
9	8	rspcev	$$⊢\left(Y\in B\wedge Y\underset{\dot{}}{·}X=Y\underset{\dot{}}{·}X\right)\to \exists z\in Bz\underset{\dot{}}{·}X=Y\underset{\dot{}}{·}X$$
10	5 6 9	sylancl	$$⊢\left(X\in B\wedge Y\in B\right)\to \exists z\in Bz\underset{\dot{}}{·}X=Y\underset{\dot{}}{·}X$$
11	1 2 3	dvdsr	$$⊢X\underset{\dot{}}{\parallel }\left(Y\underset{\dot{}}{·}X\right)\leftrightarrow \left(X\in B\wedge \exists z\in Bz\underset{\dot{}}{·}X=Y\underset{\dot{}}{·}X\right)$$
12	4 10 11	sylanbrc	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{\parallel }\left(Y\underset{\dot{}}{·}X\right)$$