dvdsrtr

Description: Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	$⊢ B = {Base}_{R}$
2		dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
3		eqid	$⊢ \cdot_{R} = \cdot_{R}$
4	1 2 3	dvdsr	$⊢ Y \underset{˙}{∥} Z \leftrightarrow (Y \in B \land \exists y \in B y \cdot_{R} Y = Z)$
5	1 2 3	dvdsr	$⊢ Z \underset{˙}{∥} X \leftrightarrow (Z \in B \land \exists x \in B x \cdot_{R} Z = X)$
6	4 5	anbi12i	$⊢ (Y \underset{˙}{∥} Z \land Z \underset{˙}{∥} X) \leftrightarrow ((Y \in B \land \exists y \in B y \cdot_{R} Y = Z) \land (Z \in B \land \exists x \in B x \cdot_{R} Z = X))$
7		an4	$⊢ ((Y \in B \land \exists y \in B y \cdot_{R} Y = Z) \land (Z \in B \land \exists x \in B x \cdot_{R} Z = X)) \leftrightarrow ((Y \in B \land Z \in B) \land (\exists y \in B y \cdot_{R} Y = Z \land \exists x \in B x \cdot_{R} Z = X))$
8	6 7	bitri	$⊢ (Y \underset{˙}{∥} Z \land Z \underset{˙}{∥} X) \leftrightarrow ((Y \in B \land Z \in B) \land (\exists y \in B y \cdot_{R} Y = Z \land \exists x \in B x \cdot_{R} Z = X))$
9		reeanv	$⊢ \exists y \in B \exists x \in B (y \cdot_{R} Y = Z \land x \cdot_{R} Z = X) \leftrightarrow (\exists y \in B y \cdot_{R} Y = Z \land \exists x \in B x \cdot_{R} Z = X)$
10		simplrl	$⊢ ((R \in Ring \land (Y \in B \land Z \in B)) \land (y \in B \land x \in B)) \to Y \in B$
11		simpll	$⊢ ((R \in Ring \land (Y \in B \land Z \in B)) \land (y \in B \land x \in B)) \to R \in Ring$
12		simprr	$⊢ ((R \in Ring \land (Y \in B \land Z \in B)) \land (y \in B \land x \in B)) \to x \in B$
13		simprl	$⊢ ((R \in Ring \land (Y \in B \land Z \in B)) \land (y \in B \land x \in B)) \to y \in B$
14	1 3	ringcl	$⊢ (R \in Ring \land x \in B \land y \in B) \to x \cdot_{R} y \in B$
15	11 12 13 14	syl3anc	$⊢ ((R \in Ring \land (Y \in B \land Z \in B)) \land (y \in B \land x \in B)) \to x \cdot_{R} y \in B$
16	1 2 3	dvdsrmul	$⊢ (Y \in B \land x \cdot_{R} y \in B) \to Y \underset{˙}{∥} ((x \cdot_{R} y) \cdot_{R} Y)$
17	10 15 16	syl2anc	$⊢ ((R \in Ring \land (Y \in B \land Z \in B)) \land (y \in B \land x \in B)) \to Y \underset{˙}{∥} ((x \cdot_{R} y) \cdot_{R} Y)$
18	1 3	ringass	$⊢ (R \in Ring \land (x \in B \land y \in B \land Y \in B)) \to (x \cdot_{R} y) \cdot_{R} Y = x \cdot_{R} (y \cdot_{R} Y)$
19	11 12 13 10 18	syl13anc	$⊢ ((R \in Ring \land (Y \in B \land Z \in B)) \land (y \in B \land x \in B)) \to (x \cdot_{R} y) \cdot_{R} Y = x \cdot_{R} (y \cdot_{R} Y)$
20	17 19	breqtrd	$⊢ ((R \in Ring \land (Y \in B \land Z \in B)) \land (y \in B \land x \in B)) \to Y \underset{˙}{∥} (x \cdot_{R} (y \cdot_{R} Y))$
21		oveq2	$⊢ y \cdot_{R} Y = Z \to x \cdot_{R} (y \cdot_{R} Y) = x \cdot_{R} Z$
22		id	$⊢ x \cdot_{R} Z = X \to x \cdot_{R} Z = X$
23	21 22	sylan9eq	$⊢ (y \cdot_{R} Y = Z \land x \cdot_{R} Z = X) \to x \cdot_{R} (y \cdot_{R} Y) = X$
24	23	breq2d	$⊢ (y \cdot_{R} Y = Z \land x \cdot_{R} Z = X) \to (Y \underset{˙}{∥} (x \cdot_{R} (y \cdot_{R} Y)) \leftrightarrow Y \underset{˙}{∥} X)$
25	20 24	syl5ibcom	$⊢ ((R \in Ring \land (Y \in B \land Z \in B)) \land (y \in B \land x \in B)) \to ((y \cdot_{R} Y = Z \land x \cdot_{R} Z = X) \to Y \underset{˙}{∥} X)$
26	25	rexlimdvva	$⊢ (R \in Ring \land (Y \in B \land Z \in B)) \to (\exists y \in B \exists x \in B (y \cdot_{R} Y = Z \land x \cdot_{R} Z = X) \to Y \underset{˙}{∥} X)$
27	9 26	biimtrrid	$⊢ (R \in Ring \land (Y \in B \land Z \in B)) \to ((\exists y \in B y \cdot_{R} Y = Z \land \exists x \in B x \cdot_{R} Z = X) \to Y \underset{˙}{∥} X)$
28	27	expimpd	$⊢ R \in Ring \to (((Y \in B \land Z \in B) \land (\exists y \in B y \cdot_{R} Y = Z \land \exists x \in B x \cdot_{R} Z = X)) \to Y \underset{˙}{∥} X)$
29	8 28	biimtrid	$⊢ R \in Ring \to ((Y \underset{˙}{∥} Z \land Z \underset{˙}{∥} X) \to Y \underset{˙}{∥} X)$
30	29	3impib	$⊢ (R \in Ring \land Y \underset{˙}{∥} Z \land Z \underset{˙}{∥} X) \to Y \underset{˙}{∥} X$

Metamath Proof Explorer

Theorem dvdsrtr

Proof