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	\|- F/_ t D
	stoweidlem58.2	\|- F/_ t U
	stoweidlem58.3	\|- F/ t ph
	stoweidlem58.4	\|- K = ( topGen ` ran (,) )
	stoweidlem58.5	\|- T = U. J
	stoweidlem58.6	\|- C = ( J Cn K )
	stoweidlem58.7	\|- ( ph -> J e. Comp )
	stoweidlem58.8	\|- ( ph -> A C_ C )
	stoweidlem58.9	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
	stoweidlem58.10	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
	stoweidlem58.11	\|- ( ( ph /\ a e. RR ) -> ( t e. T \|-> a ) e. A )
	stoweidlem58.12	\|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
	stoweidlem58.13	\|- ( ph -> B e. ( Clsd ` J ) )
	stoweidlem58.14	\|- ( ph -> D e. ( Clsd ` J ) )
	stoweidlem58.15	\|- ( ph -> ( B i^i D ) = (/) )
	stoweidlem58.16	\|- U = ( T \ B )
	stoweidlem58.17	\|- ( ph -> E e. RR+ )
	stoweidlem58.18	\|- ( ph -> E < ( 1 / 3 ) )
Assertion	stoweidlem58	\|- ( ph -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) )

Proof

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

Metamath Proof Explorer

Theorem stoweidlem58

Proof