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 = ( Base ` R )
	fracf1.2	|- E = ( RLReg ` R )
	fracf1.3	|- .1. = ( 1r ` R )
	fracf1.4	|- ( ph -> R e. CRing )
	fracf1.5	|- .~ = ( R ~RL E )
	fracf1.6	|- F = ( x e. B |-> [ <. x , .1. >. ] .~ )
Assertion	fracf1	|- ( ph -> ( F : B -1-1-> ( ( B X. E ) /. .~ ) /\ F e. ( R RingHom ( Frac ` R ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fracf1.1	|- B = ( Base ` R )
2		fracf1.2	|- E = ( RLReg ` R )
3		fracf1.3	|- .1. = ( 1r ` R )
4		fracf1.4	|- ( ph -> R e. CRing )
5		fracf1.5	|- .~ = ( R ~RL E )
6		fracf1.6	|- F = ( x e. B |-> [ <. x , .1. >. ] .~ )
7		fracval	|- ( Frac ` R ) = ( R RLocal ( RLReg ` R ) )
8	2	oveq2i	|- ( R RLocal E ) = ( R RLocal ( RLReg ` R ) )
9	7 8	eqtr4i	|- ( Frac ` R ) = ( R RLocal E )
10		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
11	4	crngringd	|- ( ph -> R e. Ring )
12	2 10 11	rrgsubm	|- ( ph -> E e. ( SubMnd ` ( mulGrp ` R ) ) )
13		ssidd	|- ( ph -> E C_ E )
14	13 2	sseqtrdi	|- ( ph -> E C_ ( RLReg ` R ) )
15	1 3 9 5 6 4 12 14	rlocf1	|- ( ph -> ( F : B -1-1-> ( ( B X. E ) /. .~ ) /\ F e. ( R RingHom ( Frac ` R ) ) ) )