| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dvdsrspss.b | . . . . . 6
⊢ 𝐵 = (Base‘𝑅) | 
| 2 |  | dvdsrspss.d | . . . . . 6
⊢  ∥ =
(∥r‘𝑅) | 
| 3 |  | dvdsruassoi.2 | . . . . . 6
⊢  · =
(.r‘𝑅) | 
| 4 | 1, 2, 3 | dvdsr 20363 | . . . . 5
⊢ (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌)) | 
| 5 |  | dvdsrspss.x | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 6 | 5 | biantrurd 532 | . . . . 5
⊢ (𝜑 → (∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌))) | 
| 7 | 4, 6 | bitr4id 290 | . . . 4
⊢ (𝜑 → (𝑋 ∥ 𝑌 ↔ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌)) | 
| 8 | 1, 2, 3 | dvdsr 20363 | . . . . 5
⊢ (𝑌 ∥ 𝑋 ↔ (𝑌 ∈ 𝐵 ∧ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋)) | 
| 9 |  | dvdsrspss.y | . . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) | 
| 10 | 9 | biantrurd 532 | . . . . 5
⊢ (𝜑 → (∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋 ↔ (𝑌 ∈ 𝐵 ∧ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋))) | 
| 11 | 8, 10 | bitr4id 290 | . . . 4
⊢ (𝜑 → (𝑌 ∥ 𝑋 ↔ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋)) | 
| 12 | 7, 11 | anbi12d 632 | . . 3
⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ (∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌 ∧ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋))) | 
| 13 |  | dvdsruasso.r | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ IDomn) | 
| 14 | 13 | idomringd 20729 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 15 |  | dvdsruassoi.1 | . . . . . . . . . . . . . . 15
⊢ 𝑈 = (Unit‘𝑅) | 
| 16 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 17 | 15, 16 | 1unit 20375 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝑈) | 
| 18 | 14, 17 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1r‘𝑅) ∈ 𝑈) | 
| 19 | 18 | ad5antr 734 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → (1r‘𝑅) ∈ 𝑈) | 
| 20 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑢 = (1r‘𝑅) → (𝑢 · 𝑋) = ((1r‘𝑅) · 𝑋)) | 
| 21 | 20 | eqeq1d 2738 | . . . . . . . . . . . . 13
⊢ (𝑢 = (1r‘𝑅) → ((𝑢 · 𝑋) = 𝑌 ↔ ((1r‘𝑅) · 𝑋) = 𝑌)) | 
| 22 | 21 | adantl 481 | . . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) ∧ 𝑢 = (1r‘𝑅)) → ((𝑢 · 𝑋) = 𝑌 ↔ ((1r‘𝑅) · 𝑋) = 𝑌)) | 
| 23 | 14 | ad5antr 734 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → 𝑅 ∈ Ring) | 
| 24 | 5 | ad5antr 734 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → 𝑋 ∈ 𝐵) | 
| 25 | 1, 3, 16, 23, 24 | ringlidmd 20270 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → ((1r‘𝑅) · 𝑋) = 𝑋) | 
| 26 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → 𝑋 = (0g‘𝑅)) | 
| 27 | 26 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → (𝑡 · 𝑋) = (𝑡 ·
(0g‘𝑅))) | 
| 28 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → (𝑡 · 𝑋) = 𝑌) | 
| 29 |  | simpllr 775 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → 𝑡 ∈ 𝐵) | 
| 30 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 31 | 1, 3, 30 | ringrz 20292 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑡 ∈ 𝐵) → (𝑡 ·
(0g‘𝑅)) =
(0g‘𝑅)) | 
| 32 | 23, 29, 31 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → (𝑡 ·
(0g‘𝑅)) =
(0g‘𝑅)) | 
| 33 | 27, 28, 32 | 3eqtr3rd 2785 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → (0g‘𝑅) = 𝑌) | 
| 34 | 25, 26, 33 | 3eqtrd 2780 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → ((1r‘𝑅) · 𝑋) = 𝑌) | 
| 35 | 19, 22, 34 | rspcedvd 3623 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 = (0g‘𝑅)) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) | 
| 36 |  | isidom 20726 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) | 
| 37 | 13, 36 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) | 
| 38 | 37 | simpld 494 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 39 | 38 | ad5antr 734 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑅 ∈ CRing) | 
| 40 |  | simp-5r 785 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑠 ∈ 𝐵) | 
| 41 |  | simpllr 775 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑡 ∈ 𝐵) | 
| 42 | 14 | ad5antr 734 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑅 ∈ Ring) | 
| 43 | 1, 3, 42, 40, 41 | ringcld 20258 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · 𝑡) ∈ 𝐵) | 
| 44 | 1, 16 | ringidcl 20263 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) | 
| 45 | 42, 44 | syl 17 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (1r‘𝑅) ∈ 𝐵) | 
| 46 | 5 | ad5antr 734 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑋 ∈ 𝐵) | 
| 47 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑋 ≠ (0g‘𝑅)) | 
| 48 |  | eldifsn 4785 | . . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ (𝐵 ∖ {(0g‘𝑅)}) ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ (0g‘𝑅))) | 
| 49 | 46, 47, 48 | sylanbrc 583 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑋 ∈ (𝐵 ∖ {(0g‘𝑅)})) | 
| 50 | 13 | ad5antr 734 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑅 ∈ IDomn) | 
| 51 |  | simplr 768 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑡 · 𝑋) = 𝑌) | 
| 52 | 51 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · (𝑡 · 𝑋)) = (𝑠 · 𝑌)) | 
| 53 |  | simp-4r 783 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · 𝑌) = 𝑋) | 
| 54 | 52, 53 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · (𝑡 · 𝑋)) = 𝑋) | 
| 55 | 1, 3, 42, 40, 41, 46 | ringassd 20255 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → ((𝑠 · 𝑡) · 𝑋) = (𝑠 · (𝑡 · 𝑋))) | 
| 56 | 1, 3, 16, 42, 46 | ringlidmd 20270 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → ((1r‘𝑅) · 𝑋) = 𝑋) | 
| 57 | 54, 55, 56 | 3eqtr4d 2786 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → ((𝑠 · 𝑡) · 𝑋) = ((1r‘𝑅) · 𝑋)) | 
| 58 | 1, 30, 3, 43, 45, 49, 50, 57 | idomrcan 33283 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · 𝑡) = (1r‘𝑅)) | 
| 59 | 42, 17 | syl 17 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (1r‘𝑅) ∈ 𝑈) | 
| 60 | 58, 59 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → (𝑠 · 𝑡) ∈ 𝑈) | 
| 61 | 15, 3, 1 | unitmulclb 20382 | . . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ CRing ∧ 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → ((𝑠 · 𝑡) ∈ 𝑈 ↔ (𝑠 ∈ 𝑈 ∧ 𝑡 ∈ 𝑈))) | 
| 62 | 61 | simplbda 499 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ (𝑠 · 𝑡) ∈ 𝑈) → 𝑡 ∈ 𝑈) | 
| 63 | 39, 40, 41, 60, 62 | syl31anc 1374 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑡 ∈ 𝑈) | 
| 64 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑡 → (𝑢 · 𝑋) = (𝑡 · 𝑋)) | 
| 65 | 64 | eqeq1d 2738 | . . . . . . . . . . . . 13
⊢ (𝑢 = 𝑡 → ((𝑢 · 𝑋) = 𝑌 ↔ (𝑡 · 𝑋) = 𝑌)) | 
| 66 | 65 | adantl 481 | . . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) ∧ 𝑢 = 𝑡) → ((𝑢 · 𝑋) = 𝑌 ↔ (𝑡 · 𝑋) = 𝑌)) | 
| 67 | 63, 66, 51 | rspcedvd 3623 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) ∧ 𝑋 ≠ (0g‘𝑅)) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) | 
| 68 | 35, 67 | pm2.61dane 3028 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ 𝑡 ∈ 𝐵) ∧ (𝑡 · 𝑋) = 𝑌) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) | 
| 69 | 68 | r19.29an 3157 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) | 
| 70 | 69 | an32s 652 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) ∧ (𝑠 · 𝑌) = 𝑋) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) | 
| 71 | 70 | ex 412 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) → ((𝑠 · 𝑌) = 𝑋 → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)) | 
| 72 | 71 | an32s 652 | . . . . . 6
⊢ (((𝜑 ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) ∧ 𝑠 ∈ 𝐵) → ((𝑠 · 𝑌) = 𝑋 → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)) | 
| 73 | 72 | imp 406 | . . . . 5
⊢ ((((𝜑 ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) ∧ 𝑠 ∈ 𝐵) ∧ (𝑠 · 𝑌) = 𝑋) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) | 
| 74 | 73 | r19.29an 3157 | . . . 4
⊢ (((𝜑 ∧ ∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌) ∧ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) | 
| 75 | 74 | anasss 466 | . . 3
⊢ ((𝜑 ∧ (∃𝑡 ∈ 𝐵 (𝑡 · 𝑋) = 𝑌 ∧ ∃𝑠 ∈ 𝐵 (𝑠 · 𝑌) = 𝑋)) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) | 
| 76 | 12, 75 | sylbida 592 | . 2
⊢ ((𝜑 ∧ (𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋)) → ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) | 
| 77 |  | dvdsrspss.k | . . . 4
⊢ 𝐾 = (RSpan‘𝑅) | 
| 78 | 5 | ad2antrr 726 | . . . 4
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → 𝑋 ∈ 𝐵) | 
| 79 | 9 | ad2antrr 726 | . . . 4
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → 𝑌 ∈ 𝐵) | 
| 80 | 14 | ad2antrr 726 | . . . 4
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → 𝑅 ∈ Ring) | 
| 81 |  | simplr 768 | . . . 4
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → 𝑢 ∈ 𝑈) | 
| 82 |  | simpr 484 | . . . 4
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → (𝑢 · 𝑋) = 𝑌) | 
| 83 | 1, 77, 2, 78, 79, 15, 3, 80, 81, 82 | dvdsruassoi 33413 | . . 3
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 · 𝑋) = 𝑌) → (𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋)) | 
| 84 | 83 | r19.29an 3157 | . 2
⊢ ((𝜑 ∧ ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌) → (𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋)) | 
| 85 | 76, 84 | impbida 800 | 1
⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)) |