dvdsrmul1

Description: The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	$⊢ B = {Base}_{R}$
2		dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
3		dvdsrmul1.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4	1 2 3	dvdsr	$⊢ X \underset{˙}{∥} Y \leftrightarrow (X \in B \land \exists x \in B x \underset{˙}{\cdot} X = Y)$
5		simplll	$⊢ (((R \in Ring \land Z \in B) \land X \in B) \land x \in B) \to R \in Ring$
6		simplr	$⊢ (((R \in Ring \land Z \in B) \land X \in B) \land x \in B) \to X \in B$
7		simpllr	$⊢ (((R \in Ring \land Z \in B) \land X \in B) \land x \in B) \to Z \in B$
8	1 3	ringcl	$⊢ (R \in Ring \land X \in B \land Z \in B) \to X \underset{˙}{\cdot} Z \in B$
9	5 6 7 8	syl3anc	$⊢ (((R \in Ring \land Z \in B) \land X \in B) \land x \in B) \to X \underset{˙}{\cdot} Z \in B$
10	1 2 3	dvdsrmul	$⊢ (X \underset{˙}{\cdot} Z \in B \land x \in B) \to (X \underset{˙}{\cdot} Z) \underset{˙}{∥} (x \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z))$
11	9 10	sylancom	$⊢ (((R \in Ring \land Z \in B) \land X \in B) \land x \in B) \to (X \underset{˙}{\cdot} Z) \underset{˙}{∥} (x \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z))$
12		simpr	$⊢ (((R \in Ring \land Z \in B) \land X \in B) \land x \in B) \to x \in B$
13	1 3	ringass	$⊢ (R \in Ring \land (x \in B \land X \in B \land Z \in B)) \to (x \underset{˙}{\cdot} X) \underset{˙}{\cdot} Z = x \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z)$
14	5 12 6 7 13	syl13anc	$⊢ (((R \in Ring \land Z \in B) \land X \in B) \land x \in B) \to (x \underset{˙}{\cdot} X) \underset{˙}{\cdot} Z = x \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z)$
15	11 14	breqtrrd	$⊢ (((R \in Ring \land Z \in B) \land X \in B) \land x \in B) \to (X \underset{˙}{\cdot} Z) \underset{˙}{∥} ((x \underset{˙}{\cdot} X) \underset{˙}{\cdot} Z)$
16		oveq1	$⊢ x \underset{˙}{\cdot} X = Y \to (x \underset{˙}{\cdot} X) \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} Z$
17	16	breq2d	$⊢ x \underset{˙}{\cdot} X = Y \to ((X \underset{˙}{\cdot} Z) \underset{˙}{∥} ((x \underset{˙}{\cdot} X) \underset{˙}{\cdot} Z) \leftrightarrow (X \underset{˙}{\cdot} Z) \underset{˙}{∥} (Y \underset{˙}{\cdot} Z))$
18	15 17	syl5ibcom	$⊢ (((R \in Ring \land Z \in B) \land X \in B) \land x \in B) \to (x \underset{˙}{\cdot} X = Y \to (X \underset{˙}{\cdot} Z) \underset{˙}{∥} (Y \underset{˙}{\cdot} Z))$
19	18	rexlimdva	$⊢ ((R \in Ring \land Z \in B) \land X \in B) \to (\exists x \in B x \underset{˙}{\cdot} X = Y \to (X \underset{˙}{\cdot} Z) \underset{˙}{∥} (Y \underset{˙}{\cdot} Z))$
20	19	expimpd	$⊢ (R \in Ring \land Z \in B) \to ((X \in B \land \exists x \in B x \underset{˙}{\cdot} X = Y) \to (X \underset{˙}{\cdot} Z) \underset{˙}{∥} (Y \underset{˙}{\cdot} Z))$
21	4 20	biimtrid	$⊢ (R \in Ring \land Z \in B) \to (X \underset{˙}{∥} Y \to (X \underset{˙}{\cdot} Z) \underset{˙}{∥} (Y \underset{˙}{\cdot} Z))$
22	21	3impia	$⊢ (R \in Ring \land Z \in B \land X \underset{˙}{∥} Y) \to (X \underset{˙}{\cdot} Z) \underset{˙}{∥} (Y \underset{˙}{\cdot} Z)$

Metamath Proof Explorer

Theorem dvdsrmul1

Proof