Proof of Theorem dvrcan5
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dvrcan5.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑅) | 
| 2 |  | dvrcan5.o | . . . . . . 7
⊢ 𝑈 = (Unit‘𝑅) | 
| 3 | 1, 2 | unitss 20377 | . . . . . 6
⊢ 𝑈 ⊆ 𝐵 | 
| 4 |  | simpr3 1196 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → 𝑍 ∈ 𝑈) | 
| 5 | 3, 4 | sselid 3980 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → 𝑍 ∈ 𝐵) | 
| 6 |  | dvrcan5.t | . . . . . . 7
⊢  · =
(.r‘𝑅) | 
| 7 | 2, 6 | unitmulcl 20381 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈) → (𝑌 · 𝑍) ∈ 𝑈) | 
| 8 | 7 | 3adant3r1 1182 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑌 · 𝑍) ∈ 𝑈) | 
| 9 |  | eqid 2736 | . . . . . 6
⊢
(invr‘𝑅) = (invr‘𝑅) | 
| 10 |  | dvrcan5.d | . . . . . 6
⊢  / =
(/r‘𝑅) | 
| 11 | 1, 6, 2, 9, 10 | dvrval 20404 | . . . . 5
⊢ ((𝑍 ∈ 𝐵 ∧ (𝑌 · 𝑍) ∈ 𝑈) → (𝑍 / (𝑌 · 𝑍)) = (𝑍 ·
((invr‘𝑅)‘(𝑌 · 𝑍)))) | 
| 12 | 5, 8, 11 | syl2anc 584 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑍 / (𝑌 · 𝑍)) = (𝑍 ·
((invr‘𝑅)‘(𝑌 · 𝑍)))) | 
| 13 |  | simpl 482 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → 𝑅 ∈ Ring) | 
| 14 |  | eqid 2736 | . . . . . . 7
⊢
((mulGrp‘𝑅)
↾s 𝑈) =
((mulGrp‘𝑅)
↾s 𝑈) | 
| 15 | 2, 14 | unitgrp 20384 | . . . . . 6
⊢ (𝑅 ∈ Ring →
((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp) | 
| 16 | 13, 15 | syl 17 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((mulGrp‘𝑅) ↾s 𝑈) ∈ Grp) | 
| 17 |  | simpr2 1195 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → 𝑌 ∈ 𝑈) | 
| 18 | 2, 14 | unitgrpbas 20383 | . . . . . . 7
⊢ 𝑈 =
(Base‘((mulGrp‘𝑅) ↾s 𝑈)) | 
| 19 | 2 | fvexi 6919 | . . . . . . . 8
⊢ 𝑈 ∈ V | 
| 20 |  | eqid 2736 | . . . . . . . . . 10
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) | 
| 21 | 20, 6 | mgpplusg 20142 | . . . . . . . . 9
⊢  · =
(+g‘(mulGrp‘𝑅)) | 
| 22 | 14, 21 | ressplusg 17335 | . . . . . . . 8
⊢ (𝑈 ∈ V → · =
(+g‘((mulGrp‘𝑅) ↾s 𝑈))) | 
| 23 | 19, 22 | ax-mp 5 | . . . . . . 7
⊢  · =
(+g‘((mulGrp‘𝑅) ↾s 𝑈)) | 
| 24 | 2, 14, 9 | invrfval 20390 | . . . . . . 7
⊢
(invr‘𝑅) =
(invg‘((mulGrp‘𝑅) ↾s 𝑈)) | 
| 25 | 18, 23, 24 | grpinvadd 19037 | . . . . . 6
⊢
((((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp ∧ 𝑌 ∈
𝑈 ∧ 𝑍 ∈ 𝑈) → ((invr‘𝑅)‘(𝑌 · 𝑍)) = (((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌))) | 
| 26 | 25 | oveq2d 7448 | . . . . 5
⊢
((((mulGrp‘𝑅)
↾s 𝑈)
∈ Grp ∧ 𝑌 ∈
𝑈 ∧ 𝑍 ∈ 𝑈) → (𝑍 ·
((invr‘𝑅)‘(𝑌 · 𝑍))) = (𝑍 ·
(((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌)))) | 
| 27 | 16, 17, 4, 26 | syl3anc 1372 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑍 ·
((invr‘𝑅)‘(𝑌 · 𝑍))) = (𝑍 ·
(((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌)))) | 
| 28 |  | eqid 2736 | . . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 29 | 2, 9, 6, 28 | unitrinv 20395 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈) → (𝑍 ·
((invr‘𝑅)‘𝑍)) = (1r‘𝑅)) | 
| 30 | 29 | oveq1d 7447 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈) → ((𝑍 ·
((invr‘𝑅)‘𝑍)) ·
((invr‘𝑅)‘𝑌)) = ((1r‘𝑅) ·
((invr‘𝑅)‘𝑌))) | 
| 31 | 30 | 3ad2antr3 1190 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑍 ·
((invr‘𝑅)‘𝑍)) ·
((invr‘𝑅)‘𝑌)) = ((1r‘𝑅) ·
((invr‘𝑅)‘𝑌))) | 
| 32 | 2, 9 | unitinvcl 20391 | . . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈) → ((invr‘𝑅)‘𝑍) ∈ 𝑈) | 
| 33 | 32 | 3ad2antr3 1190 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((invr‘𝑅)‘𝑍) ∈ 𝑈) | 
| 34 | 3, 33 | sselid 3980 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((invr‘𝑅)‘𝑍) ∈ 𝐵) | 
| 35 | 2, 9 | unitinvcl 20391 | . . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈) → ((invr‘𝑅)‘𝑌) ∈ 𝑈) | 
| 36 | 35 | 3ad2antr2 1189 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((invr‘𝑅)‘𝑌) ∈ 𝑈) | 
| 37 | 3, 36 | sselid 3980 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((invr‘𝑅)‘𝑌) ∈ 𝐵) | 
| 38 | 1, 6 | ringass 20251 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑍 ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑍) ∈ 𝐵 ∧ ((invr‘𝑅)‘𝑌) ∈ 𝐵)) → ((𝑍 ·
((invr‘𝑅)‘𝑍)) ·
((invr‘𝑅)‘𝑌)) = (𝑍 ·
(((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌)))) | 
| 39 | 13, 5, 34, 37, 38 | syl13anc 1373 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑍 ·
((invr‘𝑅)‘𝑍)) ·
((invr‘𝑅)‘𝑌)) = (𝑍 ·
(((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌)))) | 
| 40 | 1, 6, 28 | ringlidm 20267 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘𝑌) ∈ 𝐵) → ((1r‘𝑅) ·
((invr‘𝑅)‘𝑌)) = ((invr‘𝑅)‘𝑌)) | 
| 41 | 13, 37, 40 | syl2anc 584 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((1r‘𝑅) ·
((invr‘𝑅)‘𝑌)) = ((invr‘𝑅)‘𝑌)) | 
| 42 | 31, 39, 41 | 3eqtr3d 2784 | . . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑍 ·
(((invr‘𝑅)‘𝑍) ·
((invr‘𝑅)‘𝑌))) = ((invr‘𝑅)‘𝑌)) | 
| 43 | 12, 27, 42 | 3eqtrd 2780 | . . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑍 / (𝑌 · 𝑍)) = ((invr‘𝑅)‘𝑌)) | 
| 44 | 43 | oveq2d 7448 | . 2
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑋 · (𝑍 / (𝑌 · 𝑍))) = (𝑋 ·
((invr‘𝑅)‘𝑌))) | 
| 45 |  | simpr1 1194 | . . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → 𝑋 ∈ 𝐵) | 
| 46 | 1, 2, 10, 6 | dvrass 20409 | . . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ (𝑌 · 𝑍) ∈ 𝑈)) → ((𝑋 · 𝑍) / (𝑌 · 𝑍)) = (𝑋 · (𝑍 / (𝑌 · 𝑍)))) | 
| 47 | 13, 45, 5, 8, 46 | syl13anc 1373 | . 2
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑍) / (𝑌 · 𝑍)) = (𝑋 · (𝑍 / (𝑌 · 𝑍)))) | 
| 48 | 1, 6, 2, 9, 10 | dvrval 20404 | . . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈) → (𝑋 / 𝑌) = (𝑋 ·
((invr‘𝑅)‘𝑌))) | 
| 49 | 45, 17, 48 | syl2anc 584 | . 2
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → (𝑋 / 𝑌) = (𝑋 ·
((invr‘𝑅)‘𝑌))) | 
| 50 | 44, 47, 49 | 3eqtr4d 2786 | 1
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈)) → ((𝑋 · 𝑍) / (𝑌 · 𝑍)) = (𝑋 / 𝑌)) |