Metamath Proof Explorer

Theorem dvdsruasso

Description: Two elements X and Y of a ring R are associates, i.e. each divides the other, iff they are unit multiples of each 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 ‘ 𝑅 )
dvdsruasso.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
Assertion dvdsruasso ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 ) )

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 dvdsruasso.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
9 1 3 7 dvdsr ⊢ ( 𝑋 ∥ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) )
10 4 biantrurd ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) ) )
11 9 10 bitr4id ⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ↔ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) )
12 1 3 7 dvdsr ⊢ ( 𝑌 ∥ 𝑋 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) )
13 5 biantrurd ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) ) )
14 12 13 bitr4id ⊢ ( 𝜑 → ( 𝑌 ∥ 𝑋 ↔ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) )
15 11 14 anbi12d ⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ( ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) ) )
16 8 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
17 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
18 6 17 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
19 16 18 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
20 19 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
21 oveq1 ⊢ ( 𝑢 = ( 1r ‘ 𝑅 ) → ( 𝑢 · 𝑋 ) = ( ( 1r ‘ 𝑅 ) · 𝑋 ) )
22 21 eqeq1d ⊢ ( 𝑢 = ( 1r ‘ 𝑅 ) → ( ( 𝑢 · 𝑋 ) = 𝑌 ↔ ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑌 ) )
23 22 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) ∧ 𝑢 = ( 1r ‘ 𝑅 ) ) → ( ( 𝑢 · 𝑋 ) = 𝑌 ↔ ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑌 ) )
24 16 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
25 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → 𝑋 ∈ 𝐵 )
26 1 7 17 24 25 ringlidmd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
27 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → 𝑋 = ( 0g ‘ 𝑅 ) )
28 27 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( 𝑡 · 𝑋 ) = ( 𝑡 · ( 0g ‘ 𝑅 ) ) )
29 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( 𝑡 · 𝑋 ) = 𝑌 )
30 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → 𝑡 ∈ 𝐵 )
31 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
32 1 7 31 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑡 ∈ 𝐵 ) → ( 𝑡 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
33 24 30 32 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( 𝑡 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
34 28 29 33 3eqtr3rd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) = 𝑌 )
35 26 27 34 3eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑌 )
36 20 23 35 rspcedvd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 )
37 isidom ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
38 8 37 sylib ⊢ ( 𝜑 → ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
39 38 simpld ⊢ ( 𝜑 → 𝑅 ∈ CRing )
40 39 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ CRing )
41 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑠 ∈ 𝐵 )
42 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑡 ∈ 𝐵 )
43 16 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
44 1 7 43 41 42 ringcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑠 · 𝑡 ) ∈ 𝐵 )
45 1 17 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
46 43 45 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
47 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑋 ∈ 𝐵 )
48 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑋 ≠ ( 0g ‘ 𝑅 ) )
49 eldifsn ⊢ ( 𝑋 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) )
50 47 48 49 sylanbrc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑋 ∈ ( 𝐵 ∖ { ( 0g ‘ 𝑅 ) } ) )
51 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ IDomn )
52 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑡 · 𝑋 ) = 𝑌 )
53 52 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑠 · ( 𝑡 · 𝑋 ) ) = ( 𝑠 · 𝑌 ) )
54 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑠 · 𝑌 ) = 𝑋 )
55 53 54 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑠 · ( 𝑡 · 𝑋 ) ) = 𝑋 )
56 1 7 43 41 42 47 ringassd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝑠 · 𝑡 ) · 𝑋 ) = ( 𝑠 · ( 𝑡 · 𝑋 ) ) )
57 1 7 17 43 47 ringlidmd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · 𝑋 ) = 𝑋 )
58 55 56 57 3eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝑠 · 𝑡 ) · 𝑋 ) = ( ( 1r ‘ 𝑅 ) · 𝑋 ) )
59 1 31 7 44 46 50 51 58 idomrcan ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑠 · 𝑡 ) = ( 1r ‘ 𝑅 ) )
60 43 18 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
61 59 60 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑠 · 𝑡 ) ∈ 𝑈 )
62 6 7 1 unitmulclb ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) → ( ( 𝑠 · 𝑡 ) ∈ 𝑈 ↔ ( 𝑠 ∈ 𝑈 ∧ 𝑡 ∈ 𝑈 ) ) )
63 62 simplbda ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑡 ) ∈ 𝑈 ) → 𝑡 ∈ 𝑈 )
64 40 41 42 61 63 syl31anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑡 ∈ 𝑈 )
65 oveq1 ⊢ ( 𝑢 = 𝑡 → ( 𝑢 · 𝑋 ) = ( 𝑡 · 𝑋 ) )
66 65 eqeq1d ⊢ ( 𝑢 = 𝑡 → ( ( 𝑢 · 𝑋 ) = 𝑌 ↔ ( 𝑡 · 𝑋 ) = 𝑌 ) )
67 66 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑢 = 𝑡 ) → ( ( 𝑢 · 𝑋 ) = 𝑌 ↔ ( 𝑡 · 𝑋 ) = 𝑌 ) )
68 64 67 52 rspcedvd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 )
69 36 68 pm2.61dane ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑡 · 𝑋 ) = 𝑌 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 )
70 69 r19.29an ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 )
71 70 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 )
72 71 ex ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐵 ) ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) → ( ( 𝑠 · 𝑌 ) = 𝑋 → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 ) )
73 72 an32s ⊢ ( ( ( 𝜑 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑠 ∈ 𝐵 ) → ( ( 𝑠 · 𝑌 ) = 𝑋 → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 ) )
74 73 imp ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑠 · 𝑌 ) = 𝑋 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 )
75 74 r19.29an ⊢ ( ( ( 𝜑 ∧ ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ) ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 )
76 75 anasss ⊢ ( ( 𝜑 ∧ ( ∃ 𝑡 ∈ 𝐵 ( 𝑡 · 𝑋 ) = 𝑌 ∧ ∃ 𝑠 ∈ 𝐵 ( 𝑠 · 𝑌 ) = 𝑋 ) ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 )
77 15 76 sylbida ⊢ ( ( 𝜑 ∧ ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 )
78 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → 𝑋 ∈ 𝐵 )
79 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → 𝑌 ∈ 𝐵 )
80 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → 𝑅 ∈ Ring )
81 simplr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → 𝑢 ∈ 𝑈 )
82 simpr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( 𝑢 · 𝑋 ) = 𝑌 )
83 1 2 3 78 79 6 7 80 81 82 dvdsruassoi ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 · 𝑋 ) = 𝑌 ) → ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) )
84 83 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 ) → ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) )
85 77 84 impbida ⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ∃ 𝑢 ∈ 𝑈 ( 𝑢 · 𝑋 ) = 𝑌 ) )