Metamath Proof Explorer

Theorem qsssubdrg

Description: The rational numbers are a subset of any subfield of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion qsssubdrg 
|- ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) -> QQ C_ R )

Proof

Step Hyp Ref Expression
1 elq 
 |-  ( z e. QQ <-> E. x e. ZZ E. y e. NN z = ( x / y ) )
2 drngring 
 |-  ( ( CCfld |`s R ) e. DivRing -> ( CCfld |`s R ) e. Ring )
3 2 ad2antlr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> ( CCfld |`s R ) e. Ring )
4 zsssubrg 
 |-  ( R e. ( SubRing ` CCfld ) -> ZZ C_ R )
5 4 ad2antrr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> ZZ C_ R )
6 eqid 
 |-  ( CCfld |`s R ) = ( CCfld |`s R )
7 6 subrgbas 
 |-  ( R e. ( SubRing ` CCfld ) -> R = ( Base ` ( CCfld |`s R ) ) )
8 7 ad2antrr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> R = ( Base ` ( CCfld |`s R ) ) )
9 5 8 sseqtrd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> ZZ C_ ( Base ` ( CCfld |`s R ) ) )
10 simprl 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> x e. ZZ )
11 9 10 sseldd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> x e. ( Base ` ( CCfld |`s R ) ) )
12 nnz 
 |-  ( y e. NN -> y e. ZZ )
13 12 ad2antll 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> y e. ZZ )
14 9 13 sseldd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> y e. ( Base ` ( CCfld |`s R ) ) )
15 nnne0 
 |-  ( y e. NN -> y =/= 0 )
16 15 ad2antll 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> y =/= 0 )
17 cnfld0 
 |-  0 = ( 0g ` CCfld )
18 6 17 subrg0 
 |-  ( R e. ( SubRing ` CCfld ) -> 0 = ( 0g ` ( CCfld |`s R ) ) )
19 18 ad2antrr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> 0 = ( 0g ` ( CCfld |`s R ) ) )
20 16 19 neeqtrd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> y =/= ( 0g ` ( CCfld |`s R ) ) )
21 eqid 
 |-  ( Base ` ( CCfld |`s R ) ) = ( Base ` ( CCfld |`s R ) )
22 eqid 
 |-  ( Unit ` ( CCfld |`s R ) ) = ( Unit ` ( CCfld |`s R ) )
23 eqid 
 |-  ( 0g ` ( CCfld |`s R ) ) = ( 0g ` ( CCfld |`s R ) )
24 21 22 23 drngunit 
 |-  ( ( CCfld |`s R ) e. DivRing -> ( y e. ( Unit ` ( CCfld |`s R ) ) <-> ( y e. ( Base ` ( CCfld |`s R ) ) /\ y =/= ( 0g ` ( CCfld |`s R ) ) ) ) )
25 24 ad2antlr 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> ( y e. ( Unit ` ( CCfld |`s R ) ) <-> ( y e. ( Base ` ( CCfld |`s R ) ) /\ y =/= ( 0g ` ( CCfld |`s R ) ) ) ) )
26 14 20 25 mpbir2and 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> y e. ( Unit ` ( CCfld |`s R ) ) )
27 eqid 
 |-  ( /r ` ( CCfld |`s R ) ) = ( /r ` ( CCfld |`s R ) )
28 21 22 27 dvrcl 
 |-  ( ( ( CCfld |`s R ) e. Ring /\ x e. ( Base ` ( CCfld |`s R ) ) /\ y e. ( Unit ` ( CCfld |`s R ) ) ) -> ( x ( /r ` ( CCfld |`s R ) ) y ) e. ( Base ` ( CCfld |`s R ) ) )
29 3 11 26 28 syl3anc 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> ( x ( /r ` ( CCfld |`s R ) ) y ) e. ( Base ` ( CCfld |`s R ) ) )
30 simpll 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> R e. ( SubRing ` CCfld ) )
31 5 10 sseldd 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> x e. R )
32 cnflddiv 
 |-  / = ( /r ` CCfld )
33 6 32 22 27 subrgdv 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ x e. R /\ y e. ( Unit ` ( CCfld |`s R ) ) ) -> ( x / y ) = ( x ( /r ` ( CCfld |`s R ) ) y ) )
34 30 31 26 33 syl3anc 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> ( x / y ) = ( x ( /r ` ( CCfld |`s R ) ) y ) )
35 29 34 8 3eltr4d 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> ( x / y ) e. R )
36 eleq1 
 |-  ( z = ( x / y ) -> ( z e. R <-> ( x / y ) e. R ) )
37 35 36 syl5ibrcom 
 |-  ( ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) /\ ( x e. ZZ /\ y e. NN ) ) -> ( z = ( x / y ) -> z e. R ) )
38 37 rexlimdvva 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) -> ( E. x e. ZZ E. y e. NN z = ( x / y ) -> z e. R ) )
39 1 38 biimtrid 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) -> ( z e. QQ -> z e. R ) )
40 39 ssrdv 
 |-  ( ( R e. ( SubRing ` CCfld ) /\ ( CCfld |`s R ) e. DivRing ) -> QQ C_ R )