Metamath Proof Explorer

Theorem idomsubr

Description: Every integral domain is isomorphic with a subring of some field. (Proposed by Gerard Lang, 10-May-2025.) (Contributed by Thierry Arnoux, 10-May-2025)

Ref Expression
Hypothesis idomsubr.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
Assertion idomsubr ( 𝜑 → ∃ 𝑓 ∈ Field ∃ 𝑠 ∈ ( SubRing ‘ 𝑓 ) 𝑅 ≃𝑟 ( 𝑓 ↾s 𝑠 ) )

Proof

Step Hyp Ref Expression
1 idomsubr.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
2 fveq2 ⊢ ( 𝑓 = ( Frac ‘ 𝑅 ) → ( SubRing ‘ 𝑓 ) = ( SubRing ‘ ( Frac ‘ 𝑅 ) ) )
3 oveq1 ⊢ ( 𝑓 = ( Frac ‘ 𝑅 ) → ( 𝑓 ↾s 𝑠 ) = ( ( Frac ‘ 𝑅 ) ↾s 𝑠 ) )
4 3 breq2d ⊢ ( 𝑓 = ( Frac ‘ 𝑅 ) → ( 𝑅 ≃𝑟 ( 𝑓 ↾s 𝑠 ) ↔ 𝑅 ≃𝑟 ( ( Frac ‘ 𝑅 ) ↾s 𝑠 ) ) )
5 2 4 rexeqbidv ⊢ ( 𝑓 = ( Frac ‘ 𝑅 ) → ( ∃ 𝑠 ∈ ( SubRing ‘ 𝑓 ) 𝑅 ≃𝑟 ( 𝑓 ↾s 𝑠 ) ↔ ∃ 𝑠 ∈ ( SubRing ‘ ( Frac ‘ 𝑅 ) ) 𝑅 ≃𝑟 ( ( Frac ‘ 𝑅 ) ↾s 𝑠 ) ) )
6 1 fracfld ⊢ ( 𝜑 → ( Frac ‘ 𝑅 ) ∈ Field )
7 oveq2 ⊢ ( 𝑠 = ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( ( Frac ‘ 𝑅 ) ↾s 𝑠 ) = ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) )
8 7 breq2d ⊢ ( 𝑠 = ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑅 ≃𝑟 ( ( Frac ‘ 𝑅 ) ↾s 𝑠 ) ↔ 𝑅 ≃𝑟 ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 eqid ⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
11 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
12 1 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
13 eqid ⊢ ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) )
14 opeq1 ⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ = ⟨ 𝑦 , ( 1r ‘ 𝑅 ) ⟩ )
15 14 eceq1d ⊢ ( 𝑥 = 𝑦 → [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) = [ ⟨ 𝑦 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) )
16 15 cbvmptv ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑦 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) )
17 9 10 11 12 13 16 fracf1 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) –1-1→ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingHom ( Frac ‘ 𝑅 ) ) ) )
18 rnrhmsubrg ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingHom ( Frac ‘ 𝑅 ) ) → ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( SubRing ‘ ( Frac ‘ 𝑅 ) ) )
19 17 18 simpl2im ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( SubRing ‘ ( Frac ‘ 𝑅 ) ) )
20 ssidd ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ⊆ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
21 17 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingHom ( Frac ‘ 𝑅 ) ) )
22 eqid ⊢ ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) = ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
23 22 resrhm2b ⊢ ( ( ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( SubRing ‘ ( Frac ‘ 𝑅 ) ) ∧ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ⊆ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingHom ( Frac ‘ 𝑅 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingHom ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) ) )
24 23 biimpa ⊢ ( ( ( ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( SubRing ‘ ( Frac ‘ 𝑅 ) ) ∧ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ⊆ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingHom ( Frac ‘ 𝑅 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingHom ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) )
25 19 20 21 24 syl21anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingHom ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) )
26 17 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) –1-1→ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
27 f1f1orn ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) –1-1→ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) –1-1-onto→ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
28 26 27 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) –1-1-onto→ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
29 f1f ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) –1-1→ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) ⟶ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
30 26 29 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) ⟶ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
31 30 frnd ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ⊆ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) )
32 eqid ⊢ ( Frac ‘ 𝑅 ) = ( Frac ‘ 𝑅 )
33 9 10 32 13 fracbas ⊢ ( ( ( Base ‘ 𝑅 ) × ( RLReg ‘ 𝑅 ) ) / ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( Base ‘ ( Frac ‘ 𝑅 ) )
34 31 33 sseqtrdi ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ⊆ ( Base ‘ ( Frac ‘ 𝑅 ) ) )
35 eqid ⊢ ( Base ‘ ( Frac ‘ 𝑅 ) ) = ( Base ‘ ( Frac ‘ 𝑅 ) )
36 22 35 ressbas2 ⊢ ( ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ⊆ ( Base ‘ ( Frac ‘ 𝑅 ) ) → ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( Base ‘ ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) )
37 34 36 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) = ( Base ‘ ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) )
38 37 f1oeq3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) –1-1-onto→ ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) ) )
39 28 38 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) )
40 eqid ⊢ ( Base ‘ ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) = ( Base ‘ ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) )
41 9 40 isrim ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingIso ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingHom ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) ) )
42 25 39 41 sylanbrc ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingIso ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) )
43 brrici ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ∈ ( 𝑅 RingIso ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) ) → 𝑅 ≃𝑟 ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) )
44 42 43 syl ⊢ ( 𝜑 → 𝑅 ≃𝑟 ( ( Frac ‘ 𝑅 ) ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ [ ⟨ 𝑥 , ( 1r ‘ 𝑅 ) ⟩ ] ( 𝑅 ~RL ( RLReg ‘ 𝑅 ) ) ) ) )
45 8 19 44 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑠 ∈ ( SubRing ‘ ( Frac ‘ 𝑅 ) ) 𝑅 ≃𝑟 ( ( Frac ‘ 𝑅 ) ↾s 𝑠 ) )
46 5 6 45 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑓 ∈ Field ∃ 𝑠 ∈ ( SubRing ‘ 𝑓 ) 𝑅 ≃𝑟 ( 𝑓 ↾s 𝑠 ) )