Metamath Proof Explorer

Theorem dvdsrtr

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

Ref Expression
Hypotheses dvdsr.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvdsr.2 ⊢ ∥ = ( ∥r ‘ 𝑅 )
Assertion dvdsrtr ( ( 𝑅 ∈ Ring ∧ 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋 ) → 𝑌 ∥ 𝑋 )

Proof

Step Hyp Ref Expression
1 dvdsr.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dvdsr.2 ⊢ ∥ = ( ∥r ‘ 𝑅 )
3 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
4 1 2 3 dvdsr ⊢ ( 𝑌 ∥ 𝑍 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ) )
5 1 2 3 dvdsr ⊢ ( 𝑍 ∥ 𝑋 ↔ ( 𝑍 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) )
6 4 5 anbi12i ⊢ ( ( 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋 ) ↔ ( ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ) ∧ ( 𝑍 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) ) )
7 an4 ⊢ ( ( ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ) ∧ ( 𝑍 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) ) ↔ ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) ) )
8 6 7 bitri ⊢ ( ( 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋 ) ↔ ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) ) )
9 reeanv ⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) ↔ ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) )
10 simplrl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
11 simpll ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
12 simprr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
13 simprl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
14 1 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐵 )
15 11 12 13 14 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐵 )
16 1 2 3 dvdsrmul ⊢ ( ( 𝑌 ∈ 𝐵 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐵 ) → 𝑌 ∥ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑌 ) )
17 10 15 16 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → 𝑌 ∥ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑌 ) )
18 1 3 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑌 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) ) )
19 11 12 13 10 18 syl13anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑌 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) ) )
20 17 19 breqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → 𝑌 ∥ ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) ) )
21 oveq2 ⊢ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 → ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) )
22 id ⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 → ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 )
23 21 22 sylan9eq ⊢ ( ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) → ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) ) = 𝑋 )
24 23 breq2d ⊢ ( ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) → ( 𝑌 ∥ ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) ) ↔ 𝑌 ∥ 𝑋 ) )
25 20 24 syl5ibcom ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) → 𝑌 ∥ 𝑋 ) )
26 25 rexlimdvva ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) → 𝑌 ∥ 𝑋 ) )
27 9 26 biimtrrid ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) → 𝑌 ∥ 𝑋 ) )
28 27 expimpd ⊢ ( 𝑅 ∈ Ring → ( ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑍 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑍 ) = 𝑋 ) ) → 𝑌 ∥ 𝑋 ) )
29 8 28 biimtrid ⊢ ( 𝑅 ∈ Ring → ( ( 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋 ) → 𝑌 ∥ 𝑋 ) )
30 29 3impib ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∥ 𝑍 ∧ 𝑍 ∥ 𝑋 ) → 𝑌 ∥ 𝑋 )