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 𝑈 = ( Unit ‘ 𝑅 )
invrfval.g 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
invrfval.i 𝐼 = ( invr𝑅 )
Assertion invrfval 𝐼 = ( invg𝐺 )

Proof

Step Hyp Ref Expression
1 invrfval.u 𝑈 = ( Unit ‘ 𝑅 )
2 invrfval.g 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
3 invrfval.i 𝐼 = ( invr𝑅 )
4 fveq2 ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
5 fveq2 ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) )
6 5 1 eqtr4di ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = 𝑈 )
7 4 6 oveq12d ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
8 7 2 eqtr4di ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) = 𝐺 )
9 8 fveq2d ( 𝑟 = 𝑅 → ( invg ‘ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ) = ( invg𝐺 ) )
10 df-invr invr = ( 𝑟 ∈ V ↦ ( invg ‘ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ) )
11 fvex ( invg𝐺 ) ∈ V
12 9 10 11 fvmpt ( 𝑅 ∈ V → ( invr𝑅 ) = ( invg𝐺 ) )
13 fvprc ( ¬ 𝑅 ∈ V → ( invr𝑅 ) = ∅ )
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 ( ¬ 𝑅 ∈ V → ( invr𝑅 ) = ( invg ‘ ∅ ) )
20 fvprc ( ¬ 𝑅 ∈ V → ( mulGrp ‘ 𝑅 ) = ∅ )
21 20 oveq1d ( ¬ 𝑅 ∈ V → ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) = ( ∅ ↾s 𝑈 ) )
22 2 21 eqtrid ( ¬ 𝑅 ∈ V → 𝐺 = ( ∅ ↾s 𝑈 ) )
23 ress0 ( ∅ ↾s 𝑈 ) = ∅
24 22 23 eqtrdi ( ¬ 𝑅 ∈ V → 𝐺 = ∅ )
25 24 fveq2d ( ¬ 𝑅 ∈ V → ( invg𝐺 ) = ( invg ‘ ∅ ) )
26 19 25 eqtr4d ( ¬ 𝑅 ∈ V → ( invr𝑅 ) = ( invg𝐺 ) )
27 12 26 pm2.61i ( invr𝑅 ) = ( invg𝐺 )
28 3 27 eqtri 𝐼 = ( invg𝐺 )