Metamath Proof Explorer


Theorem stoweidlem58

Description: This theorem proves Lemma 2 in BrosowskiDeutsh p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem58.1 _ t D
stoweidlem58.2 _ t U
stoweidlem58.3 t φ
stoweidlem58.4 K = topGen ran .
stoweidlem58.5 T = J
stoweidlem58.6 C = J Cn K
stoweidlem58.7 φ J Comp
stoweidlem58.8 φ A C
stoweidlem58.9 φ f A g A t T f t + g t A
stoweidlem58.10 φ f A g A t T f t g t A
stoweidlem58.11 φ a t T a A
stoweidlem58.12 φ r T t T r t q A q r q t
stoweidlem58.13 φ B Clsd J
stoweidlem58.14 φ D Clsd J
stoweidlem58.15 φ B D =
stoweidlem58.16 U = T B
stoweidlem58.17 φ E +
stoweidlem58.18 φ E < 1 3
Assertion stoweidlem58 φ x A t T 0 x t x t 1 t D x t < E t B 1 E < x t

Proof

Step Hyp Ref Expression
1 stoweidlem58.1 _ t D
2 stoweidlem58.2 _ t U
3 stoweidlem58.3 t φ
4 stoweidlem58.4 K = topGen ran .
5 stoweidlem58.5 T = J
6 stoweidlem58.6 C = J Cn K
7 stoweidlem58.7 φ J Comp
8 stoweidlem58.8 φ A C
9 stoweidlem58.9 φ f A g A t T f t + g t A
10 stoweidlem58.10 φ f A g A t T f t g t A
11 stoweidlem58.11 φ a t T a A
12 stoweidlem58.12 φ r T t T r t q A q r q t
13 stoweidlem58.13 φ B Clsd J
14 stoweidlem58.14 φ D Clsd J
15 stoweidlem58.15 φ B D =
16 stoweidlem58.16 U = T B
17 stoweidlem58.17 φ E +
18 stoweidlem58.18 φ E < 1 3
19 1 nfeq1 t D =
20 3 19 nfan t φ D =
21 eqid t T 1 = t T 1
22 11 adantlr φ D = a t T a A
23 13 adantr φ D = B Clsd J
24 17 adantr φ D = E +
25 simpr φ D = D =
26 1 20 21 5 22 23 24 25 stoweidlem18 φ D = x A t T 0 x t x t 1 t D x t < E t B 1 E < x t
27 nfcv _ t
28 1 27 nfne t D
29 3 28 nfan t φ D
30 eqid h A | t T 0 h t h t 1 = h A | t T 0 h t h t 1
31 eqid w J | e + h A t T 0 h t h t 1 t w h t < e t T U 1 e < h t = w J | e + h A t T 0 h t h t 1 t w h t < e t T U 1 e < h t
32 7 adantr φ D J Comp
33 8 adantr φ D A C
34 9 3adant1r φ D f A g A t T f t + g t A
35 10 3adant1r φ D f A g A t T f t g t A
36 11 adantlr φ D a t T a A
37 12 adantlr φ D r T t T r t q A q r q t
38 13 adantr φ D B Clsd J
39 14 adantr φ D D Clsd J
40 15 adantr φ D B D =
41 simpr φ D D
42 17 adantr φ D E +
43 18 adantr φ D E < 1 3
44 1 2 29 30 31 4 5 6 16 32 33 34 35 36 37 38 39 40 41 42 43 stoweidlem57 φ D x A t T 0 x t x t 1 t D x t < E t B 1 E < x t
45 26 44 pm2.61dane φ x A t T 0 x t x t 1 t D x t < E t B 1 E < x t