Theorem fracval

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

	Ref	Expression
Assertion	fracval	$$⊢\mathrm{Frac}\left(R\right)=R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-frac	$$⊢\mathrm{Frac}=\left(r\in \mathrm{V}⟼r\mathrm{RLocal}\mathrm{RLReg}\left(r\right)\right)$$
2		id	$$⊢r=R\to r=R$$
3		fveq2	$$⊢r=R\to \mathrm{RLReg}\left(r\right)=\mathrm{RLReg}\left(R\right)$$
4	2 3	oveq12d	$$⊢r=R\to r\mathrm{RLocal}\mathrm{RLReg}\left(r\right)=R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)$$
5	4	adantl	$$⊢\left(R\in \mathrm{V}\wedge r=R\right)\to r\mathrm{RLocal}\mathrm{RLReg}\left(r\right)=R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)$$
6		id	$$⊢R\in \mathrm{V}\to R\in \mathrm{V}$$
7		ovexd	$$⊢R\in \mathrm{V}\to R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)\in \mathrm{V}$$
8	1 5 6 7	fvmptd2	$$⊢R\in \mathrm{V}\to \mathrm{Frac}\left(R\right)=R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)$$
9		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{Frac}\left(R\right)=\varnothing$$
10		reldmrloc	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{RLocal}$$
11	10	ovprc1	$$⊢\neg R\in \mathrm{V}\to R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)=\varnothing$$
12	9 11	eqtr4d	$$⊢\neg R\in \mathrm{V}\to \mathrm{Frac}\left(R\right)=R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)$$
13	8 12	pm2.61i	$$⊢\mathrm{Frac}\left(R\right)=R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)$$