![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > invrfval | Structured version Visualization version GIF version |
Description: Multiplicative inverse function for a division ring. (Contributed by NM, 21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.) |
Ref | Expression |
---|---|
invrfval.u | ⊢ 𝑈 = (Unit‘𝑅) |
invrfval.g | ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) |
invrfval.i | ⊢ 𝐼 = (invr‘𝑅) |
Ref | Expression |
---|---|
invrfval | ⊢ 𝐼 = (invg‘𝐺) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | invrfval.i | . 2 ⊢ 𝐼 = (invr‘𝑅) | |
2 | fveq2 6496 | . . . . . . 7 ⊢ (𝑟 = 𝑅 → (mulGrp‘𝑟) = (mulGrp‘𝑅)) | |
3 | fveq2 6496 | . . . . . . . 8 ⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅)) | |
4 | invrfval.u | . . . . . . . 8 ⊢ 𝑈 = (Unit‘𝑅) | |
5 | 3, 4 | syl6eqr 2825 | . . . . . . 7 ⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈) |
6 | 2, 5 | oveq12d 6992 | . . . . . 6 ⊢ (𝑟 = 𝑅 → ((mulGrp‘𝑟) ↾s (Unit‘𝑟)) = ((mulGrp‘𝑅) ↾s 𝑈)) |
7 | invrfval.g | . . . . . 6 ⊢ 𝐺 = ((mulGrp‘𝑅) ↾s 𝑈) | |
8 | 6, 7 | syl6eqr 2825 | . . . . 5 ⊢ (𝑟 = 𝑅 → ((mulGrp‘𝑟) ↾s (Unit‘𝑟)) = 𝐺) |
9 | 8 | fveq2d 6500 | . . . 4 ⊢ (𝑟 = 𝑅 → (invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟))) = (invg‘𝐺)) |
10 | df-invr 19157 | . . . 4 ⊢ invr = (𝑟 ∈ V ↦ (invg‘((mulGrp‘𝑟) ↾s (Unit‘𝑟)))) | |
11 | fvex 6509 | . . . 4 ⊢ (invg‘𝐺) ∈ V | |
12 | 9, 10, 11 | fvmpt 6593 | . . 3 ⊢ (𝑅 ∈ V → (invr‘𝑅) = (invg‘𝐺)) |
13 | fvprc 6489 | . . . . 5 ⊢ (¬ 𝑅 ∈ V → (invr‘𝑅) = ∅) | |
14 | base0 16390 | . . . . . . 7 ⊢ ∅ = (Base‘∅) | |
15 | eqid 2771 | . . . . . . 7 ⊢ (invg‘∅) = (invg‘∅) | |
16 | 14, 15 | grpinvfn 17944 | . . . . . 6 ⊢ (invg‘∅) Fn ∅ |
17 | fn0 6306 | . . . . . 6 ⊢ ((invg‘∅) Fn ∅ ↔ (invg‘∅) = ∅) | |
18 | 16, 17 | mpbi 222 | . . . . 5 ⊢ (invg‘∅) = ∅ |
19 | 13, 18 | syl6eqr 2825 | . . . 4 ⊢ (¬ 𝑅 ∈ V → (invr‘𝑅) = (invg‘∅)) |
20 | fvprc 6489 | . . . . . . . 8 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅) | |
21 | 20 | oveq1d 6989 | . . . . . . 7 ⊢ (¬ 𝑅 ∈ V → ((mulGrp‘𝑅) ↾s 𝑈) = (∅ ↾s 𝑈)) |
22 | 7, 21 | syl5eq 2819 | . . . . . 6 ⊢ (¬ 𝑅 ∈ V → 𝐺 = (∅ ↾s 𝑈)) |
23 | ress0 16412 | . . . . . 6 ⊢ (∅ ↾s 𝑈) = ∅ | |
24 | 22, 23 | syl6eq 2823 | . . . . 5 ⊢ (¬ 𝑅 ∈ V → 𝐺 = ∅) |
25 | 24 | fveq2d 6500 | . . . 4 ⊢ (¬ 𝑅 ∈ V → (invg‘𝐺) = (invg‘∅)) |
26 | 19, 25 | eqtr4d 2810 | . . 3 ⊢ (¬ 𝑅 ∈ V → (invr‘𝑅) = (invg‘𝐺)) |
27 | 12, 26 | pm2.61i 177 | . 2 ⊢ (invr‘𝑅) = (invg‘𝐺) |
28 | 1, 27 | eqtri 2795 | 1 ⊢ 𝐼 = (invg‘𝐺) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1508 ∈ wcel 2051 Vcvv 3408 ∅c0 4172 Fn wfn 6180 ‘cfv 6185 (class class class)co 6974 ↾s cress 16338 invgcminusg 17904 mulGrpcmgp 18974 Unitcui 19124 invrcinvr 19156 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-ral 3086 df-rex 3087 df-reu 3088 df-rab 3090 df-v 3410 df-sbc 3675 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-fv 6193 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-slot 16341 df-base 16343 df-ress 16345 df-minusg 17907 df-invr 19157 |
This theorem is referenced by: unitinvcl 19159 unitinvinv 19160 unitlinv 19162 unitrinv 19163 invrpropd 19183 subrgugrp 19289 cntzsdrg 19315 cnmsubglem 20325 psgninv 20443 invrvald 21004 invrcn2 22506 nrginvrcn 23019 nrgtdrg 23020 sum2dchr 25567 rdivmuldivd 30573 ringinvval 30574 dvrcan5 30575 |
Copyright terms: Public domain | W3C validator |