Metamath Proof Explorer

Theorem fracval

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

Ref Expression
Assertion fracval 
|- ( Frac ` R ) = ( R RLocal ( RLReg ` R ) )

Proof

Step Hyp Ref Expression
1 df-frac 
 |-  Frac = ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) )
2 id 
 |-  ( r = R -> r = R )
3 fveq2 
 |-  ( r = R -> ( RLReg ` r ) = ( RLReg ` R ) )
4 2 3 oveq12d 
 |-  ( r = R -> ( r RLocal ( RLReg ` r ) ) = ( R RLocal ( RLReg ` R ) ) )
5 4 adantl 
 |-  ( ( R e. _V /\ r = R ) -> ( r RLocal ( RLReg ` r ) ) = ( R RLocal ( RLReg ` R ) ) )
6 id 
 |-  ( R e. _V -> R e. _V )
7 ovexd 
 |-  ( R e. _V -> ( R RLocal ( RLReg ` R ) ) e. _V )
8 1 5 6 7 fvmptd2 
 |-  ( R e. _V -> ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) )
9 fvprc 
 |-  ( -. R e. _V -> ( Frac ` R ) = (/) )
10 reldmrloc 
 |-  Rel dom RLocal
11 10 ovprc1 
 |-  ( -. R e. _V -> ( R RLocal ( RLReg ` R ) ) = (/) )
12 9 11 eqtr4d 
 |-  ( -. R e. _V -> ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) )
13 8 12 pm2.61i 
 |-  ( Frac ` R ) = ( R RLocal ( RLReg ` R ) )