Theorem fracf1

Description: The embedding of a commutative ring R into its field of fractions. (Contributed by Thierry Arnoux, 10-May-2025)

	Ref	Expression
Hypotheses	fracf1.1	$$⊢B={\mathrm{Base}}_R$$
	fracf1.2	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	fracf1.3	$$⊢\underset{\dot{}}{1}=1_R$$
	fracf1.4	$$⊢\phi \to R\in \mathrm{CRing}$$
	fracf1.5	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathrm{RL}}E$$
	fracf1.6	$$⊢F=\left(x\in B⟼\left[⟨x,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\right)$$
Assertion	fracf1	$$⊢\phi \to \left(F:B\underset{1-1}{⟶}\left(B\times E\right)/\underset{\dot{}}{\sim }\wedge F\in \left(R\mathrm{RingHom}\mathrm{Frac}\left(R\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fracf1.1	$$⊢B={\mathrm{Base}}_R$$
2		fracf1.2	$$⊢E=\mathrm{RLReg}\left(R\right)$$
3		fracf1.3	$$⊢\underset{\dot{}}{1}=1_R$$
4		fracf1.4	$$⊢\phi \to R\in \mathrm{CRing}$$
5		fracf1.5	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathrm{RL}}E$$
6		fracf1.6	$$⊢F=\left(x\in B⟼\left[⟨x,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\right)$$
7		fracval	$$⊢\mathrm{Frac}\left(R\right)=R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)$$
8	2	oveq2i	$$⊢R\mathrm{RLocal}E=R\mathrm{RLocal}\mathrm{RLReg}\left(R\right)$$
9	7 8	eqtr4i	$$⊢\mathrm{Frac}\left(R\right)=R\mathrm{RLocal}E$$
10		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
11	4	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
12	2 10 11	rrgsubm	$$⊢\phi \to E\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
13		ssidd	$$⊢\phi \to E\subseteq E$$
14	13 2	sseqtrdi	$$⊢\phi \to E\subseteq \mathrm{RLReg}\left(R\right)$$
15	1 3 9 5 6 4 12 14	rlocf1	$$⊢\phi \to \left(F:B\underset{1-1}{⟶}\left(B\times E\right)/\underset{\dot{}}{\sim }\wedge F\in \left(R\mathrm{RingHom}\mathrm{Frac}\left(R\right)\right)\right)$$