Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  reparphti Unicode version

Theorem reparphti 18511
 Description: Lemma for reparpht 18512. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.)
Hypotheses
Ref Expression
reparpht.2
reparpht.3
reparpht.4
reparpht.5
reparphti.6
Assertion
Ref Expression
reparphti
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem reparphti
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reparpht.3 . . 3
2 reparpht.2 . . 3
3 cnco 17011 . . 3
41, 2, 3syl2anc 642 . 2
5 reparphti.6 . . 3
6 iitopon 18399 . . . . 5 TopOn
76a1i 10 . . . 4 TopOn
8 eqid 2296 . . . . . . . . . . 11 fld fld
98cnfldtop 18309 . . . . . . . . . 10 fld
10 cnrest2r 17031 . . . . . . . . . 10 fld fldt fld
119, 10mp1i 11 . . . . . . . . 9 fldt fld
127, 7cnmpt2nd 17379 . . . . . . . . . . 11
13 iirevcn 18444 . . . . . . . . . . . 12
1413a1i 10 . . . . . . . . . . 11
15 oveq2 5882 . . . . . . . . . . 11
167, 7, 12, 7, 14, 15cnmpt21 17381 . . . . . . . . . 10
178dfii3 18403 . . . . . . . . . . 11 fldt
1817oveq2i 5885 . . . . . . . . . 10 fldt
1916, 18syl6eleq 2386 . . . . . . . . 9 fldt
2011, 19sseldd 3194 . . . . . . . 8 fld
217, 7cnmpt1st 17378 . . . . . . . . . . 11
227, 7, 21, 1cnmpt21f 17382 . . . . . . . . . 10
2322, 18syl6eleq 2386 . . . . . . . . 9 fldt
2411, 23sseldd 3194 . . . . . . . 8 fld
258mulcn 18387 . . . . . . . . 9 fld fld fld
2625a1i 10 . . . . . . . 8 fld fld fld
277, 7, 20, 24, 26cnmpt22f 17385 . . . . . . 7 fld
2812, 18syl6eleq 2386 . . . . . . . . 9 fldt
2911, 28sseldd 3194 . . . . . . . 8 fld
3021, 18syl6eleq 2386 . . . . . . . . 9 fldt
3111, 30sseldd 3194 . . . . . . . 8 fld
327, 7, 29, 31, 26cnmpt22f 17385 . . . . . . 7 fld
338addcn 18385 . . . . . . . 8 fld fld fld
3433a1i 10 . . . . . . 7 fld fld fld
357, 7, 27, 32, 34cnmpt22f 17385 . . . . . 6 fld
368cnfldtopon 18308 . . . . . . . 8 fld TopOn
3736a1i 10 . . . . . . 7 fld TopOn
38 iiuni 18401 . . . . . . . . . . . . . . 15
3938, 38cnf 16992 . . . . . . . . . . . . . 14
401, 39syl 15 . . . . . . . . . . . . 13
41 ffvelrn 5679 . . . . . . . . . . . . 13
4240, 41sylan 457 . . . . . . . . . . . 12
4342adantrr 697 . . . . . . . . . . 11
44 simprl 732 . . . . . . . . . . 11
45 simprr 733 . . . . . . . . . . 11
46 0re 8854 . . . . . . . . . . . 12
47 1re 8853 . . . . . . . . . . . 12
48 icccvx 18464 . . . . . . . . . . . 12
4946, 47, 48mp2an 653 . . . . . . . . . . 11
5043, 44, 45, 49syl3anc 1182 . . . . . . . . . 10
5150ralrimivva 2648 . . . . . . . . 9
52 eqid 2296 . . . . . . . . . 10
5352fmpt2 6207 . . . . . . . . 9
5451, 53sylib 188 . . . . . . . 8
55 frn 5411 . . . . . . . 8
5654, 55syl 15 . . . . . . 7
57 iccssre 10747 . . . . . . . . . 10
5846, 47, 57mp2an 653 . . . . . . . . 9
59 ax-resscn 8810 . . . . . . . . 9
6058, 59sstri 3201 . . . . . . . 8
6160a1i 10 . . . . . . 7
62 cnrest2 17030 . . . . . . 7 fld TopOn fld fldt
6337, 56, 61, 62syl3anc 1182 . . . . . 6 fld fldt
6435, 63mpbid 201 . . . . 5 fldt
6564, 18syl6eleqr 2387 . . . 4
667, 7, 65, 2cnmpt21f 17382 . . 3
675, 66syl5eqel 2380 . 2
68 ffvelrn 5679 . . . . . . . . 9
6940, 68sylan 457 . . . . . . . 8
7060, 69sseldi 3191 . . . . . . 7
7170mulid2d 8869 . . . . . 6
7260sseli 3189 . . . . . . . 8
7372adantl 452 . . . . . . 7
7473mul02d 9026 . . . . . 6
7571, 74oveq12d 5892 . . . . 5
7670addid1d 9028 . . . . 5
7775, 76eqtrd 2328 . . . 4
7877fveq2d 5545 . . 3
79 simpr 447 . . . 4
80 0elunit 10770 . . . 4
81 simpr 447 . . . . . . . . . 10
8281oveq2d 5890 . . . . . . . . 9
83 ax-1cn 8811 . . . . . . . . . 10
8483subid1i 9134 . . . . . . . . 9
8582, 84syl6eq 2344 . . . . . . . 8
86 simpl 443 . . . . . . . . 9
8786fveq2d 5545 . . . . . . . 8
8885, 87oveq12d 5892 . . . . . . 7
8981, 86oveq12d 5892 . . . . . . 7
9088, 89oveq12d 5892 . . . . . 6
9190fveq2d 5545 . . . . 5
92 fvex 5555 . . . . 5
9391, 5, 92ovmpt2a 5994 . . . 4
9479, 80, 93sylancl 643 . . 3
95 fvco3 5612 . . . 4
9640, 95sylan 457 . . 3
9778, 94, 963eqtr4d 2338 . 2
98 1elunit 10771 . . . 4
99 simpr 447 . . . . . . . . . 10
10099oveq2d 5890 . . . . . . . . 9
101 1m1e0 9830 . . . . . . . . 9
102100, 101syl6eq 2344 . . . . . . . 8
103 simpl 443 . . . . . . . . 9
104103fveq2d 5545 . . . . . . . 8
105102, 104oveq12d 5892 . . . . . . 7
10699, 103oveq12d 5892 . . . . . . 7
107105, 106oveq12d 5892 . . . . . 6
108107fveq2d 5545 . . . . 5
109 fvex 5555 . . . . 5
110108, 5, 109ovmpt2a 5994 . . . 4
11179, 98, 110sylancl 643 . . 3
11270mul02d 9026 . . . . . 6
11373mulid2d 8869 . . . . . 6
114112, 113oveq12d 5892 . . . . 5
11573addid2d 9029 . . . . 5
116114, 115eqtrd 2328 . . . 4
117116fveq2d 5545 . . 3
118111, 117eqtrd 2328 . 2
119 reparpht.4 . . . . . . . . 9
120119adantr 451 . . . . . . . 8
121120oveq2d 5890 . . . . . . 7
122 subcl 9067 . . . . . . . . 9
12383, 73, 122sylancr 644 . . . . . . . 8
124123mul01d 9027 . . . . . . 7
125121, 124eqtrd 2328 . . . . . 6
12673mul01d 9027 . . . . . 6
127125, 126oveq12d 5892 . . . . 5
128 00id 9003 . . . . 5
129127, 128syl6eq 2344 . . . 4
130129fveq2d 5545 . . 3
131 simpr 447 . . . . . . . . 9
132131oveq2d 5890 . . . . . . . 8
133 simpl 443 . . . . . . . . 9
134133fveq2d 5545 . . . . . . . 8
135132, 134oveq12d 5892 . . . . . . 7
136131, 133oveq12d 5892 . . . . . . 7
137135, 136oveq12d 5892 . . . . . 6
138137fveq2d 5545 . . . . 5
139 fvex 5555 . . . . 5
140138, 5, 139ovmpt2a 5994 . . . 4
14180, 79, 140sylancr 644 . . 3
142 fvco3 5612 . . . . . 6
14340, 80, 142sylancl 643 . . . . 5
144119fveq2d 5545 . . . . 5
145143, 144eqtrd 2328 . . . 4
147130, 141, 1463eqtr4d 2338 . 2
148 reparpht.5 . . . . . . . . 9
149148adantr 451 . . . . . . . 8
150149oveq2d 5890 . . . . . . 7
151123mulid1d 8868 . . . . . . 7
152150, 151eqtrd 2328 . . . . . 6
15373mulid1d 8868 . . . . . 6
154152, 153oveq12d 5892 . . . . 5
155 npcan 9076 . . . . . 6
15683, 73, 155sylancr 644 . . . . 5
157154, 156eqtrd 2328 . . . 4
158157fveq2d 5545 . . 3
159 simpr 447 . . . . . . . . 9
160159oveq2d 5890 . . . . . . . 8
161 simpl 443 . . . . . . . . 9
162161fveq2d 5545 . . . . . . . 8
163160, 162oveq12d 5892 . . . . . . 7
164159, 161oveq12d 5892 . . . . . . 7
165163, 164oveq12d 5892 . . . . . 6
166165fveq2d 5545 . . . . 5
167 fvex 5555 . . . . 5
168166, 5, 167ovmpt2a 5994 . . . 4
16998, 79, 168sylancr 644 . . 3
170 fvco3 5612 . . . . . 6
17140, 98, 170sylancl 643 . . . . 5
172148fveq2d 5545 . . . . 5
173171, 172eqtrd 2328 . . . 4