This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdsrmul1

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

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

Proof

Step Hyp Ref Expression
1 dvdsr.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dvdsr.2 ⊢ ∥ = ( ∥r ‘ 𝑅 )
3 dvdsrmul1.3 ⊢ · = ( .r ‘ 𝑅 )
4 1 2 3 dvdsr ⊢ ( 𝑋 ∥ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 · 𝑋 ) = 𝑌 ) )
5 simplll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Ring )
6 simplr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7 simpllr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑍 ∈ 𝐵 )
8 1 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
9 5 6 7 8 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
10 1 2 3 dvdsrmul ⊢ ( ( ( 𝑋 · 𝑍 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) ∥ ( 𝑥 · ( 𝑋 · 𝑍 ) ) )
11 9 10 sylancom ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) ∥ ( 𝑥 · ( 𝑋 · 𝑍 ) ) )
12 simpr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
13 1 3 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑥 · 𝑋 ) · 𝑍 ) = ( 𝑥 · ( 𝑋 · 𝑍 ) ) )
14 5 12 6 7 13 syl13anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 · 𝑋 ) · 𝑍 ) = ( 𝑥 · ( 𝑋 · 𝑍 ) ) )
15 11 14 breqtrrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) ∥ ( ( 𝑥 · 𝑋 ) · 𝑍 ) )
16 oveq1 ⊢ ( ( 𝑥 · 𝑋 ) = 𝑌 → ( ( 𝑥 · 𝑋 ) · 𝑍 ) = ( 𝑌 · 𝑍 ) )
17 16 breq2d ⊢ ( ( 𝑥 · 𝑋 ) = 𝑌 → ( ( 𝑋 · 𝑍 ) ∥ ( ( 𝑥 · 𝑋 ) · 𝑍 ) ↔ ( 𝑋 · 𝑍 ) ∥ ( 𝑌 · 𝑍 ) ) )
18 15 17 syl5ibcom ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 · 𝑋 ) = 𝑌 → ( 𝑋 · 𝑍 ) ∥ ( 𝑌 · 𝑍 ) ) )
19 18 rexlimdva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 · 𝑋 ) = 𝑌 → ( 𝑋 · 𝑍 ) ∥ ( 𝑌 · 𝑍 ) ) )
20 19 expimpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 · 𝑋 ) = 𝑌 ) → ( 𝑋 · 𝑍 ) ∥ ( 𝑌 · 𝑍 ) ) )
21 4 20 biimtrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∥ 𝑌 → ( 𝑋 · 𝑍 ) ∥ ( 𝑌 · 𝑍 ) ) )
22 21 3impia ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∥ 𝑌 ) → ( 𝑋 · 𝑍 ) ∥ ( 𝑌 · 𝑍 ) )