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 2610 |
. . . . . 6
⊢
(invr‘𝑅) = (invr‘𝑅) |
7 | | dvrdir.t |
. . . . . 6
⊢ / =
(/r‘𝑅) |
8 | 3, 4, 5, 6, 7 | dvrval 18508 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋 ·
((invr‘𝑅)‘𝑌))) |
9 | 8 | oveq1d 6564 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → ((𝑋 / 𝑌) · (𝑍 / 𝑊)) = ((𝑋 ·
((invr‘𝑅)‘𝑌)) · (𝑍 / 𝑊))) |
10 | 1, 2, 9 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((𝑋 / 𝑌) · (𝑍 / 𝑊)) = ((𝑋 ·
((invr‘𝑅)‘𝑌)) · (𝑍 / 𝑊))) |
11 | | rdivmuldivd.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
12 | | crngring 18381 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
14 | 3, 5 | unitss 18483 |
. . . . 5
⊢ 𝑈 ⊆ 𝐵 |
15 | 5, 6 | unitinvcl 18497 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈) → ((invr‘𝑅)‘𝑌) ∈ 𝑈) |
16 | 13, 2, 15 | syl2anc 691 |
. . . . 5
⊢ (𝜑 →
((invr‘𝑅)‘𝑌) ∈ 𝑈) |
17 | 14, 16 | sseldi 3566 |
. . . 4
⊢ (𝜑 →
((invr‘𝑅)‘𝑌) ∈ 𝐵) |
18 | | rdivmuldivd.c |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
19 | | rdivmuldivd.d |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ 𝑈) |
20 | 3, 5, 7 | dvrcl 18509 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝑈) → (𝑍 / 𝑊) ∈ 𝐵) |
21 | 13, 18, 19, 20 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (𝑍 / 𝑊) ∈ 𝐵) |
22 | 3, 4 | ringass 18387 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑌) ∈ 𝐵 ∧ (𝑍 / 𝑊) ∈ 𝐵)) → ((𝑋 ·
((invr‘𝑅)‘𝑌)) · (𝑍 / 𝑊)) = (𝑋 ·
(((invr‘𝑅)‘𝑌) · (𝑍 / 𝑊)))) |
23 | 13, 1, 17, 21, 22 | syl13anc 1320 |
. . 3
⊢ (𝜑 → ((𝑋 ·
((invr‘𝑅)‘𝑌)) · (𝑍 / 𝑊)) = (𝑋 ·
(((invr‘𝑅)‘𝑌) · (𝑍 / 𝑊)))) |
24 | 3, 4 | crngcom 18385 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧
((invr‘𝑅)‘𝑌) ∈ 𝐵 ∧ (𝑍 / 𝑊) ∈ 𝐵) → (((invr‘𝑅)‘𝑌) · (𝑍 / 𝑊)) = ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌))) |
25 | 11, 17, 21, 24 | syl3anc 1318 |
. . . 4
⊢ (𝜑 →
(((invr‘𝑅)‘𝑌) · (𝑍 / 𝑊)) = ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌))) |
26 | 25 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (𝑋 ·
(((invr‘𝑅)‘𝑌) · (𝑍 / 𝑊))) = (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌)))) |
27 | 10, 23, 26 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → ((𝑋 / 𝑌) · (𝑍 / 𝑊)) = (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌)))) |
28 | | eqid 2610 |
. . . . . . . 8
⊢
((mulGrp‘𝑅)
↾s 𝑈) =
((mulGrp‘𝑅)
↾s 𝑈) |
29 | 5, 28 | unitgrp 18490 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp) |
30 | 13, 29 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s 𝑈) ∈ Grp) |
31 | 5, 28 | unitgrpbas 18489 |
. . . . . . 7
⊢ 𝑈 =
(Base‘((mulGrp‘𝑅) ↾s 𝑈)) |
32 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘((mulGrp‘𝑅) ↾s 𝑈)) =
(+g‘((mulGrp‘𝑅) ↾s 𝑈)) |
33 | 5, 28, 6 | invrfval 18496 |
. . . . . . 7
⊢
(invr‘𝑅) =
(invg‘((mulGrp‘𝑅) ↾s 𝑈)) |
34 | 31, 32, 33 | grpinvadd 17316 |
. . . . . 6
⊢
((((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp ∧ 𝑌 ∈
𝑈 ∧ 𝑊 ∈ 𝑈) → ((invr‘𝑅)‘(𝑌(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑊)) = (((invr‘𝑅)‘𝑊)(+g‘((mulGrp‘𝑅) ↾s 𝑈))((invr‘𝑅)‘𝑌))) |
35 | 30, 2, 19, 34 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 →
((invr‘𝑅)‘(𝑌(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑊)) = (((invr‘𝑅)‘𝑊)(+g‘((mulGrp‘𝑅) ↾s 𝑈))((invr‘𝑅)‘𝑌))) |
36 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(Unit‘𝑅)
∈ V |
37 | 5, 36 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝑈 ∈ V |
38 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈) |
39 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
40 | 38, 39 | mgpress 18323 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑈 ∈ V) →
((mulGrp‘𝑅)
↾s 𝑈) =
(mulGrp‘(𝑅
↾s 𝑈))) |
41 | 13, 37, 40 | sylancl 693 |
. . . . . . . . 9
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s 𝑈) = (mulGrp‘(𝑅 ↾s 𝑈))) |
42 | 41 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 →
(+g‘((mulGrp‘𝑅) ↾s 𝑈)) =
(+g‘(mulGrp‘(𝑅 ↾s 𝑈)))) |
43 | | eqid 2610 |
. . . . . . . . 9
⊢
(mulGrp‘(𝑅
↾s 𝑈)) =
(mulGrp‘(𝑅
↾s 𝑈)) |
44 | 38, 4 | ressmulr 15829 |
. . . . . . . . . 10
⊢ (𝑈 ∈ V → · =
(.r‘(𝑅
↾s 𝑈))) |
45 | 37, 44 | ax-mp 5 |
. . . . . . . . 9
⊢ · =
(.r‘(𝑅
↾s 𝑈)) |
46 | 43, 45 | mgpplusg 18316 |
. . . . . . . 8
⊢ · =
(+g‘(mulGrp‘(𝑅 ↾s 𝑈))) |
47 | 42, 46 | syl6reqr 2663 |
. . . . . . 7
⊢ (𝜑 → · =
(+g‘((mulGrp‘𝑅) ↾s 𝑈))) |
48 | 47 | oveqd 6566 |
. . . . . 6
⊢ (𝜑 → (𝑌 · 𝑊) = (𝑌(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑊)) |
49 | 48 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 →
((invr‘𝑅)‘(𝑌 · 𝑊)) = ((invr‘𝑅)‘(𝑌(+g‘((mulGrp‘𝑅) ↾s 𝑈))𝑊))) |
50 | 47 | oveqd 6566 |
. . . . 5
⊢ (𝜑 →
(((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌)) = (((invr‘𝑅)‘𝑊)(+g‘((mulGrp‘𝑅) ↾s 𝑈))((invr‘𝑅)‘𝑌))) |
51 | 35, 49, 50 | 3eqtr4d 2654 |
. . . 4
⊢ (𝜑 →
((invr‘𝑅)‘(𝑌 · 𝑊)) = (((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌))) |
52 | 51 | oveq2d 6565 |
. . 3
⊢ (𝜑 → ((𝑋 · 𝑍) ·
((invr‘𝑅)‘(𝑌 · 𝑊))) = ((𝑋 · 𝑍) ·
(((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌)))) |
53 | 3, 4 | ringcl 18384 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 · 𝑍) ∈ 𝐵) |
54 | 13, 1, 18, 53 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (𝑋 · 𝑍) ∈ 𝐵) |
55 | 5, 4 | unitmulcl 18487 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ∧ 𝑊 ∈ 𝑈) → (𝑌 · 𝑊) ∈ 𝑈) |
56 | 13, 2, 19, 55 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (𝑌 · 𝑊) ∈ 𝑈) |
57 | 3, 4, 5, 6, 7 | dvrval 18508 |
. . . 4
⊢ (((𝑋 · 𝑍) ∈ 𝐵 ∧ (𝑌 · 𝑊) ∈ 𝑈) → ((𝑋 · 𝑍) / (𝑌 · 𝑊)) = ((𝑋 · 𝑍) ·
((invr‘𝑅)‘(𝑌 · 𝑊)))) |
58 | 54, 56, 57 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((𝑋 · 𝑍) / (𝑌 · 𝑊)) = ((𝑋 · 𝑍) ·
((invr‘𝑅)‘(𝑌 · 𝑊)))) |
59 | 5, 6 | unitinvcl 18497 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑊 ∈ 𝑈) → ((invr‘𝑅)‘𝑊) ∈ 𝑈) |
60 | 13, 19, 59 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 →
((invr‘𝑅)‘𝑊) ∈ 𝑈) |
61 | 14, 60 | sseldi 3566 |
. . . . . . 7
⊢ (𝜑 →
((invr‘𝑅)‘𝑊) ∈ 𝐵) |
62 | 3, 4 | ringass 18387 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑊) ∈ 𝐵)) → ((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) = (𝑋 · (𝑍 ·
((invr‘𝑅)‘𝑊)))) |
63 | 13, 1, 18, 61, 62 | syl13anc 1320 |
. . . . . 6
⊢ (𝜑 → ((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) = (𝑋 · (𝑍 ·
((invr‘𝑅)‘𝑊)))) |
64 | 3, 4, 5, 6, 7 | dvrval 18508 |
. . . . . . . 8
⊢ ((𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝑈) → (𝑍 / 𝑊) = (𝑍 ·
((invr‘𝑅)‘𝑊))) |
65 | 18, 19, 64 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑍 / 𝑊) = (𝑍 ·
((invr‘𝑅)‘𝑊))) |
66 | 65 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (𝑋 · (𝑍 / 𝑊)) = (𝑋 · (𝑍 ·
((invr‘𝑅)‘𝑊)))) |
67 | 63, 66 | eqtr4d 2647 |
. . . . 5
⊢ (𝜑 → ((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) = (𝑋 · (𝑍 / 𝑊))) |
68 | 67 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → (((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) ·
((invr‘𝑅)‘𝑌)) = ((𝑋 · (𝑍 / 𝑊)) ·
((invr‘𝑅)‘𝑌))) |
69 | 3, 4 | ringass 18387 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ ((𝑋 · 𝑍) ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑊) ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑌) ∈ 𝐵)) → (((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) ·
((invr‘𝑅)‘𝑌)) = ((𝑋 · 𝑍) ·
(((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌)))) |
70 | 13, 54, 61, 17, 69 | syl13anc 1320 |
. . . 4
⊢ (𝜑 → (((𝑋 · 𝑍) ·
((invr‘𝑅)‘𝑊)) ·
((invr‘𝑅)‘𝑌)) = ((𝑋 · 𝑍) ·
(((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌)))) |
71 | 3, 4 | ringass 18387 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ (𝑍 / 𝑊) ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑌) ∈ 𝐵)) → ((𝑋 · (𝑍 / 𝑊)) ·
((invr‘𝑅)‘𝑌)) = (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌)))) |
72 | 13, 1, 21, 17, 71 | syl13anc 1320 |
. . . 4
⊢ (𝜑 → ((𝑋 · (𝑍 / 𝑊)) ·
((invr‘𝑅)‘𝑌)) = (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌)))) |
73 | 68, 70, 72 | 3eqtr3rd 2653 |
. . 3
⊢ (𝜑 → (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌))) = ((𝑋 · 𝑍) ·
(((invr‘𝑅)‘𝑊) ·
((invr‘𝑅)‘𝑌)))) |
74 | 52, 58, 73 | 3eqtr4rd 2655 |
. 2
⊢ (𝜑 → (𝑋 · ((𝑍 / 𝑊) ·
((invr‘𝑅)‘𝑌))) = ((𝑋 · 𝑍) / (𝑌 · 𝑊))) |
75 | 27, 74 | eqtrd 2644 |
1
⊢ (𝜑 → ((𝑋 / 𝑌) · (𝑍 / 𝑊)) = ((𝑋 · 𝑍) / (𝑌 · 𝑊))) |