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

Theorem reparphti 19014
 Description: Lemma for reparpht 19015. (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 17322 . . 3
41, 2, 3syl2anc 643 . 2
5 reparphti.6 . . 3
6 iitopon 18901 . . . . 5 TopOn
76a1i 11 . . . 4 TopOn
8 eqid 2435 . . . . . . . . . . 11 fld fld
98cnfldtop 18810 . . . . . . . . . 10 fld
10 cnrest2r 17343 . . . . . . . . . 10 fld fldt fld
119, 10mp1i 12 . . . . . . . . 9 fldt fld
127, 7cnmpt2nd 17693 . . . . . . . . . . 11
13 iirevcn 18947 . . . . . . . . . . . 12
1413a1i 11 . . . . . . . . . . 11
15 oveq2 6081 . . . . . . . . . . 11
167, 7, 12, 7, 14, 15cnmpt21 17695 . . . . . . . . . 10
178dfii3 18905 . . . . . . . . . . 11 fldt
1817oveq2i 6084 . . . . . . . . . 10 fldt
1916, 18syl6eleq 2525 . . . . . . . . 9 fldt
2011, 19sseldd 3341 . . . . . . . 8 fld
217, 7cnmpt1st 17692 . . . . . . . . . . 11
227, 7, 21, 1cnmpt21f 17696 . . . . . . . . . 10
2322, 18syl6eleq 2525 . . . . . . . . 9 fldt
2411, 23sseldd 3341 . . . . . . . 8 fld
258mulcn 18889 . . . . . . . . 9 fld fld fld
2625a1i 11 . . . . . . . 8 fld fld fld
277, 7, 20, 24, 26cnmpt22f 17699 . . . . . . 7 fld
2812, 18syl6eleq 2525 . . . . . . . . 9 fldt
2911, 28sseldd 3341 . . . . . . . 8 fld
3021, 18syl6eleq 2525 . . . . . . . . 9 fldt
3111, 30sseldd 3341 . . . . . . . 8 fld
327, 7, 29, 31, 26cnmpt22f 17699 . . . . . . 7 fld
338addcn 18887 . . . . . . . 8 fld fld fld
3433a1i 11 . . . . . . 7 fld fld fld
357, 7, 27, 32, 34cnmpt22f 17699 . . . . . 6 fld
368cnfldtopon 18809 . . . . . . . 8 fld TopOn
3736a1i 11 . . . . . . 7 fld TopOn
38 iiuni 18903 . . . . . . . . . . . . . . 15
3938, 38cnf 17302 . . . . . . . . . . . . . 14
401, 39syl 16 . . . . . . . . . . . . 13
4140ffvelrnda 5862 . . . . . . . . . . . 12
4241adantrr 698 . . . . . . . . . . 11
43 simprl 733 . . . . . . . . . . 11
44 simprr 734 . . . . . . . . . . 11
45 0re 9083 . . . . . . . . . . . 12
46 1re 9082 . . . . . . . . . . . 12
47 icccvx 18967 . . . . . . . . . . . 12
4845, 46, 47mp2an 654 . . . . . . . . . . 11
4942, 43, 44, 48syl3anc 1184 . . . . . . . . . 10
5049ralrimivva 2790 . . . . . . . . 9
51 eqid 2435 . . . . . . . . . 10
5251fmpt2 6410 . . . . . . . . 9
5350, 52sylib 189 . . . . . . . 8
54 frn 5589 . . . . . . . 8
5553, 54syl 16 . . . . . . 7
56 unitssre 11034 . . . . . . . . 9
57 ax-resscn 9039 . . . . . . . . 9
5856, 57sstri 3349 . . . . . . . 8
5958a1i 11 . . . . . . 7
60 cnrest2 17342 . . . . . . 7 fld TopOn fld fldt
6137, 55, 59, 60syl3anc 1184 . . . . . 6 fld fldt
6235, 61mpbid 202 . . . . 5 fldt
6362, 18syl6eleqr 2526 . . . 4
647, 7, 63, 2cnmpt21f 17696 . . 3
655, 64syl5eqel 2519 . 2
6640ffvelrnda 5862 . . . . . . . 8
6758, 66sseldi 3338 . . . . . . 7
6867mulid2d 9098 . . . . . 6
6958sseli 3336 . . . . . . . 8
7069adantl 453 . . . . . . 7
7170mul02d 9256 . . . . . 6
7268, 71oveq12d 6091 . . . . 5
7367addid1d 9258 . . . . 5
7472, 73eqtrd 2467 . . . 4
7574fveq2d 5724 . . 3
76 simpr 448 . . . 4
77 0elunit 11007 . . . 4
78 simpr 448 . . . . . . . . . 10
7978oveq2d 6089 . . . . . . . . 9
80 ax-1cn 9040 . . . . . . . . . 10
8180subid1i 9364 . . . . . . . . 9
8279, 81syl6eq 2483 . . . . . . . 8
83 simpl 444 . . . . . . . . 9
8483fveq2d 5724 . . . . . . . 8
8582, 84oveq12d 6091 . . . . . . 7
8678, 83oveq12d 6091 . . . . . . 7
8785, 86oveq12d 6091 . . . . . 6
8887fveq2d 5724 . . . . 5
89 fvex 5734 . . . . 5
9088, 5, 89ovmpt2a 6196 . . . 4
9176, 77, 90sylancl 644 . . 3
92 fvco3 5792 . . . 4
9340, 92sylan 458 . . 3
9475, 91, 933eqtr4d 2477 . 2
95 1elunit 11008 . . . 4
96 simpr 448 . . . . . . . . . 10
9796oveq2d 6089 . . . . . . . . 9
98 1m1e0 10060 . . . . . . . . 9
9997, 98syl6eq 2483 . . . . . . . 8
100 simpl 444 . . . . . . . . 9
101100fveq2d 5724 . . . . . . . 8
10299, 101oveq12d 6091 . . . . . . 7
10396, 100oveq12d 6091 . . . . . . 7
104102, 103oveq12d 6091 . . . . . 6
105104fveq2d 5724 . . . . 5
106 fvex 5734 . . . . 5
107105, 5, 106ovmpt2a 6196 . . . 4
10876, 95, 107sylancl 644 . . 3
10967mul02d 9256 . . . . . 6
11070mulid2d 9098 . . . . . 6
111109, 110oveq12d 6091 . . . . 5
11270addid2d 9259 . . . . 5
113111, 112eqtrd 2467 . . . 4
114113fveq2d 5724 . . 3
115108, 114eqtrd 2467 . 2
116 reparpht.4 . . . . . . . . 9
117116adantr 452 . . . . . . . 8
118117oveq2d 6089 . . . . . . 7
119 subcl 9297 . . . . . . . . 9
12080, 70, 119sylancr 645 . . . . . . . 8
121120mul01d 9257 . . . . . . 7
122118, 121eqtrd 2467 . . . . . 6
12370mul01d 9257 . . . . . 6
124122, 123oveq12d 6091 . . . . 5
125 00id 9233 . . . . 5
126124, 125syl6eq 2483 . . . 4
127126fveq2d 5724 . . 3
128 simpr 448 . . . . . . . . 9
129128oveq2d 6089 . . . . . . . 8
130 simpl 444 . . . . . . . . 9
131130fveq2d 5724 . . . . . . . 8
132129, 131oveq12d 6091 . . . . . . 7
133128, 130oveq12d 6091 . . . . . . 7
134132, 133oveq12d 6091 . . . . . 6
135134fveq2d 5724 . . . . 5
136 fvex 5734 . . . . 5
137135, 5, 136ovmpt2a 6196 . . . 4
13877, 76, 137sylancr 645 . . 3
139 fvco3 5792 . . . . . 6
14040, 77, 139sylancl 644 . . . . 5
141116fveq2d 5724 . . . . 5
142140, 141eqtrd 2467 . . . 4
144127, 138, 1433eqtr4d 2477 . 2
145 reparpht.5 . . . . . . . . 9
146145adantr 452 . . . . . . . 8
147146oveq2d 6089 . . . . . . 7
148120mulid1d 9097 . . . . . . 7
149147, 148eqtrd 2467 . . . . . 6
15070mulid1d 9097 . . . . . 6
151149, 150oveq12d 6091 . . . . 5
152 npcan 9306 . . . . . 6
15380, 70, 152sylancr 645 . . . . 5
154151, 153eqtrd 2467 . . . 4
155154fveq2d 5724 . . 3
156 simpr 448 . . . . . . . . 9
157156oveq2d 6089 . . . . . . . 8
158 simpl 444 . . . . . . . . 9
159158fveq2d 5724 . . . . . . . 8
160157, 159oveq12d 6091 . . . . . . 7
161156, 158oveq12d 6091 . . . . . . 7
162160, 161oveq12d 6091 . . . . . 6
163162fveq2d 5724 . . . . 5
164 fvex 5734 . . . . 5
165163, 5, 164ovmpt2a 6196 . . . 4
16695, 76, 165sylancr 645 . . 3
167 fvco3 5792 . . . . . 6
16840, 95, 167sylancl 644 . . . . 5
169145fveq2d 5724 . . . . 5
170168, 169eqtrd 2467 . . . 4