Theorem fracval

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

	Ref	Expression
Assertion	fracval	Could not format assertion : No typesetting found for |- ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-frac	Could not format Frac = ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) ) : No typesetting found for |- Frac = ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) ) with typecode |-
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	Could not format ( r = R -> ( r RLocal ( RLReg ` r ) ) = ( R RLocal ( RLReg ` R ) ) ) : No typesetting found for |- ( r = R -> ( r RLocal ( RLReg ` r ) ) = ( R RLocal ( RLReg ` R ) ) ) with typecode |-
5	4	adantl	Could not format ( ( R e. _V /\ r = R ) -> ( r RLocal ( RLReg ` r ) ) = ( R RLocal ( RLReg ` R ) ) ) : No typesetting found for |- ( ( R e. _V /\ r = R ) -> ( r RLocal ( RLReg ` r ) ) = ( R RLocal ( RLReg ` R ) ) ) with typecode |-
6		id	$$⊢R\in \mathrm{V}\to R\in \mathrm{V}$$
7		ovexd	Could not format ( R e. _V -> ( R RLocal ( RLReg ` R ) ) e. _V ) : No typesetting found for |- ( R e. _V -> ( R RLocal ( RLReg ` R ) ) e. _V ) with typecode |-
8	1 5 6 7	fvmptd2	Could not format ( R e. _V -> ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) ) : No typesetting found for |- ( R e. _V -> ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) ) with typecode |-
9		fvprc	Could not format ( -. R e. _V -> ( Frac ` R ) = (/) ) : No typesetting found for |- ( -. R e. _V -> ( Frac ` R ) = (/) ) with typecode |-
10		reldmrloc	Could not format Rel dom RLocal : No typesetting found for |- Rel dom RLocal with typecode |-
11	10	ovprc1	Could not format ( -. R e. _V -> ( R RLocal ( RLReg ` R ) ) = (/) ) : No typesetting found for |- ( -. R e. _V -> ( R RLocal ( RLReg ` R ) ) = (/) ) with typecode |-
12	9 11	eqtr4d	Could not format ( -. R e. _V -> ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) ) : No typesetting found for |- ( -. R e. _V -> ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) ) with typecode |-
13	8 12	pm2.61i	Could not format ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) : No typesetting found for |- ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) with typecode |-