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

Metamath Proof Explorer

Theorem dvdsruassoi

Description: If two elements X and Y of a ring R are unit multiples, then they are associates, i.e. each divides the other. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses dvdsrspss.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvdsrspss.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
dvdsrspss.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
dvdsrspss.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
dvdsrspss.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
dvdsruassoi.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dvdsruassoi.2 ⊢ · = ( .r ‘ 𝑅 )
dvdsruassoi.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
dvdsruassoi.3 ⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
dvdsruassoi.4 ⊢ ( 𝜑 → ( 𝑉 · 𝑋 ) = 𝑌 )
Assertion dvdsruassoi ( 𝜑 → ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 dvdsrspss.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dvdsrspss.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3 dvdsrspss.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
4 dvdsrspss.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 dvdsrspss.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 dvdsruassoi.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
7 dvdsruassoi.2 ⊢ · = ( .r ‘ 𝑅 )
8 dvdsruassoi.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
9 dvdsruassoi.3 ⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
10 dvdsruassoi.4 ⊢ ( 𝜑 → ( 𝑉 · 𝑋 ) = 𝑌 )
11 1 6 unitss ⊢ 𝑈 ⊆ 𝐵
12 11 9 sselid ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
13 oveq1 ⊢ ( 𝑡 = 𝑉 → ( 𝑡 · 𝑋 ) = ( 𝑉 · 𝑋 ) )
14 13 eqeq1d ⊢ ( 𝑡 = 𝑉 → ( ( 𝑡 · 𝑋 ) = 𝑌 ↔ ( 𝑉 · 𝑋 ) = 𝑌 ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑡 = 𝑉 ) → ( ( 𝑡 · 𝑋 ) = 𝑌 ↔ ( 𝑉 · 𝑋 ) = 𝑌 ) )
16 12 15 10 rspcedvd ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 )
17 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
18 6 17 1 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑉 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) ∈ 𝐵 )
19 8 9 18 syl2anc ⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) ∈ 𝐵 )
20 oveq1 ⊢ ( 𝑠 = ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) → ( 𝑠 · 𝑌 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑌 ) )
21 20 eqeq1d ⊢ ( 𝑠 = ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) → ( ( 𝑠 · 𝑌 ) = 𝑋 ↔ ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑌 ) = 𝑋 ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑠 = ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) ) → ( ( 𝑠 · 𝑌 ) = 𝑋 ↔ ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑌 ) = 𝑋 ) )
23 1 7 8 19 12 4 ringassd ⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑉 ) · 𝑋 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · ( 𝑉 · 𝑋 ) ) )
24 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
25 6 17 7 24 unitlinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑉 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑉 ) = ( 1r ‘ 𝑅 ) )
26 8 9 25 syl2anc ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑉 ) = ( 1r ‘ 𝑅 ) )
27 26 oveq1d ⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑉 ) · 𝑋 ) = ( ( 1r ‘ 𝑅 ) · 𝑋 ) )
28 1 7 24 8 4 ringlidmd ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
29 27 28 eqtrd ⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑉 ) · 𝑋 ) = 𝑋 )
30 10 oveq2d ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · ( 𝑉 · 𝑋 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑌 ) )
31 23 29 30 3eqtr3rd ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑉 ) · 𝑌 ) = 𝑋 )
32 19 22 31 rspcedvd ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 )
33 1 3 7 dvdsr ⊢ ( 𝑋 ∥ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) )
34 4 biantrurd ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) ) )
35 33 34 bitr4id ⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ↔ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) )
36 1 3 7 dvdsr ⊢ ( 𝑌 ∥ 𝑋 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) )
37 5 biantrurd ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) ) )
38 36 37 bitr4id ⊢ ( 𝜑 → ( 𝑌 ∥ 𝑋 ↔ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) )
39 35 38 anbi12d ⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ( ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) ) )
40 16 32 39 mpbir2and ⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) )