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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	fracf1.2	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	fracf1.3	⊢ 1 = ( 1r ‘ 𝑅 )
	fracf1.4	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	fracf1.5	⊢ ∼ = ( 𝑅 ~RL 𝐸 )
	fracf1.6	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ ⟨ 𝑥 , 1 ⟩ ] ∼ )
Assertion	fracf1	⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1→ ( ( 𝐵 × 𝐸 ) / ∼ ) ∧ 𝐹 ∈ ( 𝑅 RingHom ( Frac ‘ 𝑅 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fracf1.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		fracf1.2	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
3		fracf1.3	⊢ 1 = ( 1r ‘ 𝑅 )
4		fracf1.4	⊢ ( 𝜑 → 𝑅 ∈ CRing )
5		fracf1.5	⊢ ∼ = ( 𝑅 ~RL 𝐸 )
6		fracf1.6	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ ⟨ 𝑥 , 1 ⟩ ] ∼ )
7		fracval	⊢ ( Frac ‘ 𝑅 ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) )
8	2	oveq2i	⊢ ( 𝑅 RLocal 𝐸 ) = ( 𝑅 RLocal ( RLReg ‘ 𝑅 ) )
9	7 8	eqtr4i	⊢ ( Frac ‘ 𝑅 ) = ( 𝑅 RLocal 𝐸 )
10		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
11	4	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
12	2 10 11	rrgsubm	⊢ ( 𝜑 → 𝐸 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
13		ssidd	⊢ ( 𝜑 → 𝐸 ⊆ 𝐸 )
14	13 2	sseqtrdi	⊢ ( 𝜑 → 𝐸 ⊆ ( RLReg ‘ 𝑅 ) )
15	1 3 9 5 6 4 12 14	rlocf1	⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1→ ( ( 𝐵 × 𝐸 ) / ∼ ) ∧ 𝐹 ∈ ( 𝑅 RingHom ( Frac ‘ 𝑅 ) ) ) )