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	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝐺 = ( ∅ ↾s 𝑈 ) )
23		ress0	⊢ ( ∅ ↾s 𝑈 ) = ∅
24	22 23	syl6eq	⊢ ( ¬ 𝑅 ∈ 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 ‘ 𝐺 )