Metamath Proof Explorer


Theorem stoweidlem53

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 0 < p on T \ U . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem53.1 _tU
stoweidlem53.2 tφ
stoweidlem53.3 K=topGenran.
stoweidlem53.4 Q=hA|hZ=0tT0htht1
stoweidlem53.5 W=wJ|hQw=tT|0<ht
stoweidlem53.6 T=J
stoweidlem53.7 C=JCnK
stoweidlem53.8 φJComp
stoweidlem53.9 φAC
stoweidlem53.10 φfAgAtTft+gtA
stoweidlem53.11 φfAgAtTftgtA
stoweidlem53.12 φxtTxA
stoweidlem53.13 φrTtTrtqAqrqt
stoweidlem53.14 φUJ
stoweidlem53.15 φTU
stoweidlem53.16 φZU
Assertion stoweidlem53 φpAtT0ptpt1pZ=0tTU0<pt

Proof

Step Hyp Ref Expression
1 stoweidlem53.1 _tU
2 stoweidlem53.2 tφ
3 stoweidlem53.3 K=topGenran.
4 stoweidlem53.4 Q=hA|hZ=0tT0htht1
5 stoweidlem53.5 W=wJ|hQw=tT|0<ht
6 stoweidlem53.6 T=J
7 stoweidlem53.7 C=JCnK
8 stoweidlem53.8 φJComp
9 stoweidlem53.9 φAC
10 stoweidlem53.10 φfAgAtTft+gtA
11 stoweidlem53.11 φfAgAtTftgtA
12 stoweidlem53.12 φxtTxA
13 stoweidlem53.13 φrTtTrtqAqrqt
14 stoweidlem53.14 φUJ
15 stoweidlem53.15 φTU
16 stoweidlem53.16 φZU
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 16 stoweidlem50 φuuFinuWTUu
18 nfv tuFin
19 nfcv _tu
20 nfv thZ=0
21 nfra1 ttT0htht1
22 20 21 nfan thZ=0tT0htht1
23 nfcv _tA
24 22 23 nfrabw _thA|hZ=0tT0htht1
25 4 24 nfcxfr _tQ
26 nfrab1 _ttT|0<ht
27 26 nfeq2 tw=tT|0<ht
28 25 27 nfrex thQw=tT|0<ht
29 nfcv _tJ
30 28 29 nfrabw _twJ|hQw=tT|0<ht
31 5 30 nfcxfr _tW
32 19 31 nfss tuW
33 nfcv _tT
34 33 1 nfdif _tTU
35 nfcv _tu
36 34 35 nfss tTUu
37 18 32 36 nf3an tuFinuWTUu
38 2 37 nfan tφuFinuWTUu
39 nfv wφ
40 nfv wuFin
41 nfcv _wu
42 nfrab1 _wwJ|hQw=tT|0<ht
43 5 42 nfcxfr _wW
44 41 43 nfss wuW
45 nfv wTUu
46 40 44 45 nf3an wuFinuWTUu
47 39 46 nfan wφuFinuWTUu
48 nfv hφ
49 nfv huFin
50 nfcv _hu
51 nfre1 hhQw=tT|0<ht
52 nfcv _hJ
53 51 52 nfrabw _hwJ|hQw=tT|0<ht
54 5 53 nfcxfr _hW
55 50 54 nfss huW
56 nfv hTUu
57 49 55 56 nf3an huFinuWTUu
58 48 57 nfan hφuFinuWTUu
59 eqid wuhQ|w=tT|0<ht=wuhQ|w=tT|0<ht
60 cmptop JCompJTop
61 8 60 syl φJTop
62 retop topGenran.Top
63 3 62 eqeltri KTop
64 cnfex JTopKTopJCnKV
65 61 63 64 sylancl φJCnKV
66 9 7 sseqtrdi φAJCnK
67 65 66 ssexd φAV
68 67 adantr φuFinuWTUuAV
69 simpr1 φuFinuWTUuuFin
70 simpr2 φuFinuWTUuuW
71 simpr3 φuFinuWTUuTUu
72 15 adantr φuFinuWTUuTU
73 38 47 58 4 5 59 68 69 70 71 72 stoweidlem35 φuFinuWTUumqmq:1mQtTUi1m0<qit
74 17 73 exlimddv φmqmq:1mQtTUi1m0<qit
75 nfv iφ
76 nfv im
77 nfv iq:1mQ
78 nfcv _iTU
79 nfre1 ii1m0<qit
80 78 79 nfralw itTUi1m0<qit
81 77 80 nfan iq:1mQtTUi1m0<qit
82 76 81 nfan imq:1mQtTUi1m0<qit
83 75 82 nfan iφmq:1mQtTUi1m0<qit
84 nfv tm
85 nfcv _tq
86 nfcv _t1m
87 85 86 25 nff tq:1mQ
88 nfra1 ttTUi1m0<qit
89 87 88 nfan tq:1mQtTUi1m0<qit
90 84 89 nfan tmq:1mQtTUi1m0<qit
91 2 90 nfan tφmq:1mQtTUi1m0<qit
92 eqid tT1my=1mqyt=tT1my=1mqyt
93 simprl φmq:1mQtTUi1m0<qitm
94 simprrl φmq:1mQtTUi1m0<qitq:1mQ
95 simprrr φmq:1mQtTUi1m0<qittTUi1m0<qit
96 66 adantr φmq:1mQtTUi1m0<qitAJCnK
97 10 3adant1r φmq:1mQtTUi1m0<qitfAgAtTft+gtA
98 11 3adant1r φmq:1mQtTUi1m0<qitfAgAtTftgtA
99 12 adantlr φmq:1mQtTUi1m0<qitxtTxA
100 elssuni UJUJ
101 100 6 sseqtrrdi UJUT
102 14 101 syl φUT
103 102 16 sseldd φZT
104 103 adantr φmq:1mQtTUi1m0<qitZT
105 83 91 3 4 92 93 94 95 6 96 97 98 99 104 stoweidlem44 φmq:1mQtTUi1m0<qitpAtT0ptpt1pZ=0tTU0<pt
106 105 ex φmq:1mQtTUi1m0<qitpAtT0ptpt1pZ=0tTU0<pt
107 106 exlimdvv φmqmq:1mQtTUi1m0<qitpAtT0ptpt1pZ=0tTU0<pt
108 74 107 mpd φpAtT0ptpt1pZ=0tTU0<pt