Step | Hyp | Ref
| Expression |
1 | | reparpht.3 |
. . 3
|
2 | | reparpht.2 |
. . 3
|
3 | | cnco 21070 |
. . 3
|
4 | 1, 2, 3 | syl2anc 693 |
. 2
|
5 | | reparphti.6 |
. . 3
|
6 | | iitopon 22682 |
. . . . 5
TopOn |
7 | 6 | a1i 11 |
. . . 4
TopOn |
8 | | eqid 2622 |
. . . . . . . . . . 11
ℂfld ℂfld |
9 | 8 | cnfldtop 22587 |
. . . . . . . . . 10
ℂfld |
10 | | cnrest2r 21091 |
. . . . . . . . . 10
ℂfld ℂfld ↾t ℂfld |
11 | 9, 10 | mp1i 13 |
. . . . . . . . 9
ℂfld
↾t ℂfld |
12 | 7, 7 | cnmpt2nd 21472 |
. . . . . . . . . . 11
|
13 | | iirevcn 22729 |
. . . . . . . . . . . 12
|
14 | 13 | a1i 11 |
. . . . . . . . . . 11
|
15 | | oveq2 6658 |
. . . . . . . . . . 11
|
16 | 7, 7, 12, 7, 14, 15 | cnmpt21 21474 |
. . . . . . . . . 10
|
17 | 8 | dfii3 22686 |
. . . . . . . . . . 11
ℂfld
↾t |
18 | 17 | oveq2i 6661 |
. . . . . . . . . 10
ℂfld ↾t |
19 | 16, 18 | syl6eleq 2711 |
. . . . . . . . 9
ℂfld ↾t |
20 | 11, 19 | sseldd 3604 |
. . . . . . . 8
ℂfld |
21 | 7, 7 | cnmpt1st 21471 |
. . . . . . . . . . 11
|
22 | 7, 7, 21, 1 | cnmpt21f 21475 |
. . . . . . . . . 10
|
23 | 22, 18 | syl6eleq 2711 |
. . . . . . . . 9
ℂfld ↾t |
24 | 11, 23 | sseldd 3604 |
. . . . . . . 8
ℂfld |
25 | 8 | mulcn 22670 |
. . . . . . . . 9
ℂfld ℂfld ℂfld |
26 | 25 | a1i 11 |
. . . . . . . 8
ℂfld
ℂfld ℂfld |
27 | 7, 7, 20, 24, 26 | cnmpt22f 21478 |
. . . . . . 7
ℂfld |
28 | 12, 18 | syl6eleq 2711 |
. . . . . . . . 9
ℂfld ↾t |
29 | 11, 28 | sseldd 3604 |
. . . . . . . 8
ℂfld |
30 | 21, 18 | syl6eleq 2711 |
. . . . . . . . 9
ℂfld ↾t |
31 | 11, 30 | sseldd 3604 |
. . . . . . . 8
ℂfld |
32 | 7, 7, 29, 31, 26 | cnmpt22f 21478 |
. . . . . . 7
ℂfld |
33 | 8 | addcn 22668 |
. . . . . . . 8
ℂfld ℂfld ℂfld |
34 | 33 | a1i 11 |
. . . . . . 7
ℂfld
ℂfld ℂfld |
35 | 7, 7, 27, 32, 34 | cnmpt22f 21478 |
. . . . . 6
ℂfld |
36 | 8 | cnfldtopon 22586 |
. . . . . . . 8
ℂfld TopOn |
37 | 36 | a1i 11 |
. . . . . . 7
ℂfld
TopOn |
38 | | iiuni 22684 |
. . . . . . . . . . . . . . 15
|
39 | 38, 38 | cnf 21050 |
. . . . . . . . . . . . . 14
|
40 | 1, 39 | syl 17 |
. . . . . . . . . . . . 13
|
41 | 40 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
42 | 41 | adantrr 753 |
. . . . . . . . . . 11
|
43 | | simprl 794 |
. . . . . . . . . . 11
|
44 | | simprr 796 |
. . . . . . . . . . 11
|
45 | | 0re 10040 |
. . . . . . . . . . . 12
|
46 | | 1re 10039 |
. . . . . . . . . . . 12
|
47 | | icccvx 22749 |
. . . . . . . . . . . 12
|
48 | 45, 46, 47 | mp2an 708 |
. . . . . . . . . . 11
|
49 | 42, 43, 44, 48 | syl3anc 1326 |
. . . . . . . . . 10
|
50 | 49 | ralrimivva 2971 |
. . . . . . . . 9
|
51 | | eqid 2622 |
. . . . . . . . . 10
|
52 | 51 | fmpt2 7237 |
. . . . . . . . 9
|
53 | 50, 52 | sylib 208 |
. . . . . . . 8
|
54 | | frn 6053 |
. . . . . . . 8
|
55 | 53, 54 | syl 17 |
. . . . . . 7
|
56 | | unitssre 12319 |
. . . . . . . . 9
|
57 | | ax-resscn 9993 |
. . . . . . . . 9
|
58 | 56, 57 | sstri 3612 |
. . . . . . . 8
|
59 | 58 | a1i 11 |
. . . . . . 7
|
60 | | cnrest2 21090 |
. . . . . . 7
ℂfld
TopOn
ℂfld
ℂfld
↾t |
61 | 37, 55, 59, 60 | syl3anc 1326 |
. . . . . 6
ℂfld
ℂfld
↾t |
62 | 35, 61 | mpbid 222 |
. . . . 5
ℂfld ↾t |
63 | 62, 18 | syl6eleqr 2712 |
. . . 4
|
64 | 7, 7, 63, 2 | cnmpt21f 21475 |
. . 3
|
65 | 5, 64 | syl5eqel 2705 |
. 2
|
66 | 40 | ffvelrnda 6359 |
. . . . . . . 8
|
67 | 58, 66 | sseldi 3601 |
. . . . . . 7
|
68 | 67 | mulid2d 10058 |
. . . . . 6
|
69 | 58 | sseli 3599 |
. . . . . . . 8
|
70 | 69 | adantl 482 |
. . . . . . 7
|
71 | 70 | mul02d 10234 |
. . . . . 6
|
72 | 68, 71 | oveq12d 6668 |
. . . . 5
|
73 | 67 | addid1d 10236 |
. . . . 5
|
74 | 72, 73 | eqtrd 2656 |
. . . 4
|
75 | 74 | fveq2d 6195 |
. . 3
|
76 | | simpr 477 |
. . . 4
|
77 | | 0elunit 12290 |
. . . 4
|
78 | | simpr 477 |
. . . . . . . . . 10
|
79 | 78 | oveq2d 6666 |
. . . . . . . . 9
|
80 | | 1m0e1 11131 |
. . . . . . . . 9
|
81 | 79, 80 | syl6eq 2672 |
. . . . . . . 8
|
82 | | simpl 473 |
. . . . . . . . 9
|
83 | 82 | fveq2d 6195 |
. . . . . . . 8
|
84 | 81, 83 | oveq12d 6668 |
. . . . . . 7
|
85 | 78, 82 | oveq12d 6668 |
. . . . . . 7
|
86 | 84, 85 | oveq12d 6668 |
. . . . . 6
|
87 | 86 | fveq2d 6195 |
. . . . 5
|
88 | | fvex 6201 |
. . . . 5
|
89 | 87, 5, 88 | ovmpt2a 6791 |
. . . 4
|
90 | 76, 77, 89 | sylancl 694 |
. . 3
|
91 | | fvco3 6275 |
. . . 4
|
92 | 40, 91 | sylan 488 |
. . 3
|
93 | 75, 90, 92 | 3eqtr4d 2666 |
. 2
|
94 | | 1elunit 12291 |
. . . 4
|
95 | | simpr 477 |
. . . . . . . . . 10
|
96 | 95 | oveq2d 6666 |
. . . . . . . . 9
|
97 | | 1m1e0 11089 |
. . . . . . . . 9
|
98 | 96, 97 | syl6eq 2672 |
. . . . . . . 8
|
99 | | simpl 473 |
. . . . . . . . 9
|
100 | 99 | fveq2d 6195 |
. . . . . . . 8
|
101 | 98, 100 | oveq12d 6668 |
. . . . . . 7
|
102 | 95, 99 | oveq12d 6668 |
. . . . . . 7
|
103 | 101, 102 | oveq12d 6668 |
. . . . . 6
|
104 | 103 | fveq2d 6195 |
. . . . 5
|
105 | | fvex 6201 |
. . . . 5
|
106 | 104, 5, 105 | ovmpt2a 6791 |
. . . 4
|
107 | 76, 94, 106 | sylancl 694 |
. . 3
|
108 | 67 | mul02d 10234 |
. . . . . 6
|
109 | 70 | mulid2d 10058 |
. . . . . 6
|
110 | 108, 109 | oveq12d 6668 |
. . . . 5
|
111 | 70 | addid2d 10237 |
. . . . 5
|
112 | 110, 111 | eqtrd 2656 |
. . . 4
|
113 | 112 | fveq2d 6195 |
. . 3
|
114 | 107, 113 | eqtrd 2656 |
. 2
|
115 | | reparpht.4 |
. . . . . . . . 9
|
116 | 115 | adantr 481 |
. . . . . . . 8
|
117 | 116 | oveq2d 6666 |
. . . . . . 7
|
118 | | ax-1cn 9994 |
. . . . . . . . 9
|
119 | | subcl 10280 |
. . . . . . . . 9
|
120 | 118, 70, 119 | sylancr 695 |
. . . . . . . 8
|
121 | 120 | mul01d 10235 |
. . . . . . 7
|
122 | 117, 121 | eqtrd 2656 |
. . . . . 6
|
123 | 70 | mul01d 10235 |
. . . . . 6
|
124 | 122, 123 | oveq12d 6668 |
. . . . 5
|
125 | | 00id 10211 |
. . . . 5
|
126 | 124, 125 | syl6eq 2672 |
. . . 4
|
127 | 126 | fveq2d 6195 |
. . 3
|
128 | | simpr 477 |
. . . . . . . . 9
|
129 | 128 | oveq2d 6666 |
. . . . . . . 8
|
130 | | simpl 473 |
. . . . . . . . 9
|
131 | 130 | fveq2d 6195 |
. . . . . . . 8
|
132 | 129, 131 | oveq12d 6668 |
. . . . . . 7
|
133 | 128, 130 | oveq12d 6668 |
. . . . . . 7
|
134 | 132, 133 | oveq12d 6668 |
. . . . . 6
|
135 | 134 | fveq2d 6195 |
. . . . 5
|
136 | | fvex 6201 |
. . . . 5
|
137 | 135, 5, 136 | ovmpt2a 6791 |
. . . 4
|
138 | 77, 76, 137 | sylancr 695 |
. . 3
|
139 | | fvco3 6275 |
. . . . . 6
|
140 | 40, 77, 139 | sylancl 694 |
. . . . 5
|
141 | 115 | fveq2d 6195 |
. . . . 5
|
142 | 140, 141 | eqtrd 2656 |
. . . 4
|
143 | 142 | adantr 481 |
. . 3
|
144 | 127, 138,
143 | 3eqtr4d 2666 |
. 2
|
145 | | reparpht.5 |
. . . . . . . . 9
|
146 | 145 | adantr 481 |
. . . . . . . 8
|
147 | 146 | oveq2d 6666 |
. . . . . . 7
|
148 | 120 | mulid1d 10057 |
. . . . . . 7
|
149 | 147, 148 | eqtrd 2656 |
. . . . . 6
|
150 | 70 | mulid1d 10057 |
. . . . . 6
|
151 | 149, 150 | oveq12d 6668 |
. . . . 5
|
152 | | npcan 10290 |
. . . . . 6
|
153 | 118, 70, 152 | sylancr 695 |
. . . . 5
|
154 | 151, 153 | eqtrd 2656 |
. . . 4
|
155 | 154 | fveq2d 6195 |
. . 3
|
156 | | simpr 477 |
. . . . . . . . 9
|
157 | 156 | oveq2d 6666 |
. . . . . . . 8
|
158 | | simpl 473 |
. . . . . . . . 9
|
159 | 158 | fveq2d 6195 |
. . . . . . . 8
|
160 | 157, 159 | oveq12d 6668 |
. . . . . . 7
|
161 | 156, 158 | oveq12d 6668 |
. . . . . . 7
|
162 | 160, 161 | oveq12d 6668 |
. . . . . 6
|
163 | 162 | fveq2d 6195 |
. . . . 5
|
164 | | fvex 6201 |
. . . . 5
|
165 | 163, 5, 164 | ovmpt2a 6791 |
. . . 4
|
166 | 94, 76, 165 | sylancr 695 |
. . 3
|
167 | | fvco3 6275 |
. . . . . 6
|
168 | 40, 94, 167 | sylancl 694 |
. . . . 5
|
169 | 145 | fveq2d 6195 |
. . . . 5
|
170 | 168, 169 | eqtrd 2656 |
. . . 4
|
171 | 170 | adantr 481 |
. . 3
|
172 | 155, 166,
171 | 3eqtr4d 2666 |
. 2
|
173 | 4, 2, 65, 93, 114, 144, 172 | isphtpy2d 22786 |
1
|