Metamath Proof Explorer


Theorem dvcnvrelem1

Description: Lemma for dvcnvre . (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses dvcnvre.f φ F : X cn
dvcnvre.d φ dom F = X
dvcnvre.z φ ¬ 0 ran F
dvcnvre.1 φ F : X 1-1 onto Y
dvcnvre.c φ C X
dvcnvre.r φ R +
dvcnvre.s φ C R C + R X
Assertion dvcnvrelem1 φ F C int topGen ran . F C R C + R

Proof

Step Hyp Ref Expression
1 dvcnvre.f φ F : X cn
2 dvcnvre.d φ dom F = X
3 dvcnvre.z φ ¬ 0 ran F
4 dvcnvre.1 φ F : X 1-1 onto Y
5 dvcnvre.c φ C X
6 dvcnvre.r φ R +
7 dvcnvre.s φ C R C + R X
8 dvbsss dom F
9 2 8 eqsstrrdi φ X
10 9 5 sseldd φ C
11 6 rpred φ R
12 10 11 resubcld φ C R
13 10 11 readdcld φ C + R
14 10 6 ltsubrpd φ C R < C
15 10 6 ltaddrpd φ C < C + R
16 12 10 13 14 15 lttrd φ C R < C + R
17 12 13 16 ltled φ C R C + R
18 rescncf C R C + R X F : X cn F C R C + R : C R C + R cn
19 7 1 18 sylc φ F C R C + R : C R C + R cn
20 12 13 17 19 evthicc2 φ x y ran F C R C + R = x y
21 cncff F : X cn F : X
22 1 21 syl φ F : X
23 22 5 ffvelrnd φ F C
24 23 adantr φ x y ran F C R C + R = x y F C
25 12 rexrd φ C R *
26 13 rexrd φ C + R *
27 lbicc2 C R * C + R * C R C + R C R C R C + R
28 25 26 17 27 syl3anc φ C R C R C + R
29 28 adantr φ x y ran F C R C + R = x y C R C R C + R
30 12 10 14 ltled φ C R C
31 10 13 15 ltled φ C C + R
32 elicc2 C R C + R C C R C + R C C R C C C + R
33 12 13 32 syl2anc φ C C R C + R C C R C C C + R
34 10 30 31 33 mpbir3and φ C C R C + R
35 34 adantr φ x y ran F C R C + R = x y C C R C + R
36 14 adantr φ x y ran F C R C + R = x y C R < C
37 isorel F C R C + R Isom < , < C R C + R ran F C R C + R C R C R C + R C C R C + R C R < C F C R C + R C R < F C R C + R C
38 37 biimpd F C R C + R Isom < , < C R C + R ran F C R C + R C R C R C + R C C R C + R C R < C F C R C + R C R < F C R C + R C
39 38 exp32 F C R C + R Isom < , < C R C + R ran F C R C + R C R C R C + R C C R C + R C R < C F C R C + R C R < F C R C + R C
40 39 com4l C R C R C + R C C R C + R C R < C F C R C + R Isom < , < C R C + R ran F C R C + R F C R C + R C R < F C R C + R C
41 29 35 36 40 syl3c φ x y ran F C R C + R = x y F C R C + R Isom < , < C R C + R ran F C R C + R F C R C + R C R < F C R C + R C
42 29 fvresd φ x y ran F C R C + R = x y F C R C + R C R = F C R
43 35 fvresd φ x y ran F C R C + R = x y F C R C + R C = F C
44 42 43 breq12d φ x y ran F C R C + R = x y F C R C + R C R < F C R C + R C F C R < F C
45 41 44 sylibd φ x y ran F C R C + R = x y F C R C + R Isom < , < C R C + R ran F C R C + R F C R < F C
46 22 adantr φ x y ran F C R C + R = x y F : X
47 46 ffund φ x y ran F C R C + R = x y Fun F
48 7 adantr φ x y ran F C R C + R = x y C R C + R X
49 46 fdmd φ x y ran F C R C + R = x y dom F = X
50 48 49 sseqtrrd φ x y ran F C R C + R = x y C R C + R dom F
51 funfvima2 Fun F C R C + R dom F C R C R C + R F C R F C R C + R
52 47 50 51 syl2anc φ x y ran F C R C + R = x y C R C R C + R F C R F C R C + R
53 29 52 mpd φ x y ran F C R C + R = x y F C R F C R C + R
54 df-ima F C R C + R = ran F C R C + R
55 simprr φ x y ran F C R C + R = x y ran F C R C + R = x y
56 54 55 eqtrid φ x y ran F C R C + R = x y F C R C + R = x y
57 53 56 eleqtrd φ x y ran F C R C + R = x y F C R x y
58 elicc2 x y F C R x y F C R x F C R F C R y
59 58 ad2antrl φ x y ran F C R C + R = x y F C R x y F C R x F C R F C R y
60 57 59 mpbid φ x y ran F C R C + R = x y F C R x F C R F C R y
61 60 simp2d φ x y ran F C R C + R = x y x F C R
62 simprll φ x y ran F C R C + R = x y x
63 7 28 sseldd φ C R X
64 22 63 ffvelrnd φ F C R
65 64 adantr φ x y ran F C R C + R = x y F C R
66 lelttr x F C R F C x F C R F C R < F C x < F C
67 62 65 24 66 syl3anc φ x y ran F C R C + R = x y x F C R F C R < F C x < F C
68 61 67 mpand φ x y ran F C R C + R = x y F C R < F C x < F C
69 45 68 syld φ x y ran F C R C + R = x y F C R C + R Isom < , < C R C + R ran F C R C + R x < F C
70 ubicc2 C R * C + R * C R C + R C + R C R C + R
71 25 26 17 70 syl3anc φ C + R C R C + R
72 71 adantr φ x y ran F C R C + R = x y C + R C R C + R
73 15 adantr φ x y ran F C R C + R = x y C < C + R
74 isorel F C R C + R Isom < , < -1 C R C + R ran F C R C + R C C R C + R C + R C R C + R C < C + R F C R C + R C < -1 F C R C + R C + R
75 74 biimpd F C R C + R Isom < , < -1 C R C + R ran F C R C + R C C R C + R C + R C R C + R C < C + R F C R C + R C < -1 F C R C + R C + R
76 75 exp32 F C R C + R Isom < , < -1 C R C + R ran F C R C + R C C R C + R C + R C R C + R C < C + R F C R C + R C < -1 F C R C + R C + R
77 76 com4l C C R C + R C + R C R C + R C < C + R F C R C + R Isom < , < -1 C R C + R ran F C R C + R F C R C + R C < -1 F C R C + R C + R
78 35 72 73 77 syl3c φ x y ran F C R C + R = x y F C R C + R Isom < , < -1 C R C + R ran F C R C + R F C R C + R C < -1 F C R C + R C + R
79 fvex F C R C + R C V
80 fvex F C R C + R C + R V
81 79 80 brcnv F C R C + R C < -1 F C R C + R C + R F C R C + R C + R < F C R C + R C
82 72 fvresd φ x y ran F C R C + R = x y F C R C + R C + R = F C + R
83 82 43 breq12d φ x y ran F C R C + R = x y F C R C + R C + R < F C R C + R C F C + R < F C
84 81 83 syl5bb φ x y ran F C R C + R = x y F C R C + R C < -1 F C R C + R C + R F C + R < F C
85 78 84 sylibd φ x y ran F C R C + R = x y F C R C + R Isom < , < -1 C R C + R ran F C R C + R F C + R < F C
86 funfvima2 Fun F C R C + R dom F C + R C R C + R F C + R F C R C + R
87 47 50 86 syl2anc φ x y ran F C R C + R = x y C + R C R C + R F C + R F C R C + R
88 72 87 mpd φ x y ran F C R C + R = x y F C + R F C R C + R
89 88 56 eleqtrd φ x y ran F C R C + R = x y F C + R x y
90 elicc2 x y F C + R x y F C + R x F C + R F C + R y
91 90 ad2antrl φ x y ran F C R C + R = x y F C + R x y F C + R x F C + R F C + R y
92 89 91 mpbid φ x y ran F C R C + R = x y F C + R x F C + R F C + R y
93 92 simp2d φ x y ran F C R C + R = x y x F C + R
94 7 71 sseldd φ C + R X
95 22 94 ffvelrnd φ F C + R
96 95 adantr φ x y ran F C R C + R = x y F C + R
97 lelttr x F C + R F C x F C + R F C + R < F C x < F C
98 62 96 24 97 syl3anc φ x y ran F C R C + R = x y x F C + R F C + R < F C x < F C
99 93 98 mpand φ x y ran F C R C + R = x y F C + R < F C x < F C
100 85 99 syld φ x y ran F C R C + R = x y F C R C + R Isom < , < -1 C R C + R ran F C R C + R x < F C
101 ax-resscn
102 101 a1i φ
103 fss F : X F : X
104 22 101 103 sylancl φ F : X
105 7 9 sstrd φ C R C + R
106 eqid TopOpen fld = TopOpen fld
107 106 tgioo2 topGen ran . = TopOpen fld 𝑡
108 106 107 dvres F : X X C R C + R D F C R C + R = F int topGen ran . C R C + R
109 102 104 9 105 108 syl22anc φ D F C R C + R = F int topGen ran . C R C + R
110 iccntr C R C + R int topGen ran . C R C + R = C R C + R
111 12 13 110 syl2anc φ int topGen ran . C R C + R = C R C + R
112 111 reseq2d φ F int topGen ran . C R C + R = F C R C + R
113 109 112 eqtrd φ D F C R C + R = F C R C + R
114 113 dmeqd φ dom F C R C + R = dom F C R C + R
115 dmres dom F C R C + R = C R C + R dom F
116 ioossicc C R C + R C R C + R
117 116 7 sstrid φ C R C + R X
118 117 2 sseqtrrd φ C R C + R dom F
119 df-ss C R C + R dom F C R C + R dom F = C R C + R
120 118 119 sylib φ C R C + R dom F = C R C + R
121 115 120 eqtrid φ dom F C R C + R = C R C + R
122 114 121 eqtrd φ dom F C R C + R = C R C + R
123 resss F C R C + R D F
124 113 123 eqsstrdi φ D F C R C + R D F
125 rnss D F C R C + R D F ran F C R C + R ran F
126 124 125 syl φ ran F C R C + R ran F
127 126 3 ssneldd φ ¬ 0 ran F C R C + R
128 12 13 19 122 127 dvne0 φ F C R C + R Isom < , < C R C + R ran F C R C + R F C R C + R Isom < , < -1 C R C + R ran F C R C + R
129 128 adantr φ x y ran F C R C + R = x y F C R C + R Isom < , < C R C + R ran F C R C + R F C R C + R Isom < , < -1 C R C + R ran F C R C + R
130 69 100 129 mpjaod φ x y ran F C R C + R = x y x < F C
131 isorel F C R C + R Isom < , < C R C + R ran F C R C + R C C R C + R C + R C R C + R C < C + R F C R C + R C < F C R C + R C + R
132 131 biimpd F C R C + R Isom < , < C R C + R ran F C R C + R C C R C + R C + R C R C + R C < C + R F C R C + R C < F C R C + R C + R
133 132 exp32 F C R C + R Isom < , < C R C + R ran F C R C + R C C R C + R C + R C R C + R C < C + R F C R C + R C < F C R C + R C + R
134 133 com4l C C R C + R C + R C R C + R C < C + R F C R C + R Isom < , < C R C + R ran F C R C + R F C R C + R C < F C R C + R C + R
135 35 72 73 134 syl3c φ x y ran F C R C + R = x y F C R C + R Isom < , < C R C + R ran F C R C + R F C R C + R C < F C R C + R C + R
136 43 82 breq12d φ x y ran F C R C + R = x y F C R C + R C < F C R C + R C + R F C < F C + R
137 135 136 sylibd φ x y ran F C R C + R = x y F C R C + R Isom < , < C R C + R ran F C R C + R F C < F C + R
138 92 simp3d φ x y ran F C R C + R = x y F C + R y
139 simprlr φ x y ran F C R C + R = x y y
140 ltletr F C F C + R y F C < F C + R F C + R y F C < y
141 24 96 139 140 syl3anc φ x y ran F C R C + R = x y F C < F C + R F C + R y F C < y
142 138 141 mpan2d φ x y ran F C R C + R = x y F C < F C + R F C < y
143 137 142 syld φ x y ran F C R C + R = x y F C R C + R Isom < , < C R C + R ran F C R C + R F C < y
144 isorel F C R C + R Isom < , < -1 C R C + R ran F C R C + R C R C R C + R C C R C + R C R < C F C R C + R C R < -1 F C R C + R C
145 144 biimpd F C R C + R Isom < , < -1 C R C + R ran F C R C + R C R C R C + R C C R C + R C R < C F C R C + R C R < -1 F C R C + R C
146 145 exp32 F C R C + R Isom < , < -1 C R C + R ran F C R C + R C R C R C + R C C R C + R C R < C F C R C + R C R < -1 F C R C + R C
147 146 com4l C R C R C + R C C R C + R C R < C F C R C + R Isom < , < -1 C R C + R ran F C R C + R F C R C + R C R < -1 F C R C + R C
148 29 35 36 147 syl3c φ x y ran F C R C + R = x y F C R C + R Isom < , < -1 C R C + R ran F C R C + R F C R C + R C R < -1 F C R C + R C
149 fvex F C R C + R C R V
150 149 79 brcnv F C R C + R C R < -1 F C R C + R C F C R C + R C < F C R C + R C R
151 43 42 breq12d φ x y ran F C R C + R = x y F C R C + R C < F C R C + R C R F C < F C R
152 150 151 syl5bb φ x y ran F C R C + R = x y F C R C + R C R < -1 F C R C + R C F C < F C R
153 148 152 sylibd φ x y ran F C R C + R = x y F C R C + R Isom < , < -1 C R C + R ran F C R C + R F C < F C R
154 60 simp3d φ x y ran F C R C + R = x y F C R y
155 ltletr F C F C R y F C < F C R F C R y F C < y
156 24 65 139 155 syl3anc φ x y ran F C R C + R = x y F C < F C R F C R y F C < y
157 154 156 mpan2d φ x y ran F C R C + R = x y F C < F C R F C < y
158 153 157 syld φ x y ran F C R C + R = x y F C R C + R Isom < , < -1 C R C + R ran F C R C + R F C < y
159 143 158 129 mpjaod φ x y ran F C R C + R = x y F C < y
160 62 rexrd φ x y ran F C R C + R = x y x *
161 139 rexrd φ x y ran F C R C + R = x y y *
162 elioo2 x * y * F C x y F C x < F C F C < y
163 160 161 162 syl2anc φ x y ran F C R C + R = x y F C x y F C x < F C F C < y
164 24 130 159 163 mpbir3and φ x y ran F C R C + R = x y F C x y
165 56 fveq2d φ x y ran F C R C + R = x y int topGen ran . F C R C + R = int topGen ran . x y
166 iccntr x y int topGen ran . x y = x y
167 166 ad2antrl φ x y ran F C R C + R = x y int topGen ran . x y = x y
168 165 167 eqtrd φ x y ran F C R C + R = x y int topGen ran . F C R C + R = x y
169 164 168 eleqtrrd φ x y ran F C R C + R = x y F C int topGen ran . F C R C + R
170 169 expr φ x y ran F C R C + R = x y F C int topGen ran . F C R C + R
171 170 rexlimdvva φ x y ran F C R C + R = x y F C int topGen ran . F C R C + R
172 20 171 mpd φ F C int topGen ran . F C R C + R