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 _ t U
stoweidlem53.2 t φ
stoweidlem53.3 K = topGen ran .
stoweidlem53.4 Q = h A | h Z = 0 t T 0 h t h t 1
stoweidlem53.5 W = w J | h Q w = t T | 0 < h t
stoweidlem53.6 T = J
stoweidlem53.7 C = J Cn K
stoweidlem53.8 φ J Comp
stoweidlem53.9 φ A C
stoweidlem53.10 φ f A g A t T f t + g t A
stoweidlem53.11 φ f A g A t T f t g t A
stoweidlem53.12 φ x t T x A
stoweidlem53.13 φ r T t T r t q A q r q t
stoweidlem53.14 φ U J
stoweidlem53.15 φ T U
stoweidlem53.16 φ Z U
Assertion stoweidlem53 φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t

Proof

Step Hyp Ref Expression
1 stoweidlem53.1 _ t U
2 stoweidlem53.2 t φ
3 stoweidlem53.3 K = topGen ran .
4 stoweidlem53.4 Q = h A | h Z = 0 t T 0 h t h t 1
5 stoweidlem53.5 W = w J | h Q w = t T | 0 < h t
6 stoweidlem53.6 T = J
7 stoweidlem53.7 C = J Cn K
8 stoweidlem53.8 φ J Comp
9 stoweidlem53.9 φ A C
10 stoweidlem53.10 φ f A g A t T f t + g t A
11 stoweidlem53.11 φ f A g A t T f t g t A
12 stoweidlem53.12 φ x t T x A
13 stoweidlem53.13 φ r T t T r t q A q r q t
14 stoweidlem53.14 φ U J
15 stoweidlem53.15 φ T U
16 stoweidlem53.16 φ Z U
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 16 stoweidlem50 φ u u Fin u W T U u
18 nfv t u Fin
19 nfcv _ t u
20 nfv t h Z = 0
21 nfra1 t t T 0 h t h t 1
22 20 21 nfan t h Z = 0 t T 0 h t h t 1
23 nfcv _ t A
24 22 23 nfrabw _ t h A | h Z = 0 t T 0 h t h t 1
25 4 24 nfcxfr _ t Q
26 nfrab1 _ t t T | 0 < h t
27 26 nfeq2 t w = t T | 0 < h t
28 25 27 nfrex t h Q w = t T | 0 < h t
29 nfcv _ t J
30 28 29 nfrabw _ t w J | h Q w = t T | 0 < h t
31 5 30 nfcxfr _ t W
32 19 31 nfss t u W
33 nfcv _ t T
34 33 1 nfdif _ t T U
35 nfcv _ t u
36 34 35 nfss t T U u
37 18 32 36 nf3an t u Fin u W T U u
38 2 37 nfan t φ u Fin u W T U u
39 nfv w φ
40 nfv w u Fin
41 nfcv _ w u
42 nfrab1 _ w w J | h Q w = t T | 0 < h t
43 5 42 nfcxfr _ w W
44 41 43 nfss w u W
45 nfv w T U u
46 40 44 45 nf3an w u Fin u W T U u
47 39 46 nfan w φ u Fin u W T U u
48 nfv h φ
49 nfv h u Fin
50 nfcv _ h u
51 nfre1 h h Q w = t T | 0 < h t
52 nfcv _ h J
53 51 52 nfrabw _ h w J | h Q w = t T | 0 < h t
54 5 53 nfcxfr _ h W
55 50 54 nfss h u W
56 nfv h T U u
57 49 55 56 nf3an h u Fin u W T U u
58 48 57 nfan h φ u Fin u W T U u
59 eqid w u h Q | w = t T | 0 < h t = w u h Q | w = t T | 0 < h t
60 cmptop J Comp J Top
61 8 60 syl φ J Top
62 retop topGen ran . Top
63 3 62 eqeltri K Top
64 cnfex J Top K Top J Cn K V
65 61 63 64 sylancl φ J Cn K V
66 9 7 sseqtrdi φ A J Cn K
67 65 66 ssexd φ A V
68 67 adantr φ u Fin u W T U u A V
69 simpr1 φ u Fin u W T U u u Fin
70 simpr2 φ u Fin u W T U u u W
71 simpr3 φ u Fin u W T U u T U u
72 15 adantr φ u Fin u W T U u T U
73 38 47 58 4 5 59 68 69 70 71 72 stoweidlem35 φ u Fin u W T U u m q m q : 1 m Q t T U i 1 m 0 < q i t
74 17 73 exlimddv φ m q m q : 1 m Q t T U i 1 m 0 < q i t
75 nfv i φ
76 nfv i m
77 nfv i q : 1 m Q
78 nfcv _ i T U
79 nfre1 i i 1 m 0 < q i t
80 78 79 nfralw i t T U i 1 m 0 < q i t
81 77 80 nfan i q : 1 m Q t T U i 1 m 0 < q i t
82 76 81 nfan i m q : 1 m Q t T U i 1 m 0 < q i t
83 75 82 nfan i φ m q : 1 m Q t T U i 1 m 0 < q i t
84 nfv t m
85 nfcv _ t q
86 nfcv _ t 1 m
87 85 86 25 nff t q : 1 m Q
88 nfra1 t t T U i 1 m 0 < q i t
89 87 88 nfan t q : 1 m Q t T U i 1 m 0 < q i t
90 84 89 nfan t m q : 1 m Q t T U i 1 m 0 < q i t
91 2 90 nfan t φ m q : 1 m Q t T U i 1 m 0 < q i t
92 eqid t T 1 m y = 1 m q y t = t T 1 m y = 1 m q y t
93 simprl φ m q : 1 m Q t T U i 1 m 0 < q i t m
94 simprrl φ m q : 1 m Q t T U i 1 m 0 < q i t q : 1 m Q
95 simprrr φ m q : 1 m Q t T U i 1 m 0 < q i t t T U i 1 m 0 < q i t
96 66 adantr φ m q : 1 m Q t T U i 1 m 0 < q i t A J Cn K
97 10 3adant1r φ m q : 1 m Q t T U i 1 m 0 < q i t f A g A t T f t + g t A
98 11 3adant1r φ m q : 1 m Q t T U i 1 m 0 < q i t f A g A t T f t g t A
99 12 adantlr φ m q : 1 m Q t T U i 1 m 0 < q i t x t T x A
100 elssuni U J U J
101 100 6 sseqtrrdi U J U T
102 14 101 syl φ U T
103 102 16 sseldd φ Z T
104 103 adantr φ m q : 1 m Q t T U i 1 m 0 < q i t Z T
105 83 91 3 4 92 93 94 95 6 96 97 98 99 104 stoweidlem44 φ m q : 1 m Q t T U i 1 m 0 < q i t p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t
106 105 ex φ m q : 1 m Q t T U i 1 m 0 < q i t p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t
107 106 exlimdvv φ m q m q : 1 m Q t T U i 1 m 0 < q i t p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t
108 74 107 mpd φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t