Step | Hyp | Ref
| Expression |
1 | | qqhrhm.1 |
. . 3
ℂfld ↾s   |
2 | 1 | qrngbas 24450 |
. 2
     |
3 | 1 | qrng1 24453 |
. 2
     |
4 | | eqid 2450 |
. 2
         |
5 | | qex 11273 |
. . 3
 |
6 | | cnfldmul 18969 |
. . . 4
  ℂfld |
7 | 1, 6 | ressmulr 15243 |
. . 3
       |
8 | 5, 7 | ax-mp 5 |
. 2
     |
9 | | eqid 2450 |
. 2
         |
10 | 1 | qdrng 24451 |
. . 3
 |
11 | | drngring 17975 |
. . 3
   |
12 | 10, 11 | mp1i 13 |
. 2
  Field
chr  
  |
13 | | isfld 17977 |
. . . . 5
 Field 
   |
14 | 13 | simplbi 462 |
. . . 4
 Field   |
15 | 14 | adantr 467 |
. . 3
  Field
chr  
  |
16 | | drngring 17975 |
. . 3
   |
17 | 15, 16 | syl 17 |
. 2
  Field
chr  
  |
18 | | qqhval2.0 |
. . . 4
     |
19 | | qqhval2.1 |
. . . 4
/r   |
20 | | qqhval2.2 |
. . . 4
 RHom   |
21 | 18, 19, 20 | qqh1 28782 |
. . 3
  chr  
 QQHom           |
22 | 14, 21 | sylan 474 |
. 2
  Field
chr  
 QQHom           |
23 | | eqid 2450 |
. . . 4
Unit  Unit   |
24 | | eqid 2450 |
. . . 4
       |
25 | 13 | simprbi 466 |
. . . . 5
 Field   |
26 | 25 | ad2antrr 731 |
. . . 4
   Field chr     
  |
27 | 20 | zrhrhm 19076 |
. . . . . . 7

ℤring RingHom    |
28 | | zringbas 19038 |
. . . . . . . 8
  ℤring |
29 | 28, 18 | rhmf 17947 |
. . . . . . 7
 ℤring RingHom        |
30 | 17, 27, 29 | 3syl 18 |
. . . . . 6
  Field
chr  
      |
31 | 30 | adantr 467 |
. . . . 5
   Field chr            |
32 | | qnumcl 14682 |
. . . . . 6
 numer    |
33 | 32 | ad2antrl 733 |
. . . . 5
   Field chr      numer    |
34 | 31, 33 | ffvelrnd 6021 |
. . . 4
   Field chr         numer     |
35 | 14 | ad2antrr 731 |
. . . . . 6
   Field chr     
  |
36 | | simplr 761 |
. . . . . 6
   Field chr      chr    |
37 | 35, 36 | jca 535 |
. . . . 5
   Field chr       chr     |
38 | | qdencl 14683 |
. . . . . . 7
 denom    |
39 | 38 | ad2antrl 733 |
. . . . . 6
   Field chr      denom    |
40 | 39 | nnzd 11036 |
. . . . 5
   Field chr      denom    |
41 | 39 | nnne0d 10651 |
. . . . 5
   Field chr      denom    |
42 | | eqid 2450 |
. . . . . 6
         |
43 | 18, 20, 42 | elzrhunit 28776 |
. . . . 5
   chr    denom  denom       denom   Unit    |
44 | 37, 40, 41, 43 | syl12anc 1265 |
. . . 4
   Field chr         denom   Unit    |
45 | | qnumcl 14682 |
. . . . . 6
 numer    |
46 | 45 | ad2antll 734 |
. . . . 5
   Field chr      numer    |
47 | 31, 46 | ffvelrnd 6021 |
. . . 4
   Field chr         numer     |
48 | | qdencl 14683 |
. . . . . . 7
 denom    |
49 | 48 | ad2antll 734 |
. . . . . 6
   Field chr      denom    |
50 | 49 | nnzd 11036 |
. . . . 5
   Field chr      denom    |
51 | 49 | nnne0d 10651 |
. . . . 5
   Field chr      denom    |
52 | 18, 20, 42 | elzrhunit 28776 |
. . . . 5
   chr    denom  denom       denom   Unit    |
53 | 37, 50, 51, 52 | syl12anc 1265 |
. . . 4
   Field chr         denom   Unit    |
54 | 18, 23, 24, 19, 9, 26, 34, 44, 47, 53 | rdivmuldivd 28547 |
. . 3
   Field chr           numer      denom              numer      denom          numer            numer   
    denom            denom       |
55 | | qeqnumdivden 14688 |
. . . . . . 7
  numer  denom     |
56 | 55 | fveq2d 5867 |
. . . . . 6
  QQHom      QQHom     numer  denom      |
57 | 56 | ad2antrl 733 |
. . . . 5
   Field chr       QQHom      QQHom     numer  denom      |
58 | 18, 19, 20 | qqhvq 28784 |
. . . . . 6
   chr    numer  denom  denom     QQHom     numer  denom        numer      denom      |
59 | 37, 33, 40, 41, 58 | syl13anc 1269 |
. . . . 5
   Field chr       QQHom     numer  denom        numer      denom      |
60 | 57, 59 | eqtrd 2484 |
. . . 4
   Field chr       QQHom         numer      denom      |
61 | | qeqnumdivden 14688 |
. . . . . . 7
  numer  denom     |
62 | 61 | fveq2d 5867 |
. . . . . 6
  QQHom      QQHom     numer  denom      |
63 | 62 | ad2antll 734 |
. . . . 5
   Field chr       QQHom      QQHom     numer  denom      |
64 | 18, 19, 20 | qqhvq 28784 |
. . . . . 6
   chr    numer  denom  denom     QQHom     numer  denom        numer      denom      |
65 | 37, 46, 50, 51, 64 | syl13anc 1269 |
. . . . 5
   Field chr       QQHom     numer  denom        numer      denom      |
66 | 63, 65 | eqtrd 2484 |
. . . 4
   Field chr       QQHom         numer      denom      |
67 | 60, 66 | oveq12d 6306 |
. . 3
   Field chr        QQHom            QQHom           numer      denom              numer      denom       |
68 | 55 | ad2antrl 733 |
. . . . . . 7
   Field chr     
 numer  denom     |
69 | 61 | ad2antll 734 |
. . . . . . 7
   Field chr       numer  denom     |
70 | 68, 69 | oveq12d 6306 |
. . . . . 6
   Field chr          numer  denom    numer  denom      |
71 | 33 | zcnd 11038 |
. . . . . . 7
   Field chr      numer    |
72 | 40 | zcnd 11038 |
. . . . . . 7
   Field chr      denom    |
73 | 46 | zcnd 11038 |
. . . . . . 7
   Field chr      numer    |
74 | 50 | zcnd 11038 |
. . . . . . 7
   Field chr      denom    |
75 | 71, 72, 73, 74, 41, 51 | divmuldivd 10421 |
. . . . . 6
   Field chr        numer  denom    numer  denom      numer  numer    denom  denom      |
76 | 70, 75 | eqtrd 2484 |
. . . . 5
   Field chr          numer  numer    denom  denom      |
77 | 76 | fveq2d 5867 |
. . . 4
   Field chr       QQHom        QQHom      numer  numer    denom  denom       |
78 | 33, 46 | zmulcld 11043 |
. . . . 5
   Field chr       numer  numer     |
79 | 40, 50 | zmulcld 11043 |
. . . . 5
   Field chr       denom  denom     |
80 | 72, 74, 41, 51 | mulne0d 10261 |
. . . . 5
   Field chr       denom  denom     |
81 | 18, 19, 20 | qqhvq 28784 |
. . . . 5
   chr     numer  numer    denom  denom    denom  denom      QQHom      numer  numer    denom  denom          numer  numer        denom  denom       |
82 | 37, 78, 79, 80, 81 | syl13anc 1269 |
. . . 4
   Field chr       QQHom      numer  numer    denom  denom          numer  numer        denom  denom       |
83 | 35, 16 | syl 17 |
. . . . . . 7
   Field chr     
  |
84 | 83, 27 | syl 17 |
. . . . . 6
   Field chr     
ℤring
RingHom    |
85 | | zringmulr 19041 |
. . . . . . 7
  ℤring |
86 | 28, 85, 9 | rhmmul 17948 |
. . . . . 6
  ℤring
RingHom  numer  numer       numer  numer        numer            numer      |
87 | 84, 33, 46, 86 | syl3anc 1267 |
. . . . 5
   Field chr          numer  numer        numer            numer      |
88 | 28, 85, 9 | rhmmul 17948 |
. . . . . 6
  ℤring
RingHom  denom  denom       denom  denom        denom            denom      |
89 | 84, 40, 50, 88 | syl3anc 1267 |
. . . . 5
   Field chr          denom  denom        denom            denom      |
90 | 87, 89 | oveq12d 6306 |
. . . 4
   Field chr           numer  numer        denom  denom          numer            numer        denom            denom       |
91 | 77, 82, 90 | 3eqtrd 2488 |
. . 3
   Field chr       QQHom            numer            numer        denom            denom       |
92 | 54, 67, 91 | 3eqtr4rd 2495 |
. 2
   Field chr       QQHom         QQHom            QQHom        |
93 | | cnfldadd 18968 |
. . . 4
 ℂfld |
94 | 1, 93 | ressplusg 15232 |
. . 3
      |
95 | 5, 94 | ax-mp 5 |
. 2
    |
96 | 18, 19, 20 | qqhf 28783 |
. . 3
  chr  
QQHom        |
97 | 14, 96 | sylan 474 |
. 2
  Field
chr  
QQHom        |
98 | 33, 50 | zmulcld 11043 |
. . . . 5
   Field chr       numer  denom     |
99 | 31, 98 | ffvelrnd 6021 |
. . . 4
   Field chr          numer  denom      |
100 | 46, 40 | zmulcld 11043 |
. . . . 5
   Field chr       numer  denom     |
101 | 31, 100 | ffvelrnd 6021 |
. . . 4
   Field chr          numer  denom      |
102 | 23, 9 | unitmulcl 17885 |
. . . . . 6
     denom   Unit     denom   Unit       denom            denom    Unit    |
103 | 83, 44, 53, 102 | syl3anc 1267 |
. . . . 5
   Field chr          denom            denom    Unit    |
104 | 89, 103 | eqeltrd 2528 |
. . . 4
   Field chr          denom  denom    Unit    |
105 | 18, 23, 24, 19 | dvrdir 28546 |
. . . 4
       numer  denom        numer  denom        denom  denom    Unit          numer  denom             numer  denom         denom  denom           numer  denom        denom  denom               numer  denom        denom  denom        |
106 | 83, 99, 101, 104, 105 | syl13anc 1269 |
. . 3
   Field chr            numer  denom             numer  denom         denom  denom           numer  denom        denom  denom               numer  denom        denom  denom        |
107 | 68, 69 | oveq12d 6306 |
. . . . . 6
   Field chr          numer  denom    numer  denom      |
108 | 71, 72, 73, 74, 41, 51 | divadddivd 10424 |
. . . . . 6
   Field chr        numer  denom    numer  denom       numer  denom    numer  denom     denom  denom      |
109 | 107, 108 | eqtrd 2484 |
. . . . 5
   Field chr           numer  denom    numer  denom     denom  denom      |
110 | 109 | fveq2d 5867 |
. . . 4
   Field chr       QQHom        QQHom       numer  denom    numer  denom     denom  denom       |
111 | 98, 100 | zaddcld 11041 |
. . . . 5
   Field chr        numer  denom    numer  denom      |
112 | 18, 19, 20 | qqhvq 28784 |
. . . . 5
   chr      numer  denom    numer  denom     denom  denom    denom  denom    
 QQHom       numer  denom    numer  denom     denom  denom           numer  denom    numer  denom    
    denom  denom       |
113 | 37, 111, 79, 80, 112 | syl13anc 1269 |
. . . 4
   Field chr       QQHom       numer  denom    numer  denom     denom  denom           numer  denom    numer  denom    
    denom  denom       |
114 | | rhmghm 17946 |
. . . . . 6
 ℤring RingHom  ℤring    |
115 | 84, 114 | syl 17 |
. . . . 5
   Field chr     
ℤring
   |
116 | | zringplusg 19039 |
. . . . . . 7
 ℤring |
117 | 28, 116, 24 | ghmlin 16881 |
. . . . . 6
  ℤring   numer  denom    numer  denom         numer  denom    numer  denom          numer  denom             numer  denom       |
118 | 117 | oveq1d 6303 |
. . . . 5
  ℤring   numer  denom    numer  denom          numer  denom    numer  denom    
    denom  denom           numer  denom             numer  denom    
    denom  denom       |
119 | 115, 98, 100, 118 | syl3anc 1267 |
. . . 4
   Field chr            numer  denom    numer  denom    
    denom  denom           numer  denom             numer  denom    
    denom  denom       |
120 | 110, 113,
119 | 3eqtrd 2488 |
. . 3
   Field chr       QQHom             numer  denom             numer  denom         denom  denom       |
121 | 23, 28, 19, 85 | rhmdvd 28577 |
. . . . . 6
  ℤring
RingHom   numer  denom  denom       denom   Unit     denom   Unit        numer      denom         numer  denom        denom  denom       |
122 | 84, 33, 40, 50, 44, 53, 121 | syl132anc 1285 |
. . . . 5
   Field chr          numer      denom         numer  denom        denom  denom       |
123 | 57, 59, 122 | 3eqtrd 2488 |
. . . 4
   Field chr       QQHom          numer  denom        denom  denom       |
124 | 23, 28, 19, 85 | rhmdvd 28577 |
. . . . . . 7
  ℤring
RingHom   numer  denom  denom       denom   Unit     denom   Unit        numer      denom         numer  denom        denom  denom       |
125 | 84, 46, 50, 40, 53, 44, 124 | syl132anc 1285 |
. . . . . 6
   Field chr          numer      denom         numer  denom        denom  denom       |
126 | 72, 74 | mulcomd 9661 |
. . . . . . . 8
   Field chr       denom  denom    denom  denom     |
127 | 126 | fveq2d 5867 |
. . . . . . 7
   Field chr          denom  denom        denom  denom      |
128 | 127 | oveq2d 6304 |
. . . . . 6
   Field chr           numer  denom        denom  denom          numer  denom        denom  denom       |
129 | 125, 65, 128 | 3eqtr4d 2494 |
. . . . 5
   Field chr       QQHom     numer  denom         numer  denom        denom  denom       |
130 | 63, 129 | eqtrd 2484 |
. . . 4
   Field chr       QQHom          numer  denom        denom  denom       |
131 | 123, 130 | oveq12d 6306 |
. . 3
   Field chr        QQHom           QQHom            numer  denom        denom  denom               numer  denom        denom  denom        |
132 | 106, 120,
131 | 3eqtr4d 2494 |
. 2
   Field chr       QQHom         QQHom           QQHom        |
133 | 2, 3, 4, 8, 9, 12,
17, 22, 92, 18, 95, 24, 97, 132 | isrhmd 17950 |
1
  Field
chr  
QQHom   RingHom    |