Metamath Proof Explorer

Definition df-frac

Description: Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025)

Ref Expression
Assertion df-frac 
|- Frac = ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrac 
 |-  Frac
1 vr 
 |-  r
2 cvv 
 |-  _V
3 1 cv 
 |-  r
4 crloc 
 |-  RLocal
5 crlreg 
 |-  RLReg
6 3 5 cfv 
 |-  ( RLReg ` r )
7 3 6 4 co 
 |-  ( r RLocal ( RLReg ` r ) )
8 1 2 7 cmpt 
 |-  ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) )
9 0 8 wceq 
 |-  Frac = ( r e. _V |-> ( r RLocal ( RLReg ` r ) ) )