Proof of Theorem rdivmuldivd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rdivmuldivd.a | . . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 2 |  | rdivmuldivd.b | . . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑈) | 
| 3 |  | dvrdir.b | . . . . . 6
⊢ 𝐵 = (Base‘𝑅) | 
| 4 |  | rdivmuldivd.p | . . . . . 6
⊢  · =
(.r‘𝑅) | 
| 5 |  | dvrdir.u | . . . . . 6
⊢ 𝑈 = (Unit‘𝑅) | 
| 6 |  | eqid 2736 | . . . . . 6
⊢
(invr‘𝑅) = (invr‘𝑅) | 
| 7 |  | dvrdir.t | . . . . . 6
⊢  / =
(/r‘𝑅) | 
| 8 | 3, 4, 5, 6, 7 | dvrval 20404 | . . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋 ·
((invr‘𝑅)‘𝑌))) | 
| 9 | 8 | oveq1d 7447 | . . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) · (𝑍 / 𝑊)) = ((𝑋 ·
((invr‘𝑅)‘𝑌)) · (𝑍 / 𝑊))) | 
| 10 | 1, 2, 9 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝑋 / 𝑌) · (𝑍 / 𝑊)) = ((𝑋 ·
((invr‘𝑅)‘𝑌)) · (𝑍 / 𝑊))) | 
| 11 |  | rdivmuldivd.r | . . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 12 |  | crngring 20243 | . . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | 
| 13 | 11, 12 | syl 17 | . . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 14 | 3, 5 | unitss 20377 | . . . . 5
⊢ 𝑈 ⊆ 𝐵 | 
| 15 | 5, 6 | unitinvcl 20391 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈) → ((invr‘𝑅)‘𝑌) ∈ 𝑈) | 
| 16 | 13, 2, 15 | syl2anc 584 | . . . . 5
⊢ (𝜑 →
((invr‘𝑅)‘𝑌) ∈ 𝑈) | 
| 17 | 14, 16 | sselid 3980 | . . . 4
⊢ (𝜑 →
((invr‘𝑅)‘𝑌) ∈ 𝐵) | 
| 18 |  | rdivmuldivd.c | . . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝐵) | 
| 19 |  | rdivmuldivd.d | . . . . 5
⊢ (𝜑 → 𝑊 ∈ 𝑈) | 
| 20 | 3, 5, 7 | dvrcl 20405 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝑈) → (𝑍 / 𝑊) ∈ 𝐵) | 
| 21 | 13, 18, 19, 20 | syl3anc 1372 | . . . 4
⊢ (𝜑 → (𝑍 / 𝑊) ∈ 𝐵) | 
| 22 | 3, 4 | ringass 20251 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑌) ∈ 𝐵 ∧ (𝑍 / 𝑊) ∈ 𝐵)) → ((𝑋 ·
((invr‘𝑅)‘𝑌)) · (𝑍 / 𝑊)) = (𝑋 ·
(((invr‘𝑅)‘𝑌) · (𝑍 / 𝑊)))) | 
| 23 | 13, 1, 17, 21, 22 | syl13anc 1373 | . . 3
⊢ (𝜑 → ((𝑋 ·
((invr‘𝑅)‘𝑌)) · (𝑍 / 𝑊)) = (𝑋 ·
(((invr‘𝑅)‘𝑌) · (𝑍 / 𝑊)))) | 
| 24 | 3, 4 | crngcom 20249 | . . . . 5
⊢ ((𝑅 ∈ CRing ∧
((invr‘𝑅)‘𝑌) ∈ 𝐵 ∧ (𝑍 / 𝑊) ∈ 𝐵) → (((invr‘𝑅)‘𝑌) · (𝑍 / 𝑊)) = ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌))) | 
| 25 | 11, 17, 21, 24 | syl3anc 1372 | . . . 4
⊢ (𝜑 →
(((invr‘𝑅)‘𝑌) · (𝑍 / 𝑊)) = ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌))) | 
| 26 | 25 | oveq2d 7448 | . . 3
⊢ (𝜑 → (𝑋 ·
(((invr‘𝑅)‘𝑌) · (𝑍 / 𝑊))) = (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌)))) | 
| 27 | 10, 23, 26 | 3eqtrd 2780 | . 2
⊢ (𝜑 → ((𝑋 / 𝑌) · (𝑍 / 𝑊)) = (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌)))) | 
| 28 |  | eqid 2736 | . . . . . . . 8
⊢
((mulGrp‘𝑅)
↾s 𝑈) =
((mulGrp‘𝑅)
↾s 𝑈) | 
| 29 | 5, 28 | unitgrp 20384 | . . . . . . 7
⊢ (𝑅 ∈ Ring →
((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp) | 
| 30 | 13, 29 | syl 17 | . . . . . 6
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s 𝑈) ∈ Grp) | 
| 31 | 5, 28 | unitgrpbas 20383 | . . . . . . 7
⊢ 𝑈 =
(Base‘((mulGrp‘𝑅) ↾s 𝑈)) | 
| 32 |  | eqid 2736 | . . . . . . 7
⊢
(+g‘((mulGrp‘𝑅) ↾s 𝑈)) =
(+g‘((mulGrp‘𝑅) ↾s 𝑈)) | 
| 33 | 5, 28, 6 | invrfval 20390 | . . . . . . 7
⊢
(invr‘𝑅) =
(invg‘((mulGrp‘𝑅) ↾s 𝑈)) | 
| 34 | 31, 32, 33 | grpinvadd 19037 | . . . . . 6
⊢
((((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp ∧ 𝑌 ∈
𝑈 ∧ 𝑊 ∈ 𝑈) → ((invr‘𝑅)‘(𝑌(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑊)) = (((invr‘𝑅)‘𝑊)(+g‘((mulGrp‘𝑅) ↾s 𝑈))((invr‘𝑅)‘𝑌))) | 
| 35 | 30, 2, 19, 34 | syl3anc 1372 | . . . . 5
⊢ (𝜑 →
((invr‘𝑅)‘(𝑌(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑊)) = (((invr‘𝑅)‘𝑊)(+g‘((mulGrp‘𝑅) ↾s 𝑈))((invr‘𝑅)‘𝑌))) | 
| 36 |  | eqid 2736 | . . . . . . . . 9
⊢
(mulGrp‘(𝑅
↾s 𝑈)) =
(mulGrp‘(𝑅
↾s 𝑈)) | 
| 37 | 5 | fvexi 6919 | . . . . . . . . . 10
⊢ 𝑈 ∈ V | 
| 38 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈) | 
| 39 | 38, 4 | ressmulr 17352 | . . . . . . . . . 10
⊢ (𝑈 ∈ V → · =
(.r‘(𝑅
↾s 𝑈))) | 
| 40 | 37, 39 | ax-mp 5 | . . . . . . . . 9
⊢  · =
(.r‘(𝑅
↾s 𝑈)) | 
| 41 | 36, 40 | mgpplusg 20142 | . . . . . . . 8
⊢  · =
(+g‘(mulGrp‘(𝑅 ↾s 𝑈))) | 
| 42 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) | 
| 43 | 38, 42 | mgpress 20148 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ V) →
((mulGrp‘𝑅)
↾s 𝑈) =
(mulGrp‘(𝑅
↾s 𝑈))) | 
| 44 | 13, 37, 43 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s 𝑈) = (mulGrp‘(𝑅 ↾s 𝑈))) | 
| 45 | 44 | fveq2d 6909 | . . . . . . . 8
⊢ (𝜑 →
(+g‘((mulGrp‘𝑅) ↾s 𝑈)) =
(+g‘(mulGrp‘(𝑅 ↾s 𝑈)))) | 
| 46 | 41, 45 | eqtr4id 2795 | . . . . . . 7
⊢ (𝜑 → · =
(+g‘((mulGrp‘𝑅) ↾s 𝑈))) | 
| 47 | 46 | oveqd 7449 | . . . . . 6
⊢ (𝜑 → (𝑌 · 𝑊) = (𝑌(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑊)) | 
| 48 | 47 | fveq2d 6909 | . . . . 5
⊢ (𝜑 →
((invr‘𝑅)‘(𝑌 · 𝑊)) = ((invr‘𝑅)‘(𝑌(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑊))) | 
| 49 | 46 | oveqd 7449 | . . . . 5
⊢ (𝜑 →
(((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌)) = (((invr‘𝑅)‘𝑊)(+g‘((mulGrp‘𝑅) ↾s 𝑈))((invr‘𝑅)‘𝑌))) | 
| 50 | 35, 48, 49 | 3eqtr4d 2786 | . . . 4
⊢ (𝜑 →
((invr‘𝑅)‘(𝑌 · 𝑊)) = (((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌))) | 
| 51 | 50 | oveq2d 7448 | . . 3
⊢ (𝜑 → ((𝑋 · 𝑍) ·
((invr‘𝑅)‘(𝑌 · 𝑊))) = ((𝑋 · 𝑍) ·
(((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌)))) | 
| 52 | 3, 4 | ringcl 20248 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 · 𝑍) ∈ 𝐵) | 
| 53 | 13, 1, 18, 52 | syl3anc 1372 | . . . 4
⊢ (𝜑 → (𝑋 · 𝑍) ∈ 𝐵) | 
| 54 | 5, 4 | unitmulcl 20381 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ∧ 𝑊 ∈ 𝑈) → (𝑌 · 𝑊) ∈ 𝑈) | 
| 55 | 13, 2, 19, 54 | syl3anc 1372 | . . . 4
⊢ (𝜑 → (𝑌 · 𝑊) ∈ 𝑈) | 
| 56 | 3, 4, 5, 6, 7 | dvrval 20404 | . . . 4
⊢ (((𝑋 · 𝑍) ∈ 𝐵 ∧ (𝑌 · 𝑊) ∈ 𝑈) → ((𝑋 · 𝑍) / (𝑌 · 𝑊)) = ((𝑋 · 𝑍) ·
((invr‘𝑅)‘(𝑌 · 𝑊)))) | 
| 57 | 53, 55, 56 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝑋 · 𝑍) / (𝑌 · 𝑊)) = ((𝑋 · 𝑍) ·
((invr‘𝑅)‘(𝑌 · 𝑊)))) | 
| 58 | 5, 6 | unitinvcl 20391 | . . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑊 ∈ 𝑈) → ((invr‘𝑅)‘𝑊) ∈ 𝑈) | 
| 59 | 13, 19, 58 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 →
((invr‘𝑅)‘𝑊) ∈ 𝑈) | 
| 60 | 14, 59 | sselid 3980 | . . . . . . 7
⊢ (𝜑 →
((invr‘𝑅)‘𝑊) ∈ 𝐵) | 
| 61 | 3, 4 | ringass 20251 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑊) ∈ 𝐵)) → ((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) = (𝑋 · (𝑍 ·
((invr‘𝑅)‘𝑊)))) | 
| 62 | 13, 1, 18, 60, 61 | syl13anc 1373 | . . . . . 6
⊢ (𝜑 → ((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) = (𝑋 · (𝑍 ·
((invr‘𝑅)‘𝑊)))) | 
| 63 | 3, 4, 5, 6, 7 | dvrval 20404 | . . . . . . . 8
⊢ ((𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝑈) → (𝑍 / 𝑊) = (𝑍 ·
((invr‘𝑅)‘𝑊))) | 
| 64 | 18, 19, 63 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝑍 / 𝑊) = (𝑍 ·
((invr‘𝑅)‘𝑊))) | 
| 65 | 64 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (𝑋 · (𝑍 / 𝑊)) = (𝑋 · (𝑍 ·
((invr‘𝑅)‘𝑊)))) | 
| 66 | 62, 65 | eqtr4d 2779 | . . . . 5
⊢ (𝜑 → ((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) = (𝑋 · (𝑍 / 𝑊))) | 
| 67 | 66 | oveq1d 7447 | . . . 4
⊢ (𝜑 → (((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) ·
((invr‘𝑅)‘𝑌)) = ((𝑋 · (𝑍 / 𝑊)) ·
((invr‘𝑅)‘𝑌))) | 
| 68 | 3, 4 | ringass 20251 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ ((𝑋 · 𝑍) ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑊) ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑌) ∈ 𝐵)) → (((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) ·
((invr‘𝑅)‘𝑌)) = ((𝑋 · 𝑍) ·
(((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌)))) | 
| 69 | 13, 53, 60, 17, 68 | syl13anc 1373 | . . . 4
⊢ (𝜑 → (((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) ·
((invr‘𝑅)‘𝑌)) = ((𝑋 · 𝑍) ·
(((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌)))) | 
| 70 | 3, 4 | ringass 20251 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ (𝑍 / 𝑊) ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑌) ∈ 𝐵)) → ((𝑋 · (𝑍 / 𝑊)) ·
((invr‘𝑅)‘𝑌)) = (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌)))) | 
| 71 | 13, 1, 21, 17, 70 | syl13anc 1373 | . . . 4
⊢ (𝜑 → ((𝑋 · (𝑍 / 𝑊)) ·
((invr‘𝑅)‘𝑌)) = (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌)))) | 
| 72 | 67, 69, 71 | 3eqtr3rd 2785 | . . 3
⊢ (𝜑 → (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌))) = ((𝑋 · 𝑍) ·
(((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌)))) | 
| 73 | 51, 57, 72 | 3eqtr4rd 2787 | . 2
⊢ (𝜑 → (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌))) = ((𝑋 · 𝑍) / (𝑌 · 𝑊))) | 
| 74 | 27, 73 | eqtrd 2776 | 1
⊢ (𝜑 → ((𝑋 / 𝑌) · (𝑍 / 𝑊)) = ((𝑋 · 𝑍) / (𝑌 · 𝑊))) |