| 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 ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∥ 𝑌 ) → ( 𝑋 · 𝑍 ) ∥ ( 𝑌 · 𝑍 ) ) |