# Metamath Proof Explorer

## Theorem invrfval

Description: Multiplicative inverse function for a division ring. (Contributed by NM, 21-Sep-2011) (Revised by Mario Carneiro, 25-Dec-2014)

Ref Expression
Hypotheses invrfval.u ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
invrfval.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}$
invrfval.i ${⊢}{I}={inv}_{r}\left({R}\right)$
Assertion invrfval ${⊢}{I}={inv}_{g}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 invrfval.u ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
2 invrfval.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}$
3 invrfval.i ${⊢}{I}={inv}_{r}\left({R}\right)$
4 fveq2 ${⊢}{r}={R}\to {\mathrm{mulGrp}}_{{r}}={\mathrm{mulGrp}}_{{R}}$
5 fveq2 ${⊢}{r}={R}\to \mathrm{Unit}\left({r}\right)=\mathrm{Unit}\left({R}\right)$
6 5 1 eqtr4di ${⊢}{r}={R}\to \mathrm{Unit}\left({r}\right)={U}$
7 4 6 oveq12d ${⊢}{r}={R}\to {\mathrm{mulGrp}}_{{r}}{↾}_{𝑠}\mathrm{Unit}\left({r}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}$
8 7 2 eqtr4di ${⊢}{r}={R}\to {\mathrm{mulGrp}}_{{r}}{↾}_{𝑠}\mathrm{Unit}\left({r}\right)={G}$
9 8 fveq2d ${⊢}{r}={R}\to {inv}_{g}\left({\mathrm{mulGrp}}_{{r}}{↾}_{𝑠}\mathrm{Unit}\left({r}\right)\right)={inv}_{g}\left({G}\right)$
10 df-invr ${⊢}{inv}_{r}=\left({r}\in \mathrm{V}⟼{inv}_{g}\left({\mathrm{mulGrp}}_{{r}}{↾}_{𝑠}\mathrm{Unit}\left({r}\right)\right)\right)$
11 fvex ${⊢}{inv}_{g}\left({G}\right)\in \mathrm{V}$
12 9 10 11 fvmpt ${⊢}{R}\in \mathrm{V}\to {inv}_{r}\left({R}\right)={inv}_{g}\left({G}\right)$
13 fvprc ${⊢}¬{R}\in \mathrm{V}\to {inv}_{r}\left({R}\right)=\varnothing$
14 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
15 eqid ${⊢}{inv}_{g}\left(\varnothing \right)={inv}_{g}\left(\varnothing \right)$
16 14 15 grpinvfn ${⊢}{inv}_{g}\left(\varnothing \right)Fn\varnothing$
17 fn0 ${⊢}{inv}_{g}\left(\varnothing \right)Fn\varnothing ↔{inv}_{g}\left(\varnothing \right)=\varnothing$
18 16 17 mpbi ${⊢}{inv}_{g}\left(\varnothing \right)=\varnothing$
19 13 18 eqtr4di ${⊢}¬{R}\in \mathrm{V}\to {inv}_{r}\left({R}\right)={inv}_{g}\left(\varnothing \right)$
20 fvprc ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{mulGrp}}_{{R}}=\varnothing$
21 20 oveq1d ${⊢}¬{R}\in \mathrm{V}\to {\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}=\varnothing {↾}_{𝑠}{U}$
22 2 21 syl5eq ${⊢}¬{R}\in \mathrm{V}\to {G}=\varnothing {↾}_{𝑠}{U}$
23 ress0 ${⊢}\varnothing {↾}_{𝑠}{U}=\varnothing$
24 22 23 eqtrdi ${⊢}¬{R}\in \mathrm{V}\to {G}=\varnothing$
25 24 fveq2d ${⊢}¬{R}\in \mathrm{V}\to {inv}_{g}\left({G}\right)={inv}_{g}\left(\varnothing \right)$
26 19 25 eqtr4d ${⊢}¬{R}\in \mathrm{V}\to {inv}_{r}\left({R}\right)={inv}_{g}\left({G}\right)$
27 12 26 pm2.61i ${⊢}{inv}_{r}\left({R}\right)={inv}_{g}\left({G}\right)$
28 3 27 eqtri ${⊢}{I}={inv}_{g}\left({G}\right)$