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	No typesetting found for |- .~ = ( R ~RL E ) with typecode |-
	fracf1.6	$$⊢F=\left(x\in B⟼\left[⟨x,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\right)$$
Assertion	fracf1	Could not format assertion : No typesetting found for |- ( ph -> ( F : B -1-1-> ( ( B X. E ) /. .~ ) /\ F e. ( R RingHom ( Frac ` R ) ) ) ) with typecode |-

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	Could not format .~ = ( R ~RL E ) : No typesetting found for |- .~ = ( R ~RL E ) with typecode |-
6		fracf1.6	$$⊢F=\left(x\in B⟼\left[⟨x,\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\right)$$
7		fracval	Could not format ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) : No typesetting found for |- ( Frac ` R ) = ( R RLocal ( RLReg ` R ) ) with typecode |-
8	2	oveq2i	Could not format ( R RLocal E ) = ( R RLocal ( RLReg ` R ) ) : No typesetting found for |- ( R RLocal E ) = ( R RLocal ( RLReg ` R ) ) with typecode |-
9	7 8	eqtr4i	Could not format ( Frac ` R ) = ( R RLocal E ) : No typesetting found for |- ( Frac ` R ) = ( R RLocal E ) with typecode |-
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	Could not format ( ph -> ( F : B -1-1-> ( ( B X. E ) /. .~ ) /\ F e. ( R RingHom ( Frac ` R ) ) ) ) : No typesetting found for |- ( ph -> ( F : B -1-1-> ( ( B X. E ) /. .~ ) /\ F e. ( R RingHom ( Frac ` R ) ) ) ) with typecode |-