Step | Hyp | Ref
| Expression |
1 | | qqhrhm.1 |
. . 3
ℂfld ↾s |
2 | 1 | qrngbas 25308 |
. 2
|
3 | 1 | qrng1 25311 |
. 2
|
4 | | eqid 2622 |
. 2
|
5 | | qex 11800 |
. . 3
|
6 | | cnfldmul 19752 |
. . . 4
ℂfld |
7 | 1, 6 | ressmulr 16006 |
. . 3
|
8 | 5, 7 | ax-mp 5 |
. 2
|
9 | | eqid 2622 |
. 2
|
10 | 1 | qdrng 25309 |
. . 3
|
11 | | drngring 18754 |
. . 3
|
12 | 10, 11 | mp1i 13 |
. 2
Field
chr
|
13 | | isfld 18756 |
. . . . 5
Field
|
14 | 13 | simplbi 476 |
. . . 4
Field |
15 | 14 | adantr 481 |
. . 3
Field
chr
|
16 | | drngring 18754 |
. . 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 30029 |
. . 3
chr
QQHom |
22 | 14, 21 | sylan 488 |
. 2
Field
chr
QQHom |
23 | | eqid 2622 |
. . . 4
Unit Unit |
24 | | eqid 2622 |
. . . 4
|
25 | 13 | simprbi 480 |
. . . . 5
Field |
26 | 25 | ad2antrr 762 |
. . . 4
Field chr
|
27 | 20 | zrhrhm 19860 |
. . . . . . 7
ℤring RingHom |
28 | | zringbas 19824 |
. . . . . . . 8
ℤring |
29 | 28, 18 | rhmf 18726 |
. . . . . . 7
ℤring RingHom |
30 | 17, 27, 29 | 3syl 18 |
. . . . . 6
Field
chr
|
31 | 30 | adantr 481 |
. . . . 5
Field chr |
32 | | qnumcl 15448 |
. . . . . 6
numer |
33 | 32 | ad2antrl 764 |
. . . . 5
Field chr numer |
34 | 31, 33 | ffvelrnd 6360 |
. . . 4
Field chr numer |
35 | 14 | ad2antrr 762 |
. . . . . 6
Field chr
|
36 | | simplr 792 |
. . . . . 6
Field chr chr |
37 | 35, 36 | jca 554 |
. . . . 5
Field chr chr |
38 | | qdencl 15449 |
. . . . . . 7
denom |
39 | 38 | ad2antrl 764 |
. . . . . 6
Field chr denom |
40 | 39 | nnzd 11481 |
. . . . 5
Field chr denom |
41 | 39 | nnne0d 11065 |
. . . . 5
Field chr denom |
42 | | eqid 2622 |
. . . . . 6
|
43 | 18, 20, 42 | elzrhunit 30023 |
. . . . 5
chr denom denom denom Unit |
44 | 37, 40, 41, 43 | syl12anc 1324 |
. . . 4
Field chr denom Unit |
45 | | qnumcl 15448 |
. . . . . 6
numer |
46 | 45 | ad2antll 765 |
. . . . 5
Field chr numer |
47 | 31, 46 | ffvelrnd 6360 |
. . . 4
Field chr numer |
48 | | qdencl 15449 |
. . . . . . 7
denom |
49 | 48 | ad2antll 765 |
. . . . . 6
Field chr denom |
50 | 49 | nnzd 11481 |
. . . . 5
Field chr denom |
51 | 49 | nnne0d 11065 |
. . . . 5
Field chr denom |
52 | 18, 20, 42 | elzrhunit 30023 |
. . . . 5
chr denom denom denom Unit |
53 | 37, 50, 51, 52 | syl12anc 1324 |
. . . 4
Field chr denom Unit |
54 | 18, 23, 24, 19, 9, 26, 34, 44, 47, 53 | rdivmuldivd 29791 |
. . 3
Field chr numer denomnumer denom numernumer
denomdenom |
55 | | qeqnumdivden 15454 |
. . . . . . 7
numer denom |
56 | 55 | fveq2d 6195 |
. . . . . 6
QQHom QQHomnumer denom |
57 | 56 | ad2antrl 764 |
. . . . 5
Field chr QQHom QQHomnumer denom |
58 | 18, 19, 20 | qqhvq 30031 |
. . . . . 6
chr numer denom denom QQHomnumer denom numer denom |
59 | 37, 33, 40, 41, 58 | syl13anc 1328 |
. . . . 5
Field chr QQHomnumer denom numer denom |
60 | 57, 59 | eqtrd 2656 |
. . . 4
Field chr QQHom numer denom |
61 | | qeqnumdivden 15454 |
. . . . . . 7
numer denom |
62 | 61 | fveq2d 6195 |
. . . . . 6
QQHom QQHomnumer denom |
63 | 62 | ad2antll 765 |
. . . . 5
Field chr QQHom QQHomnumer denom |
64 | 18, 19, 20 | qqhvq 30031 |
. . . . . 6
chr numer denom denom QQHomnumer denom numer denom |
65 | 37, 46, 50, 51, 64 | syl13anc 1328 |
. . . . 5
Field chr QQHomnumer denom numer denom |
66 | 63, 65 | eqtrd 2656 |
. . . 4
Field chr QQHom numer denom |
67 | 60, 66 | oveq12d 6668 |
. . 3
Field chr QQHomQQHom numer denomnumer denom |
68 | 55 | ad2antrl 764 |
. . . . . . 7
Field chr
numer denom |
69 | 61 | ad2antll 765 |
. . . . . . 7
Field chr numer denom |
70 | 68, 69 | oveq12d 6668 |
. . . . . 6
Field chr numer denom numer denom |
71 | 33 | zcnd 11483 |
. . . . . . 7
Field chr numer |
72 | 40 | zcnd 11483 |
. . . . . . 7
Field chr denom |
73 | 46 | zcnd 11483 |
. . . . . . 7
Field chr numer |
74 | 50 | zcnd 11483 |
. . . . . . 7
Field chr denom |
75 | 71, 72, 73, 74, 41, 51 | divmuldivd 10842 |
. . . . . 6
Field chr numer denom numer denom numer numer denom denom |
76 | 70, 75 | eqtrd 2656 |
. . . . 5
Field chr numer numer denom denom |
77 | 76 | fveq2d 6195 |
. . . 4
Field chr QQHom QQHomnumer numer denom denom |
78 | 33, 46 | zmulcld 11488 |
. . . . 5
Field chr numer numer |
79 | 40, 50 | zmulcld 11488 |
. . . . 5
Field chr denom denom |
80 | 72, 74, 41, 51 | mulne0d 10679 |
. . . . 5
Field chr denom denom |
81 | 18, 19, 20 | qqhvq 30031 |
. . . . 5
chr numer numer denom denom denom denom QQHomnumer numer denom denom numer numer denom denom |
82 | 37, 78, 79, 80, 81 | syl13anc 1328 |
. . . 4
Field chr QQHomnumer 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 19827 |
. . . . . . 7
ℤring |
86 | 28, 85, 9 | rhmmul 18727 |
. . . . . 6
ℤring
RingHom numer numer numer numer numernumer |
87 | 84, 33, 46, 86 | syl3anc 1326 |
. . . . 5
Field chr numer numer numernumer |
88 | 28, 85, 9 | rhmmul 18727 |
. . . . . 6
ℤring
RingHom denom denom denom denom denomdenom |
89 | 84, 40, 50, 88 | syl3anc 1326 |
. . . . 5
Field chr denom denom denomdenom |
90 | 87, 89 | oveq12d 6668 |
. . . 4
Field chr numer numer denom denom numernumer denomdenom |
91 | 77, 82, 90 | 3eqtrd 2660 |
. . 3
Field chr QQHom numernumer denomdenom |
92 | 54, 67, 91 | 3eqtr4rd 2667 |
. 2
Field chr QQHom QQHomQQHom |
93 | | cnfldadd 19751 |
. . . 4
ℂfld |
94 | 1, 93 | ressplusg 15993 |
. . 3
|
95 | 5, 94 | ax-mp 5 |
. 2
|
96 | 18, 19, 20 | qqhf 30030 |
. . 3
chr
QQHom |
97 | 14, 96 | sylan 488 |
. 2
Field
chr
QQHom |
98 | 33, 50 | zmulcld 11488 |
. . . . 5
Field chr numer denom |
99 | 31, 98 | ffvelrnd 6360 |
. . . 4
Field chr numer denom |
100 | 46, 40 | zmulcld 11488 |
. . . . 5
Field chr numer denom |
101 | 31, 100 | ffvelrnd 6360 |
. . . 4
Field chr numer denom |
102 | 23, 9 | unitmulcl 18664 |
. . . . . 6
denom Unit denom Unit denomdenom Unit |
103 | 83, 44, 53, 102 | syl3anc 1326 |
. . . . 5
Field chr denomdenom Unit |
104 | 89, 103 | eqeltrd 2701 |
. . . 4
Field chr denom denom Unit |
105 | 18, 23, 24, 19 | dvrdir 29790 |
. . . 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 1328 |
. . 3
Field chr numer denom numer denom denom denom numer denom denom denom numer denom denom denom |
107 | 68, 69 | oveq12d 6668 |
. . . . . 6
Field chr numer denom numer denom |
108 | 71, 72, 73, 74, 41, 51 | divadddivd 10845 |
. . . . . 6
Field chr numer denom numer denom numer denom numer denom denom denom |
109 | 107, 108 | eqtrd 2656 |
. . . . 5
Field chr numer denom numer denom denom denom |
110 | 109 | fveq2d 6195 |
. . . 4
Field chr QQHom QQHomnumer denom numer denom denom denom |
111 | 98, 100 | zaddcld 11486 |
. . . . 5
Field chr numer denom numer denom |
112 | 18, 19, 20 | qqhvq 30031 |
. . . . 5
chr numer denom numer denom denom denom denom denom
QQHomnumer denom numer denom denom denom numer denom numer denom
denom denom |
113 | 37, 111, 79, 80, 112 | syl13anc 1328 |
. . . 4
Field chr QQHomnumer denom numer denom denom denom numer denom numer denom
denom denom |
114 | | rhmghm 18725 |
. . . . . 6
ℤring RingHom ℤring |
115 | 84, 114 | syl 17 |
. . . . 5
Field chr
ℤring
|
116 | | zringplusg 19825 |
. . . . . . 7
ℤring |
117 | 28, 116, 24 | ghmlin 17665 |
. . . . . 6
ℤring numer denom numer denom numer denom numer denom numer denom numer denom |
118 | 117 | oveq1d 6665 |
. . . . 5
ℤring numer denom numer denom numer denom numer denom
denom denom numer denom numer denom
denom denom |
119 | 115, 98, 100, 118 | syl3anc 1326 |
. . . 4
Field chr numer denom numer denom
denom denom numer denom numer denom
denom denom |
120 | 110, 113,
119 | 3eqtrd 2660 |
. . 3
Field chr QQHom numer denom numer denom denom denom |
121 | 23, 28, 19, 85 | rhmdvd 29821 |
. . . . . 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 1344 |
. . . . 5
Field chr numer denom numer denom denom denom |
123 | 57, 59, 122 | 3eqtrd 2660 |
. . . 4
Field chr QQHom numer denom denom denom |
124 | 23, 28, 19, 85 | rhmdvd 29821 |
. . . . . . 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 1344 |
. . . . . 6
Field chr numer denom numer denom denom denom |
126 | 72, 74 | mulcomd 10061 |
. . . . . . . 8
Field chr denom denom denom denom |
127 | 126 | fveq2d 6195 |
. . . . . . 7
Field chr denom denom denom denom |
128 | 127 | oveq2d 6666 |
. . . . . 6
Field chr numer denom denom denom numer denom denom denom |
129 | 125, 65, 128 | 3eqtr4d 2666 |
. . . . 5
Field chr QQHomnumer denom numer denom denom denom |
130 | 63, 129 | eqtrd 2656 |
. . . 4
Field chr QQHom numer denom denom denom |
131 | 123, 130 | oveq12d 6668 |
. . 3
Field chr QQHom QQHom numer denom denom denom numer denom denom denom |
132 | 106, 120,
131 | 3eqtr4d 2666 |
. 2
Field chr QQHom QQHom QQHom |
133 | 2, 3, 4, 8, 9, 12,
17, 22, 92, 18, 95, 24, 97, 132 | isrhmd 18729 |
1
Field
chr
QQHom RingHom |