Theorem fracval

Description: Value of the field of fractions. (Contributed by Thierry Arnoux, 5-May-2025)

	Ref	Expression
Assertion	fracval	⊢ ( Frac ‘ 𝑅 ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		df-frac	⊢ Frac = ( 𝑟 ∈ V ↦ ( 𝑟 RLocal ( RLReg ‘ 𝑟 ) ) )
2		id	⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
3		fveq2	⊢ ( 𝑟 = 𝑅 → ( RLReg ‘ 𝑟 ) = ( RLReg ‘ 𝑅 ) )
4	2 3	oveq12d	⊢ ( 𝑟 = 𝑅 → ( 𝑟 RLocal ( RLReg ‘ 𝑟 ) ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) )
5	4	adantl	⊢ ( ( 𝑅 ∈ V ∧ 𝑟 = 𝑅 ) → ( 𝑟 RLocal ( RLReg ‘ 𝑟 ) ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) )
6		id	⊢ ( 𝑅 ∈ V → 𝑅 ∈ V )
7		ovexd	⊢ ( 𝑅 ∈ V → ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) ∈ V )
8	1 5 6 7	fvmptd2	⊢ ( 𝑅 ∈ V → ( Frac ‘ 𝑅 ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) )
9		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Frac ‘ 𝑅 ) = ∅ )
10		reldmrloc	⊢ Rel dom RLocal
11	10	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) = ∅ )
12	9 11	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( Frac ‘ 𝑅 ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) ) )
13	8 12	pm2.61i	⊢ ( Frac ‘ 𝑅 ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) )