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 
|- ( ph -> R e. IDomn )
Assertion idomsubr 
|- ( ph -> E. f e. Field E. s e. ( SubRing ` f ) R ~=r ( f |`s s ) )

Proof

Step Hyp Ref Expression
1 idomsubr.1 
 |-  ( ph -> R e. IDomn )
2 fveq2 
 |-  ( f = ( Frac ` R ) -> ( SubRing ` f ) = ( SubRing ` ( Frac ` R ) ) )
3 oveq1 
 |-  ( f = ( Frac ` R ) -> ( f |`s s ) = ( ( Frac ` R ) |`s s ) )
4 3 breq2d 
 |-  ( f = ( Frac ` R ) -> ( R ~=r ( f |`s s ) <-> R ~=r ( ( Frac ` R ) |`s s ) ) )
5 2 4 rexeqbidv 
 |-  ( 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 ) ) )
6 1 fracfld 
 |-  ( ph -> ( Frac ` R ) e. Field )
7 oveq2 
 |-  ( 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 ) ) ) ) )
8 7 breq2d 
 |-  ( 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 ) ) ) ) ) )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 eqid 
 |-  ( RLReg ` R ) = ( RLReg ` R )
11 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
12 1 idomcringd 
 |-  ( ph -> R e. CRing )
13 eqid 
 |-  ( R ~RL ( RLReg ` R ) ) = ( R ~RL ( RLReg ` R ) )
14 opeq1 
 |-  ( x = y -> <. x , ( 1r ` R ) >. = <. y , ( 1r ` R ) >. )
15 14 eceq1d 
 |-  ( x = y -> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) = [ <. y , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) )
16 15 cbvmptv 
 |-  ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) = ( y e. ( Base ` R ) |-> [ <. y , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) )
17 9 10 11 12 13 16 fracf1 
 |-  ( 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 ) ) ) )
18 rnrhmsubrg 
 |-  ( ( 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 ) ) )
19 17 18 simpl2im 
 |-  ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( SubRing ` ( Frac ` R ) ) )
20 ssidd 
 |-  ( 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 ) ) ) )
21 17 simprd 
 |-  ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) e. ( R RingHom ( Frac ` R ) ) )
22 eqid 
 |-  ( ( 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 ) ) ) )
23 22 resrhm2b 
 |-  ( ( 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 ) ) ) ) ) ) )
24 23 biimpa 
 |-  ( ( ( 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 ) ) ) ) ) )
25 19 20 21 24 syl21anc 
 |-  ( 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 ) ) ) ) ) )
26 17 simpld 
 |-  ( 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 ) ) ) )
27 f1f1orn 
 |-  ( ( 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 ) ) ) )
28 26 27 syl 
 |-  ( 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 ) ) ) )
29 f1f 
 |-  ( ( 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 ) ) ) )
30 26 29 syl 
 |-  ( ph -> ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) : ( Base ` R ) --> ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) )
31 30 frnd 
 |-  ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) )
32 eqid 
 |-  ( Frac ` R ) = ( Frac ` R )
33 9 10 32 13 fracbas 
 |-  ( ( ( Base ` R ) X. ( RLReg ` R ) ) /. ( R ~RL ( RLReg ` R ) ) ) = ( Base ` ( Frac ` R ) )
34 31 33 sseqtrdi 
 |-  ( ph -> ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) C_ ( Base ` ( Frac ` R ) ) )
35 eqid 
 |-  ( Base ` ( Frac ` R ) ) = ( Base ` ( Frac ` R ) )
36 22 35 ressbas2 
 |-  ( 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 ) ) ) ) ) )
37 34 36 syl 
 |-  ( 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 ) ) ) ) ) )
38 37 f1oeq3d 
 |-  ( 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 ) ) ) ) ) ) )
39 28 38 mpbid 
 |-  ( 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 ) ) ) ) ) )
40 eqid 
 |-  ( 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 ) ) ) ) )
41 9 40 isrim 
 |-  ( ( 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 ) ) ) ) ) ) )
42 25 39 41 sylanbrc 
 |-  ( 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 ) ) ) ) ) )
43 brrici 
 |-  ( ( 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 ) ) ) ) )
44 42 43 syl 
 |-  ( ph -> R ~=r ( ( Frac ` R ) |`s ran ( x e. ( Base ` R ) |-> [ <. x , ( 1r ` R ) >. ] ( R ~RL ( RLReg ` R ) ) ) ) )
45 8 19 44 rspcedvdw 
 |-  ( ph -> E. s e. ( SubRing ` ( Frac ` R ) ) R ~=r ( ( Frac ` R ) |`s s ) )
46 5 6 45 rspcedvdw 
 |-  ( ph -> E. f e. Field E. s e. ( SubRing ` f ) R ~=r ( f |`s s ) )