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 = ( 𝑟 ∈ V ↦ ( 𝑟 RLocal ( RLReg ‘ 𝑟 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfrac	⊢ Frac
1		vr	⊢ 𝑟
2		cvv	⊢ V
3	1	cv	⊢ 𝑟
4		crloc	⊢ RLocal
5		crlreg	⊢ RLReg
6	3 5	cfv	⊢ ( RLReg ‘ 𝑟 )
7	3 6 4	co	⊢ ( 𝑟 RLocal ( RLReg ‘ 𝑟 ) )
8	1 2 7	cmpt	⊢ ( 𝑟 ∈ V ↦ ( 𝑟 RLocal ( RLReg ‘ 𝑟 ) ) )
9	0 8	wceq	⊢ Frac = ( 𝑟 ∈ V ↦ ( 𝑟 RLocal ( RLReg ‘ 𝑟 ) ) )