This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐺 )