Step | Hyp | Ref
| Expression |
1 | | qqhucn.2 |
. . . 4
|
2 | | qqhucn.4 |
. . . 4
chr |
3 | | qqhucn.b |
. . . . 5
|
4 | | eqid 2622 |
. . . . 5
/r /r |
5 | | eqid 2622 |
. . . . 5
RHom RHom |
6 | 3, 4, 5 | qqhf 30030 |
. . . 4
chr
QQHom |
7 | 1, 2, 6 | syl2anc 693 |
. . 3
QQHom |
8 | | simpr 477 |
. . . . 5
|
9 | | qqhucn.1 |
. . . . . . . . . . . . . . 15
NrmRing |
10 | | nrgngp 22466 |
. . . . . . . . . . . . . . 15
NrmRing NrmGrp |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . 14
NrmGrp |
12 | 11 | ad2antrr 762 |
. . . . . . . . . . . . 13
NrmGrp |
13 | 7 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
QQHom |
14 | 13 | adantr 481 |
. . . . . . . . . . . . 13
QQHom |
15 | 7 | adantr 481 |
. . . . . . . . . . . . . 14
QQHom |
16 | 15 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
QQHom |
17 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
18 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
19 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
20 | 17, 3, 18, 19 | ngpdsr 22409 |
. . . . . . . . . . . . 13
NrmGrp
QQHom QQHom QQHomQQHom QQHomQQHom |
21 | 12, 14, 16, 20 | syl3anc 1326 |
. . . . . . . . . . . 12
QQHomQQHom QQHomQQHom |
22 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
23 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
24 | | qsubdrg 19798 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
ℂfld ↾s
|
25 | 24 | simpli 474 |
. . . . . . . . . . . . . . . . . 18
SubRingℂfld |
26 | | subrgsubg 18786 |
. . . . . . . . . . . . . . . . . 18
SubRingℂfld
SubGrpℂfld |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
SubGrpℂfld |
28 | | cnfldsub 19774 |
. . . . . . . . . . . . . . . . . 18
ℂfld |
29 | | qqhucn.q |
. . . . . . . . . . . . . . . . . 18
ℂfld ↾s |
30 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
31 | 28, 29, 30 | subgsub 17606 |
. . . . . . . . . . . . . . . . 17
SubGrpℂfld
|
32 | 27, 31 | mp3an1 1411 |
. . . . . . . . . . . . . . . 16
|
33 | 22, 23, 32 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
34 | 33 | fveq2d 6195 |
. . . . . . . . . . . . . 14
QQHom QQHom |
35 | 3, 4, 5, 29 | qqhghm 30032 |
. . . . . . . . . . . . . . . . 17
chr
QQHom |
36 | 1, 2, 35 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
QQHom |
37 | 36 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
QQHom |
38 | 29 | qrngbas 25308 |
. . . . . . . . . . . . . . . 16
|
39 | 38, 30, 18 | ghmsub 17668 |
. . . . . . . . . . . . . . 15
QQHom QQHom QQHomQQHom |
40 | 37, 22, 23, 39 | syl3anc 1326 |
. . . . . . . . . . . . . 14
QQHom QQHomQQHom |
41 | 34, 40 | eqtr2d 2657 |
. . . . . . . . . . . . 13
QQHomQQHom QQHom |
42 | 41 | fveq2d 6195 |
. . . . . . . . . . . 12
QQHomQQHom QQHom |
43 | 9, 1 | elind 3798 |
. . . . . . . . . . . . . 14
NrmRing |
44 | 43 | ad2antrr 762 |
. . . . . . . . . . . . 13
NrmRing
|
45 | | qqhucn.3 |
. . . . . . . . . . . . . 14
NrmMod |
46 | 45 | ad2antrr 762 |
. . . . . . . . . . . . 13
NrmMod |
47 | 2 | ad2antrr 762 |
. . . . . . . . . . . . 13
chr |
48 | | qsubcl 11807 |
. . . . . . . . . . . . . 14
|
49 | 22, 23, 48 | syl2anc 693 |
. . . . . . . . . . . . 13
|
50 | | qqhucn.z |
. . . . . . . . . . . . . 14
Mod |
51 | 17, 50 | qqhnm 30034 |
. . . . . . . . . . . . 13
NrmRing NrmMod chr QQHom |
52 | 44, 46, 47, 49, 51 | syl31anc 1329 |
. . . . . . . . . . . 12
QQHom |
53 | 21, 42, 52 | 3eqtrd 2660 |
. . . . . . . . . . 11
QQHomQQHom |
54 | 14, 16 | ovresd 6801 |
. . . . . . . . . . 11
QQHom QQHom QQHomQQHom |
55 | | qsscn 11799 |
. . . . . . . . . . . . . 14
|
56 | 55, 23 | sseldi 3601 |
. . . . . . . . . . . . 13
|
57 | 55, 22 | sseldi 3601 |
. . . . . . . . . . . . 13
|
58 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
59 | 58 | cnmetdval 22574 |
. . . . . . . . . . . . 13
|
60 | 56, 57, 59 | syl2anc 693 |
. . . . . . . . . . . 12
|
61 | 23, 22 | ovresd 6801 |
. . . . . . . . . . . 12
|
62 | 57, 56 | abssubd 14192 |
. . . . . . . . . . . 12
|
63 | 60, 61, 62 | 3eqtr4d 2666 |
. . . . . . . . . . 11
|
64 | 53, 54, 63 | 3eqtr4rd 2667 |
. . . . . . . . . 10
QQHom QQHom |
65 | 64 | breq1d 4663 |
. . . . . . . . 9
QQHom QQHom |
66 | 65 | biimpd 219 |
. . . . . . . 8
QQHom QQHom |
67 | 66 | ralrimiva 2966 |
. . . . . . 7
QQHom QQHom
|
68 | 67 | ralrimiva 2966 |
. . . . . 6
QQHom QQHom |
69 | 68 | adantr 481 |
. . . . 5
QQHom QQHom
|
70 | | breq2 4657 |
. . . . . . . 8
|
71 | 70 | imbi1d 331 |
. . . . . . 7
QQHom QQHom
QQHom QQHom
|
72 | 71 | 2ralbidv 2989 |
. . . . . 6
QQHom QQHom
QQHom QQHom
|
73 | 72 | rspcev 3309 |
. . . . 5
QQHom QQHom
QQHom QQHom
|
74 | 8, 69, 73 | syl2anc 693 |
. . . 4
QQHom QQHom
|
75 | 74 | ralrimiva 2966 |
. . 3
QQHom QQHom
|
76 | | eqid 2622 |
. . . 4
metUnif
metUnif
|
77 | | qqhucn.v |
. . . 4
metUnif
|
78 | | 0z 11388 |
. . . . . 6
|
79 | | zq 11794 |
. . . . . 6
|
80 | | ne0i 3921 |
. . . . . 6
|
81 | 78, 79, 80 | mp2b 10 |
. . . . 5
|
82 | 81 | a1i 11 |
. . . 4
|
83 | | drngring 18754 |
. . . . 5
|
84 | | eqid 2622 |
. . . . . 6
|
85 | 3, 84 | ringidcl 18568 |
. . . . 5
|
86 | | ne0i 3921 |
. . . . 5
|
87 | 1, 83, 85, 86 | 4syl 19 |
. . . 4
|
88 | | cnfldxms 22580 |
. . . . . . . 8
ℂfld |
89 | | qex 11800 |
. . . . . . . 8
|
90 | | ressxms 22330 |
. . . . . . . 8
ℂfld
ℂfld
↾s |
91 | 88, 89, 90 | mp2an 708 |
. . . . . . 7
ℂfld
↾s |
92 | 29, 91 | eqeltri 2697 |
. . . . . 6
|
93 | | cnfldds 19756 |
. . . . . . . . 9
ℂfld |
94 | 29, 93 | ressds 16073 |
. . . . . . . 8
|
95 | 89, 94 | ax-mp 5 |
. . . . . . 7
|
96 | 38, 95 | xmsxmet2 22264 |
. . . . . 6
|
97 | 92, 96 | mp1i 13 |
. . . . 5
|
98 | | xmetpsmet 22153 |
. . . . 5
PsMet |
99 | 97, 98 | syl 17 |
. . . 4
PsMet |
100 | | ngpxms 22405 |
. . . . . 6
NrmGrp |
101 | 3, 19 | xmsxmet2 22264 |
. . . . . 6
|
102 | 9, 10, 100, 101 | 4syl 19 |
. . . . 5
|
103 | | xmetpsmet 22153 |
. . . . 5
PsMet |
104 | 102, 103 | syl 17 |
. . . 4
PsMet |
105 | 76, 77, 82, 87, 99, 104 | metucn 22376 |
. . 3
QQHom metUnif
Cnu
QQHom
QQHom QQHom |
106 | 7, 75, 105 | mpbir2and 957 |
. 2
QQHom metUnif
Cnu |
107 | | qqhucn.u |
. . . . . 6
UnifSt |
108 | 29 | fveq2i 6194 |
. . . . . 6
UnifSt UnifStℂfld ↾s |
109 | | ressuss 22067 |
. . . . . . 7
UnifStℂfld ↾s UnifStℂfld
↾t |
110 | 89, 109 | ax-mp 5 |
. . . . . 6
UnifStℂfld ↾s UnifStℂfld
↾t |
111 | 107, 108,
110 | 3eqtri 2648 |
. . . . 5
UnifStℂfld
↾t |
112 | | eqid 2622 |
. . . . . . 7
UnifStℂfld UnifStℂfld |
113 | 112 | cnflduss 23152 |
. . . . . 6
UnifStℂfld metUnif |
114 | 113 | oveq1i 6660 |
. . . . 5
UnifStℂfld ↾t
metUnif ↾t |
115 | | cnxmet 22576 |
. . . . . . 7
|
116 | | xmetpsmet 22153 |
. . . . . . 7
PsMet |
117 | 115, 116 | ax-mp 5 |
. . . . . 6
PsMet |
118 | | restmetu 22375 |
. . . . . 6
PsMet
metUnif ↾t metUnif
|
119 | 81, 117, 55, 118 | mp3an 1424 |
. . . . 5
metUnif
↾t metUnif
|
120 | 111, 114,
119 | 3eqtri 2648 |
. . . 4
metUnif
|
121 | 120 | a1i 11 |
. . 3
metUnif
|
122 | 121 | oveq1d 6665 |
. 2
Cnu metUnif
Cnu |
123 | 106, 122 | eleqtrrd 2704 |
1
QQHom
Cnu |