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	$$⊢\phi \to R\in \mathrm{IDomn}$$
Assertion	idomsubr	$$⊢\phi \to \exists f\in \mathrm{Field}\exists s\in \mathrm{SubRing}\left(f\right)R{\simeq }_{𝑟}\left(f{\upharpoonright }_{𝑠}s\right)$$

Proof

Step	Hyp	Ref	Expression
1		idomsubr.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
2		fveq2	Could not format ( f = ( Frac ` R ) -> ( SubRing ` f ) = ( SubRing ` ( Frac ` R ) ) ) : No typesetting found for |- ( f = ( Frac ` R ) -> ( SubRing ` f ) = ( SubRing ` ( Frac ` R ) ) ) with typecode |-
3		oveq1	Could not format ( f = ( Frac ` R ) -> ( f |`s s ) = ( ( Frac ` R ) |`s s ) ) : No typesetting found for |- ( f = ( Frac ` R ) -> ( f |`s s ) = ( ( Frac ` R ) |`s s ) ) with typecode |-
4	3	breq2d	Could not format ( f = ( Frac ` R ) -> ( R ~=r ( f |`s s ) <-> R ~=r ( ( Frac ` R ) |`s s ) ) ) : No typesetting found for |- ( f = ( Frac ` R ) -> ( R ~=r ( f |`s s ) <-> R ~=r ( ( Frac ` R ) |`s s ) ) ) with typecode |-
5	2 4	rexeqbidv	Could not format ( f = ( Frac ` R ) -> ( E. s e. ( SubRing ` f ) R ~=r ( f |`s s ) <-> E. s e. ( SubRing ` ( Frac ` R ) ) R ~=r ( ( Frac ` R ) |`s s ) ) ) : No typesetting found for |- ( f = ( Frac ` R ) -> ( E. s e. ( SubRing ` f ) R ~=r ( f |`s s ) <-> E. s e. ( SubRing ` ( Frac ` R ) ) R ~=r ( ( Frac ` R ) |`s s ) ) ) with typecode |-
6	1	fracfld	Could not format ( ph -> ( Frac ` R ) e. Field ) : No typesetting found for |- ( ph -> ( Frac ` R ) e. Field ) with typecode |-
7		oveq2	Could not format ( s = ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( Frac ` R ) |`s s ) = ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) : No typesetting found for |- ( s = ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( ( Frac ` R ) |`s s ) = ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) with typecode |-
8	7	breq2d	Could not format ( s = ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( R ~=r ( ( Frac ` R ) |`s s ) <-> R ~=r ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) : No typesetting found for |- ( s = ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) -> ( R ~=r ( ( Frac ` R ) |`s s ) <-> R ~=r ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) with typecode |-
9		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
10		eqid	$$⊢\mathrm{RLReg}\left(R\right)=\mathrm{RLReg}\left(R\right)$$
11		eqid	$$⊢1_R=1_R$$
12	1	idomcringd	$$⊢\phi \to R\in \mathrm{CRing}$$
13		eqid	Could not format ( R ~RL ( RLReg ` R ) ) = ( R ~RL ( RLReg ` R ) ) : No typesetting found for |- ( R ~RL ( RLReg ` R ) ) = ( R ~RL ( RLReg ` R ) ) with typecode |-
14		opeq1	$$⊢x=y\to ⟨x,1_R⟩=⟨y,1_R⟩$$
15	14	eceq1d	Could not format ( x = y -> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. y , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : No typesetting found for |- ( x = y -> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. y , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) with typecode |-
16	15	cbvmptv	Could not format ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) = ( y e. ( Base ` R ) |-> [ <. y , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : No typesetting found for |- ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) = ( y e. ( Base ` R ) |-> [ <. y , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) with typecode |-
17	9 10 11 12 13 16	fracf1	Could not format ( ph -> ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) /\ ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) ) ) : No typesetting found for |- ( ph -> ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) /\ ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) ) ) with typecode |-
18		rnrhmsubrg	Could not format ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( SubRing ` ( Frac ` R ) ) ) : No typesetting found for |- ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( SubRing ` ( Frac ` R ) ) ) with typecode |-
19	17 18	simpl2im	Could not format ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( SubRing ` ( Frac ` R ) ) ) : No typesetting found for |- ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( SubRing ` ( Frac ` R ) ) ) with typecode |-
20		ssidd	Could not format ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
21	17	simprd	Could not format ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) ) : No typesetting found for |- ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) ) with typecode |-
22		eqid	Could not format ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) = ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) = ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
23	22	resrhm2b	Could not format ( ( ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( SubRing ` ( Frac ` R ) ) /\ ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) -> ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) <-> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) ) : No typesetting found for |- ( ( ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( SubRing ` ( Frac ` R ) ) /\ ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) -> ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) <-> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) ) with typecode |-
24	23	biimpa	Could not format ( ( ( ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( SubRing ` ( Frac ` R ) ) /\ ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) /\ ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) ) -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) : No typesetting found for |- ( ( ( ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( SubRing ` ( Frac ` R ) ) /\ ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) /\ ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) ) -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) with typecode |-
25	19 20 21 24	syl21anc	Could not format ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) with typecode |-
26	17	simpld	Could not format ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
27		f1f1orn	Could not format ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
28	26 27	syl	Could not format ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
29		f1f	Could not format ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) --> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) --> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
30	26 29	syl	Could not format ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) --> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) --> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
31	30	frnd	Could not format ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) : No typesetting found for |- ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) ) with typecode |-
32		eqid	Could not format ( Frac ` R ) = ( Frac ` R ) : No typesetting found for |- ( Frac ` R ) = ( Frac ` R ) with typecode |-
33	9 10 32 13	fracbas	Could not format ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( Frac ` R ) ) : No typesetting found for |- ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( Frac ` R ) ) with typecode |-
34	31 33	sseqtrdi	Could not format ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ( Base ` ( Frac ` R ) ) ) : No typesetting found for |- ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ( Base ` ( Frac ` R ) ) ) with typecode |-
35		eqid	Could not format ( Base ` ( Frac ` R ) ) = ( Base ` ( Frac ` R ) ) : No typesetting found for |- ( Base ` ( Frac ` R ) ) = ( Base ` ( Frac ` R ) ) with typecode |-
36	22 35	ressbas2	Could not format ( ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ( Base ` ( Frac ` R ) ) -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) : No typesetting found for |- ( ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ( Base ` ( Frac ` R ) ) -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) with typecode |-
37	34 36	syl	Could not format ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) : No typesetting found for |- ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) with typecode |-
38	37	f1oeq3d	Could not format ( ph -> ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) <-> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) <-> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) ) with typecode |-
39	28 38	mpbid	Could not format ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) with typecode |-
40		eqid	Could not format ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) = ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) : No typesetting found for |- ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) = ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) with typecode |-
41	9 40	isrim	Could not format ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingIso ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) <-> ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) /\ ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) ) : No typesetting found for |- ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingIso ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) <-> ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) /\ ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) -1-1-onto-> ( Base ` ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) ) with typecode |-
42	25 39 41	sylanbrc	Could not format ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingIso ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingIso ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) ) with typecode |-
43		brrici	Could not format ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingIso ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) -> R ~=r ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) : No typesetting found for |- ( ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingIso ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) -> R ~=r ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) with typecode |-
44	42 43	syl	Could not format ( ph -> R ~=r ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) : No typesetting found for |- ( ph -> R ~=r ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) ) with typecode |-
45	8 19 44	rspcedvdw	Could not format ( ph -> E. s e. ( SubRing ` ( Frac ` R ) ) R ~=r ( ( Frac ` R ) |`s s ) ) : No typesetting found for |- ( ph -> E. s e. ( SubRing ` ( Frac ` R ) ) R ~=r ( ( Frac ` R ) |`s s ) ) with typecode |-
46	5 6 45	rspcedvdw	$$⊢\phi \to \exists f\in \mathrm{Field}\exists s\in \mathrm{SubRing}\left(f\right)R{\simeq }_{𝑟}\left(f{\upharpoonright }_{𝑠}s\right)$$