Metamath Proof Explorer


Theorem stoweidlem35

Description: This lemma is used to prove the existence of a function p as in Lemma 1 of BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Here ( qi ) is used to represent p__(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem35.1 tφ
stoweidlem35.2 wφ
stoweidlem35.3 hφ
stoweidlem35.4 Q=hA|hZ=0tT0htht1
stoweidlem35.5 W=wJ|hQw=tT|0<ht
stoweidlem35.6 G=wXhQ|w=tT|0<ht
stoweidlem35.7 φAV
stoweidlem35.8 φXFin
stoweidlem35.9 φXW
stoweidlem35.10 φTUX
stoweidlem35.11 φTU
Assertion stoweidlem35 φmqmq:1mQtTUi1m0<qit

Proof

Step Hyp Ref Expression
1 stoweidlem35.1 tφ
2 stoweidlem35.2 wφ
3 stoweidlem35.3 hφ
4 stoweidlem35.4 Q=hA|hZ=0tT0htht1
5 stoweidlem35.5 W=wJ|hQw=tT|0<ht
6 stoweidlem35.6 G=wXhQ|w=tT|0<ht
7 stoweidlem35.7 φAV
8 stoweidlem35.8 φXFin
9 stoweidlem35.9 φXW
10 stoweidlem35.10 φTUX
11 stoweidlem35.11 φTU
12 6 rnmptfi XFinranGFin
13 8 12 syl φranGFin
14 fnchoice ranGFinggFnranGlranGlgll
15 14 adantl φranGFinggFnranGlranGlgll
16 simprl φgFnranGlranGlgllgFnranG
17 nfmpt1 _wwXhQ|w=tT|0<ht
18 6 17 nfcxfr _wG
19 18 nfrn _wranG
20 19 nfcri wkranG
21 2 20 nfan wφkranG
22 9 sselda φwXwW
23 22 5 eleqtrdi φwXwwJ|hQw=tT|0<ht
24 rabid wwJ|hQw=tT|0<htwJhQw=tT|0<ht
25 23 24 sylib φwXwJhQw=tT|0<ht
26 25 simprd φwXhQw=tT|0<ht
27 df-rex hQw=tT|0<hthhQw=tT|0<ht
28 26 27 sylib φwXhhQw=tT|0<ht
29 rabid hhQ|w=tT|0<hthQw=tT|0<ht
30 29 exbii hhhQ|w=tT|0<hthhQw=tT|0<ht
31 28 30 sylibr φwXhhhQ|w=tT|0<ht
32 31 adantr φwXk=hQ|w=tT|0<hthhhQ|w=tT|0<ht
33 nfv hwX
34 3 33 nfan hφwX
35 nfrab1 _hhQ|w=tT|0<ht
36 35 nfeq2 hk=hQ|w=tT|0<ht
37 34 36 nfan hφwXk=hQ|w=tT|0<ht
38 eleq2 k=hQ|w=tT|0<hthkhhQ|w=tT|0<ht
39 38 biimprd k=hQ|w=tT|0<hthhQ|w=tT|0<hthk
40 39 adantl φwXk=hQ|w=tT|0<hthhQ|w=tT|0<hthk
41 37 40 eximd φwXk=hQ|w=tT|0<hthhhQ|w=tT|0<hthhk
42 32 41 mpd φwXk=hQ|w=tT|0<hthhk
43 42 adantllr φkranGwXk=hQ|w=tT|0<hthhk
44 6 elrnmpt kranGkranGwXk=hQ|w=tT|0<ht
45 44 ibi kranGwXk=hQ|w=tT|0<ht
46 45 adantl φkranGwXk=hQ|w=tT|0<ht
47 21 43 46 r19.29af φkranGhhk
48 n0 khhk
49 47 48 sylibr φkranGk
50 49 adantlr φgFnranGlranGlgllkranGk
51 simplrr φgFnranGlranGlgllkranGlranGlgll
52 neeq1 l=klk
53 fveq2 l=kgl=gk
54 53 eleq1d l=kgllgkl
55 eleq2 l=kgklgkk
56 54 55 bitrd l=kgllgkk
57 52 56 imbi12d l=klgllkgkk
58 57 rspccva lranGlgllkranGkgkk
59 51 58 sylancom φgFnranGlranGlgllkranGkgkk
60 50 59 mpd φgFnranGlranGlgllkranGgkk
61 60 ralrimiva φgFnranGlranGlgllkranGgkk
62 fveq2 k=lgk=gl
63 62 eleq1d k=lgkkglk
64 eleq2 k=lglkgll
65 63 64 bitrd k=lgkkgll
66 65 cbvralvw kranGgkklranGgll
67 61 66 sylib φgFnranGlranGlglllranGgll
68 16 67 jca φgFnranGlranGlgllgFnranGlranGgll
69 68 ex φgFnranGlranGlgllgFnranGlranGgll
70 69 adantr φranGFingFnranGlranGlgllgFnranGlranGgll
71 70 eximdv φranGFinggFnranGlranGlgllggFnranGlranGgll
72 15 71 mpd φranGFinggFnranGlranGgll
73 13 72 mpdan φggFnranGlranGgll
74 73 ralrimivw φmggFnranGlranGgll
75 ssn0 TUXTUX
76 10 11 75 syl2anc φX
77 76 neneqd φ¬X=
78 unieq X=X=
79 uni0 =
80 78 79 eqtrdi X=X=
81 77 80 nsyl φ¬X=
82 dm0rn0 domG=ranG=
83 4 7 rabexd φQV
84 nfrab1 _hhA|hZ=0tT0htht1
85 4 84 nfcxfr _hQ
86 85 rabexgf QVhQ|w=tT|0<htV
87 83 86 syl φhQ|w=tT|0<htV
88 87 adantr φwXhQ|w=tT|0<htV
89 2 88 6 fmptdf φG:XV
90 dffn2 GFnXG:XV
91 89 90 sylibr φGFnX
92 91 fndmd φdomG=X
93 92 eqeq1d φdomG=X=
94 82 93 bitr3id φranG=X=
95 81 94 mtbird φ¬ranG=
96 fz1f1o ranGFinranG=ranGff:1ranG1-1 ontoranG
97 13 96 syl φranG=ranGff:1ranG1-1 ontoranG
98 97 ord φ¬ranG=ranGff:1ranG1-1 ontoranG
99 95 98 mpd φranGff:1ranG1-1 ontoranG
100 oveq2 m=ranG1m=1ranG
101 100 f1oeq2d m=ranGf:1m1-1 ontoranGf:1ranG1-1 ontoranG
102 101 exbidv m=ranGff:1m1-1 ontoranGff:1ranG1-1 ontoranG
103 102 rspcev ranGff:1ranG1-1 ontoranGmff:1m1-1 ontoranG
104 99 103 syl φmff:1m1-1 ontoranG
105 r19.29 mggFnranGlranGgllmff:1m1-1 ontoranGmggFnranGlranGgllff:1m1-1 ontoranG
106 74 104 105 syl2anc φmggFnranGlranGgllff:1m1-1 ontoranG
107 exdistrv gfgFnranGlranGgllf:1m1-1 ontoranGggFnranGlranGgllff:1m1-1 ontoranG
108 107 biimpri ggFnranGlranGgllff:1m1-1 ontoranGgfgFnranGlranGgllf:1m1-1 ontoranG
109 108 a1i φggFnranGlranGgllff:1m1-1 ontoranGgfgFnranGlranGgllf:1m1-1 ontoranG
110 109 reximdv φmggFnranGlranGgllff:1m1-1 ontoranGmgfgFnranGlranGgllf:1m1-1 ontoranG
111 106 110 mpd φmgfgFnranGlranGgllf:1m1-1 ontoranG
112 df-rex mgfgFnranGlranGgllf:1m1-1 ontoranGmmgfgFnranGlranGgllf:1m1-1 ontoranG
113 111 112 sylib φmmgfgFnranGlranGgllf:1m1-1 ontoranG
114 ax-5 mgm
115 19.29 gmgfgFnranGlranGgllf:1m1-1 ontoranGgmfgFnranGlranGgllf:1m1-1 ontoranG
116 114 115 sylan mgfgFnranGlranGgllf:1m1-1 ontoranGgmfgFnranGlranGgllf:1m1-1 ontoranG
117 ax-5 mfm
118 19.29 fmfgFnranGlranGgllf:1m1-1 ontoranGfmgFnranGlranGgllf:1m1-1 ontoranG
119 117 118 sylan mfgFnranGlranGgllf:1m1-1 ontoranGfmgFnranGlranGgllf:1m1-1 ontoranG
120 119 eximi gmfgFnranGlranGgllf:1m1-1 ontoranGgfmgFnranGlranGgllf:1m1-1 ontoranG
121 116 120 syl mgfgFnranGlranGgllf:1m1-1 ontoranGgfmgFnranGlranGgllf:1m1-1 ontoranG
122 df-3an gFnranGlranGgllf:1m1-1 ontoranGgFnranGlranGgllf:1m1-1 ontoranG
123 122 anbi2i mgFnranGlranGgllf:1m1-1 ontoranGmgFnranGlranGgllf:1m1-1 ontoranG
124 123 2exbii gfmgFnranGlranGgllf:1m1-1 ontoranGgfmgFnranGlranGgllf:1m1-1 ontoranG
125 121 124 sylibr mgfgFnranGlranGgllf:1m1-1 ontoranGgfmgFnranGlranGgllf:1m1-1 ontoranG
126 125 a1i φmgfgFnranGlranGgllf:1m1-1 ontoranGgfmgFnranGlranGgllf:1m1-1 ontoranG
127 126 eximdv φmmgfgFnranGlranGgllf:1m1-1 ontoranGmgfmgFnranGlranGgllf:1m1-1 ontoranG
128 113 127 mpd φmgfmgFnranGlranGgllf:1m1-1 ontoranG
129 83 adantr φmgFnranGlranGgllf:1m1-1 ontoranGQV
130 simprl φmgFnranGlranGgllf:1m1-1 ontoranGm
131 simprr1 φmgFnranGlranGgllf:1m1-1 ontoranGgFnranG
132 elex ranGFinranGV
133 13 132 syl φranGV
134 133 adantr φmgFnranGlranGgllf:1m1-1 ontoranGranGV
135 simprr2 φmgFnranGlranGgllf:1m1-1 ontoranGlranGgll
136 56 rspccva lranGgllkranGgkk
137 135 136 sylan φmgFnranGlranGgllf:1m1-1 ontoranGkranGgkk
138 simprr3 φmgFnranGlranGgllf:1m1-1 ontoranGf:1m1-1 ontoranG
139 10 adantr φmgFnranGlranGgllf:1m1-1 ontoranGTUX
140 nfv tm
141 nfcv _tg
142 nfcv _tX
143 nfrab1 _ttT|0<ht
144 143 nfeq2 tw=tT|0<ht
145 nfv thZ=0
146 nfra1 ttT0htht1
147 145 146 nfan thZ=0tT0htht1
148 nfcv _tA
149 147 148 nfrabw _thA|hZ=0tT0htht1
150 4 149 nfcxfr _tQ
151 144 150 nfrabw _thQ|w=tT|0<ht
152 142 151 nfmpt _twXhQ|w=tT|0<ht
153 6 152 nfcxfr _tG
154 153 nfrn _tranG
155 141 154 nffn tgFnranG
156 nfv tgll
157 154 156 nfralw tlranGgll
158 nfcv _tf
159 nfcv _t1m
160 158 159 154 nff1o tf:1m1-1 ontoranG
161 155 157 160 nf3an tgFnranGlranGgllf:1m1-1 ontoranG
162 140 161 nfan tmgFnranGlranGgllf:1m1-1 ontoranG
163 1 162 nfan tφmgFnranGlranGgllf:1m1-1 ontoranG
164 nfv wm
165 nfcv _wg
166 165 19 nffn wgFnranG
167 nfv wgll
168 19 167 nfralw wlranGgll
169 nfcv _wf
170 nfcv _w1m
171 169 170 19 nff1o wf:1m1-1 ontoranG
172 166 168 171 nf3an wgFnranGlranGgllf:1m1-1 ontoranG
173 164 172 nfan wmgFnranGlranGgllf:1m1-1 ontoranG
174 2 173 nfan wφmgFnranGlranGgllf:1m1-1 ontoranG
175 6 129 130 131 134 137 138 139 163 174 85 stoweidlem27 φmgFnranGlranGgllf:1m1-1 ontoranGqmq:1mQtTUi1m0<qit
176 175 ex φmgFnranGlranGgllf:1m1-1 ontoranGqmq:1mQtTUi1m0<qit
177 176 2eximdv φgfmgFnranGlranGgllf:1m1-1 ontoranGgfqmq:1mQtTUi1m0<qit
178 177 eximdv φmgfmgFnranGlranGgllf:1m1-1 ontoranGmgfqmq:1mQtTUi1m0<qit
179 128 178 mpd φmgfqmq:1mQtTUi1m0<qit
180 id qmq:1mQtTUi1m0<qitqmq:1mQtTUi1m0<qit
181 180 exlimivv gfqmq:1mQtTUi1m0<qitqmq:1mQtTUi1m0<qit
182 181 eximi mgfqmq:1mQtTUi1m0<qitmqmq:1mQtTUi1m0<qit
183 179 182 syl φmqmq:1mQtTUi1m0<qit