Metamath Proof Explorer


Theorem stoweidlem55

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

Ref Expression
Hypotheses stoweidlem55.1 _ t U
stoweidlem55.2 t φ
stoweidlem55.3 K = topGen ran .
stoweidlem55.4 φ J Comp
stoweidlem55.5 T = J
stoweidlem55.6 C = J Cn K
stoweidlem55.7 φ A C
stoweidlem55.8 φ f A g A t T f t + g t A
stoweidlem55.9 φ f A g A t T f t g t A
stoweidlem55.10 φ x t T x A
stoweidlem55.11 φ r T t T r t q A q r q t
stoweidlem55.12 φ U J
stoweidlem55.13 φ Z U
stoweidlem55.14 Q = h A | h Z = 0 t T 0 h t h t 1
stoweidlem55.15 W = w J | h Q w = t T | 0 < h t
Assertion stoweidlem55 φ 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 stoweidlem55.1 _ t U
2 stoweidlem55.2 t φ
3 stoweidlem55.3 K = topGen ran .
4 stoweidlem55.4 φ J Comp
5 stoweidlem55.5 T = J
6 stoweidlem55.6 C = J Cn K
7 stoweidlem55.7 φ A C
8 stoweidlem55.8 φ f A g A t T f t + g t A
9 stoweidlem55.9 φ f A g A t T f t g t A
10 stoweidlem55.10 φ x t T x A
11 stoweidlem55.11 φ r T t T r t q A q r q t
12 stoweidlem55.12 φ U J
13 stoweidlem55.13 φ Z U
14 stoweidlem55.14 Q = h A | h Z = 0 t T 0 h t h t 1
15 stoweidlem55.15 W = w J | h Q w = t T | 0 < h t
16 0re 0
17 10 stoweidlem4 φ 0 t T 0 A
18 16 17 mpan2 φ t T 0 A
19 18 adantr φ T U = t T 0 A
20 nfcv _ t T
21 20 1 nfdif _ t T U
22 nfcv _ t
23 21 22 nfeq t T U =
24 2 23 nfan t φ T U =
25 0le0 0 0
26 0cn 0
27 eqid t T 0 = t T 0
28 27 fvmpt2 t T 0 t T 0 t = 0
29 26 28 mpan2 t T t T 0 t = 0
30 25 29 breqtrrid t T 0 t T 0 t
31 30 adantl φ T U = t T 0 t T 0 t
32 0le1 0 1
33 29 32 eqbrtrdi t T t T 0 t 1
34 33 adantl φ T U = t T t T 0 t 1
35 31 34 jca φ T U = t T 0 t T 0 t t T 0 t 1
36 35 ex φ T U = t T 0 t T 0 t t T 0 t 1
37 24 36 ralrimi φ T U = t T 0 t T 0 t t T 0 t 1
38 13 12 jca φ Z U U J
39 elunii Z U U J Z J
40 39 5 eleqtrrdi Z U U J Z T
41 eqidd t = Z 0 = 0
42 c0ex 0 V
43 41 27 42 fvmpt Z T t T 0 Z = 0
44 38 40 43 3syl φ t T 0 Z = 0
45 44 adantr φ T U = t T 0 Z = 0
46 23 rzalf T U = t T U 0 < t T 0 t
47 46 adantl φ T U = t T U 0 < t T 0 t
48 nfcv _ t p
49 nfmpt1 _ t t T 0
50 48 49 nfeq t p = t T 0
51 fveq1 p = t T 0 p t = t T 0 t
52 51 breq2d p = t T 0 0 p t 0 t T 0 t
53 51 breq1d p = t T 0 p t 1 t T 0 t 1
54 52 53 anbi12d p = t T 0 0 p t p t 1 0 t T 0 t t T 0 t 1
55 50 54 ralbid p = t T 0 t T 0 p t p t 1 t T 0 t T 0 t t T 0 t 1
56 fveq1 p = t T 0 p Z = t T 0 Z
57 56 eqeq1d p = t T 0 p Z = 0 t T 0 Z = 0
58 51 breq2d p = t T 0 0 < p t 0 < t T 0 t
59 50 58 ralbid p = t T 0 t T U 0 < p t t T U 0 < t T 0 t
60 55 57 59 3anbi123d p = t T 0 t T 0 p t p t 1 p Z = 0 t T U 0 < p t t T 0 t T 0 t t T 0 t 1 t T 0 Z = 0 t T U 0 < t T 0 t
61 60 rspcev t T 0 A t T 0 t T 0 t t T 0 t 1 t T 0 Z = 0 t T U 0 < t T 0 t p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t
62 19 37 45 47 61 syl13anc φ T U = p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t
63 23 nfn t ¬ T U =
64 2 63 nfan t φ ¬ T U =
65 4 adantr φ ¬ T U = J Comp
66 7 adantr φ ¬ T U = A C
67 8 3adant1r φ ¬ T U = f A g A t T f t + g t A
68 9 3adant1r φ ¬ T U = f A g A t T f t g t A
69 10 adantlr φ ¬ T U = x t T x A
70 11 adantlr φ ¬ T U = r T t T r t q A q r q t
71 12 adantr φ ¬ T U = U J
72 neqne ¬ T U = T U
73 72 adantl φ ¬ T U = T U
74 13 adantr φ ¬ T U = Z U
75 1 64 3 14 15 5 6 65 66 67 68 69 70 71 73 74 stoweidlem53 φ ¬ T U = p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t
76 62 75 pm2.61dan φ p A t T 0 p t p t 1 p Z = 0 t T U 0 < p t