Proof of Theorem dvrcan5
Step | Hyp | Ref
| Expression |
1 | | dvrcan5.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
2 | | dvrcan5.o |
. . . . . . 7
⊢ 𝑈 = (Unit‘𝑅) |
3 | 1, 2 | unitss 18660 |
. . . . . 6
⊢ 𝑈 ⊆ 𝐵 |
4 | | simpr3 1069 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → 𝑍 ∈ 𝑈) |
5 | 3, 4 | sseldi 3601 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → 𝑍 ∈ 𝐵) |
6 | | dvrcan5.t |
. . . . . . 7
⊢ · =
(.r‘𝑅) |
7 | 2, 6 | unitmulcl 18664 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈) → (𝑌 · 𝑍) ∈ 𝑈) |
8 | 7 | 3adant3r1 1274 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑌 · 𝑍) ∈ 𝑈) |
9 | | eqid 2622 |
. . . . . 6
⊢
(invr‘𝑅) = (invr‘𝑅) |
10 | | dvrcan5.d |
. . . . . 6
⊢ / =
(/r‘𝑅) |
11 | 1, 6, 2, 9, 10 | dvrval 18685 |
. . . . 5
⊢ ((𝑍 ∈ 𝐵 ∧ (𝑌 · 𝑍) ∈ 𝑈) → (𝑍 / (𝑌 · 𝑍)) = (𝑍 ·
((invr‘𝑅)‘(𝑌 · 𝑍)))) |
12 | 5, 8, 11 | syl2anc 693 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑍 / (𝑌 · 𝑍)) = (𝑍 ·
((invr‘𝑅)‘(𝑌 · 𝑍)))) |
13 | | simpl 473 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → 𝑅 ∈ Ring) |
14 | | eqid 2622 |
. . . . . . 7
⊢
((mulGrp‘𝑅)
↾s 𝑈) =
((mulGrp‘𝑅)
↾s 𝑈) |
15 | 2, 14 | unitgrp 18667 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp) |
16 | 13, 15 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((mulGrp‘𝑅) ↾s 𝑈) ∈ Grp) |
17 | | simpr2 1068 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → 𝑌 ∈ 𝑈) |
18 | 2, 14 | unitgrpbas 18666 |
. . . . . . 7
⊢ 𝑈 =
(Base‘((mulGrp‘𝑅) ↾s 𝑈)) |
19 | | fvex 6201 |
. . . . . . . . 9
⊢
(Unit‘𝑅)
∈ V |
20 | 2, 19 | eqeltri 2697 |
. . . . . . . 8
⊢ 𝑈 ∈ V |
21 | | eqid 2622 |
. . . . . . . . . 10
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
22 | 21, 6 | mgpplusg 18493 |
. . . . . . . . 9
⊢ · =
(+g‘(mulGrp‘𝑅)) |
23 | 14, 22 | ressplusg 15993 |
. . . . . . . 8
⊢ (𝑈 ∈ V → · =
(+g‘((mulGrp‘𝑅) ↾s 𝑈))) |
24 | 20, 23 | ax-mp 5 |
. . . . . . 7
⊢ · =
(+g‘((mulGrp‘𝑅) ↾s 𝑈)) |
25 | 2, 14, 9 | invrfval 18673 |
. . . . . . 7
⊢
(invr‘𝑅) =
(invg‘((mulGrp‘𝑅) ↾s 𝑈)) |
26 | 18, 24, 25 | grpinvadd 17493 |
. . . . . 6
⊢
((((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp ∧ 𝑌 ∈
𝑈 ∧ 𝑍 ∈ 𝑈) → ((invr‘𝑅)‘(𝑌 · 𝑍)) = (((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌))) |
27 | 26 | oveq2d 6666 |
. . . . 5
⊢
((((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp ∧ 𝑌 ∈
𝑈 ∧ 𝑍 ∈ 𝑈) → (𝑍 ·
((invr‘𝑅)‘(𝑌 · 𝑍))) = (𝑍 ·
(((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌)))) |
28 | 16, 17, 4, 27 | syl3anc 1326 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑍 ·
((invr‘𝑅)‘(𝑌 · 𝑍))) = (𝑍 ·
(((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌)))) |
29 | | eqid 2622 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
30 | 2, 9, 6, 29 | unitrinv 18678 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈) → (𝑍 ·
((invr‘𝑅)‘𝑍)) = (1r‘𝑅)) |
31 | 30 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈) → ((𝑍 ·
((invr‘𝑅)‘𝑍)) ·
((invr‘𝑅)‘𝑌)) = ((1r‘𝑅) ·
((invr‘𝑅)‘𝑌))) |
32 | 31 | 3ad2antr3 1228 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑍 ·
((invr‘𝑅)‘𝑍)) ·
((invr‘𝑅)‘𝑌)) = ((1r‘𝑅) ·
((invr‘𝑅)‘𝑌))) |
33 | 2, 9 | unitinvcl 18674 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈) → ((invr‘𝑅)‘𝑍) ∈ 𝑈) |
34 | 33 | 3ad2antr3 1228 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((invr‘𝑅)‘𝑍) ∈ 𝑈) |
35 | 3, 34 | sseldi 3601 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((invr‘𝑅)‘𝑍) ∈ 𝐵) |
36 | 2, 9 | unitinvcl 18674 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈) → ((invr‘𝑅)‘𝑌) ∈ 𝑈) |
37 | 36 | 3ad2antr2 1227 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((invr‘𝑅)‘𝑌) ∈ 𝑈) |
38 | 3, 37 | sseldi 3601 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((invr‘𝑅)‘𝑌) ∈ 𝐵) |
39 | 1, 6 | ringass 18564 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑍 ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑍) ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑌) ∈ 𝐵)) → ((𝑍 ·
((invr‘𝑅)‘𝑍)) ·
((invr‘𝑅)‘𝑌)) = (𝑍 ·
(((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌)))) |
40 | 13, 5, 35, 38, 39 | syl13anc 1328 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑍 ·
((invr‘𝑅)‘𝑍)) ·
((invr‘𝑅)‘𝑌)) = (𝑍 ·
(((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌)))) |
41 | 1, 6, 29 | ringlidm 18571 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘𝑌) ∈ 𝐵) → ((1r‘𝑅) ·
((invr‘𝑅)‘𝑌)) = ((invr‘𝑅)‘𝑌)) |
42 | 13, 38, 41 | syl2anc 693 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((1r‘𝑅) ·
((invr‘𝑅)‘𝑌)) = ((invr‘𝑅)‘𝑌)) |
43 | 32, 40, 42 | 3eqtr3d 2664 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑍 ·
(((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌))) = ((invr‘𝑅)‘𝑌)) |
44 | 12, 28, 43 | 3eqtrd 2660 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑍 / (𝑌 · 𝑍)) = ((invr‘𝑅)‘𝑌)) |
45 | 44 | oveq2d 6666 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑋 · (𝑍 / (𝑌 · 𝑍))) = (𝑋 ·
((invr‘𝑅)‘𝑌))) |
46 | | simpr1 1067 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → 𝑋 ∈ 𝐵) |
47 | 1, 2, 10, 6 | dvrass 18690 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ (𝑌 · 𝑍) ∈ 𝑈)) → ((𝑋 · 𝑍) / (𝑌 · 𝑍)) = (𝑋 · (𝑍 / (𝑌 · 𝑍)))) |
48 | 13, 46, 5, 8, 47 | syl13anc 1328 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑍) / (𝑌 · 𝑍)) = (𝑋 · (𝑍 / (𝑌 · 𝑍)))) |
49 | 1, 6, 2, 9, 10 | dvrval 18685 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋 ·
((invr‘𝑅)‘𝑌))) |
50 | 46, 17, 49 | syl2anc 693 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑋 / 𝑌) = (𝑋 ·
((invr‘𝑅)‘𝑌))) |
51 | 45, 48, 50 | 3eqtr4d 2666 |
1
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑍) / (𝑌 · 𝑍)) = (𝑋 / 𝑌)) |