dvdsrmul

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

	Ref	Expression
Hypotheses	dvdsr.1	$⊢ B = {Base}_{R}$
	dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
	dvdsr.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	dvdsrmul	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{∥} (Y \underset{˙}{\cdot} X)$

Step	Hyp	Ref	Expression
1		dvdsr.1	$⊢ B = {Base}_{R}$
2		dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
3		dvdsr.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		simpl	$⊢ (X \in B \land Y \in B) \to X \in B$
5		simpr	$⊢ (X \in B \land Y \in B) \to Y \in B$
6		eqid	$⊢ Y \underset{˙}{\cdot} X = Y \underset{˙}{\cdot} X$
7		oveq1	$⊢ z = Y \to z \underset{˙}{\cdot} X = Y \underset{˙}{\cdot} X$
8	7	eqeq1d	$⊢ z = Y \to (z \underset{˙}{\cdot} X = Y \underset{˙}{\cdot} X \leftrightarrow Y \underset{˙}{\cdot} X = Y \underset{˙}{\cdot} X)$
9	8	rspcev	$⊢ (Y \in B \land Y \underset{˙}{\cdot} X = Y \underset{˙}{\cdot} X) \to \exists z \in B z \underset{˙}{\cdot} X = Y \underset{˙}{\cdot} X$
10	5 6 9	sylancl	$⊢ (X \in B \land Y \in B) \to \exists z \in B z \underset{˙}{\cdot} X = Y \underset{˙}{\cdot} X$
11	1 2 3	dvdsr	$⊢ X \underset{˙}{∥} (Y \underset{˙}{\cdot} X) \leftrightarrow (X \in B \land \exists z \in B z \underset{˙}{\cdot} X = Y \underset{˙}{\cdot} X)$
12	4 10 11	sylanbrc	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{∥} (Y \underset{˙}{\cdot} X)$

Metamath Proof Explorer