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 = ( Unit ` R )
invrfval.g 
|- G = ( ( mulGrp ` R ) |`s U )
invrfval.i 
|- I = ( invr ` R )
Assertion invrfval 
|- I = ( invg ` G )

Proof

Step Hyp Ref Expression
1 invrfval.u 
 |-  U = ( Unit ` R )
2 invrfval.g 
 |-  G = ( ( mulGrp ` R ) |`s U )
3 invrfval.i 
 |-  I = ( invr ` R )
4 fveq2 
 |-  ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
5 fveq2 
 |-  ( r = R -> ( Unit ` r ) = ( Unit ` R ) )
6 5 1 eqtr4di 
 |-  ( r = R -> ( Unit ` r ) = U )
7 4 6 oveq12d 
 |-  ( r = R -> ( ( mulGrp ` r ) |`s ( Unit ` r ) ) = ( ( mulGrp ` R ) |`s U ) )
8 7 2 eqtr4di 
 |-  ( r = R -> ( ( mulGrp ` r ) |`s ( Unit ` r ) ) = G )
9 8 fveq2d 
 |-  ( r = R -> ( invg ` ( ( mulGrp ` r ) |`s ( Unit ` r ) ) ) = ( invg ` G ) )
10 df-invr 
 |-  invr = ( r e. _V |-> ( invg ` ( ( mulGrp ` r ) |`s ( Unit ` r ) ) ) )
11 fvex 
 |-  ( invg ` G ) e. _V
12 9 10 11 fvmpt 
 |-  ( R e. _V -> ( invr ` R ) = ( invg ` G ) )
13 fvprc 
 |-  ( -. R e. _V -> ( invr ` R ) = (/) )
14 base0 
 |-  (/) = ( Base ` (/) )
15 eqid 
 |-  ( invg ` (/) ) = ( invg ` (/) )
16 14 15 grpinvfn 
 |-  ( invg ` (/) ) Fn (/)
17 fn0 
 |-  ( ( invg ` (/) ) Fn (/) <-> ( invg ` (/) ) = (/) )
18 16 17 mpbi 
 |-  ( invg ` (/) ) = (/)
19 13 18 eqtr4di 
 |-  ( -. R e. _V -> ( invr ` R ) = ( invg ` (/) ) )
20 fvprc 
 |-  ( -. R e. _V -> ( mulGrp ` R ) = (/) )
21 20 oveq1d 
 |-  ( -. R e. _V -> ( ( mulGrp ` R ) |`s U ) = ( (/) |`s U ) )
22 2 21 eqtrid 
 |-  ( -. R e. _V -> G = ( (/) |`s U ) )
23 ress0 
 |-  ( (/) |`s U ) = (/)
24 22 23 eqtrdi 
 |-  ( -. R e. _V -> G = (/) )
25 24 fveq2d 
 |-  ( -. R e. _V -> ( invg ` G ) = ( invg ` (/) ) )
26 19 25 eqtr4d 
 |-  ( -. R e. _V -> ( invr ` R ) = ( invg ` G ) )
27 12 26 pm2.61i 
 |-  ( invr ` R ) = ( invg ` G )
28 3 27 eqtri 
 |-  I = ( invg ` G )