stoweidlem51

Description: There exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91. Here D is used to represent A in the paper, because here A is used for the subalgebra of functions. E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem51.1	\|- F/ i ph
	stoweidlem51.2	\|- F/ t ph
	stoweidlem51.3	\|- F/ w ph
	stoweidlem51.4	\|- F/_ w V
	stoweidlem51.5	\|- Y = { h e. A \| A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
	stoweidlem51.6	\|- P = ( f e. Y , g e. Y \|-> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) )
	stoweidlem51.7	\|- X = ( seq 1 ( P , U ) ` M )
	stoweidlem51.8	\|- F = ( t e. T \|-> ( i e. ( 1 ... M ) \|-> ( ( U ` i ) ` t ) ) )
	stoweidlem51.9	\|- Z = ( t e. T \|-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )
	stoweidlem51.10	\|- ( ph -> M e. NN )
	stoweidlem51.11	\|- ( ph -> W : ( 1 ... M ) --> V )
	stoweidlem51.12	\|- ( ph -> U : ( 1 ... M ) --> Y )
	stoweidlem51.13	\|- ( ( ph /\ w e. V ) -> w C_ T )
	stoweidlem51.14	\|- ( ph -> D C_ U. ran W )
	stoweidlem51.15	\|- ( ph -> D C_ T )
	stoweidlem51.16	\|- ( ph -> B C_ T )
	stoweidlem51.17	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. ( W ` i ) ( ( U ` i ) ` t ) < ( E / M ) )
	stoweidlem51.18	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. B ( 1 - ( E / M ) ) < ( ( U ` i ) ` t ) )
	stoweidlem51.19	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
	stoweidlem51.20	\|- ( ( ph /\ f e. A ) -> f : T --> RR )
	stoweidlem51.21	\|- ( ph -> T e. _V )
	stoweidlem51.22	\|- ( ph -> E e. RR+ )
	stoweidlem51.23	\|- ( ph -> E < ( 1 / 3 ) )
Assertion	stoweidlem51	\|- ( ph -> E. x ( 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		stoweidlem51.1	\|- F/ i ph
2		stoweidlem51.2	\|- F/ t ph
3		stoweidlem51.3	\|- F/ w ph
4		stoweidlem51.4	\|- F/_ w V
5		stoweidlem51.5	\|- Y = { h e. A \| A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
6		stoweidlem51.6	\|- P = ( f e. Y , g e. Y \|-> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) )
7		stoweidlem51.7	\|- X = ( seq 1 ( P , U ) ` M )
8		stoweidlem51.8	\|- F = ( t e. T \|-> ( i e. ( 1 ... M ) \|-> ( ( U ` i ) ` t ) ) )
9		stoweidlem51.9	\|- Z = ( t e. T \|-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )
10		stoweidlem51.10	\|- ( ph -> M e. NN )
11		stoweidlem51.11	\|- ( ph -> W : ( 1 ... M ) --> V )
12		stoweidlem51.12	\|- ( ph -> U : ( 1 ... M ) --> Y )
13		stoweidlem51.13	\|- ( ( ph /\ w e. V ) -> w C_ T )
14		stoweidlem51.14	\|- ( ph -> D C_ U. ran W )
15		stoweidlem51.15	\|- ( ph -> D C_ T )
16		stoweidlem51.16	\|- ( ph -> B C_ T )
17		stoweidlem51.17	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. ( W ` i ) ( ( U ` i ) ` t ) < ( E / M ) )
18		stoweidlem51.18	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. B ( 1 - ( E / M ) ) < ( ( U ` i ) ` t ) )
19		stoweidlem51.19	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
20		stoweidlem51.20	\|- ( ( ph /\ f e. A ) -> f : T --> RR )
21		stoweidlem51.21	\|- ( ph -> T e. _V )
22		stoweidlem51.22	\|- ( ph -> E e. RR+ )
23		stoweidlem51.23	\|- ( ph -> E < ( 1 / 3 ) )
24		ssrab2	\|- { h e. A \| A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } C_ A
25	5 24	eqsstri	\|- Y C_ A
26		1zzd	\|- ( ph -> 1 e. ZZ )
27	10	nnzd	\|- ( ph -> M e. ZZ )
28	26 27 27	3jca	\|- ( ph -> ( 1 e. ZZ /\ M e. ZZ /\ M e. ZZ ) )
29	10	nnge1d	\|- ( ph -> 1 <_ M )
30	10	nnred	\|- ( ph -> M e. RR )
31	30	leidd	\|- ( ph -> M <_ M )
32	29 31	jca	\|- ( ph -> ( 1 <_ M /\ M <_ M ) )
33		elfz2	\|- ( M e. ( 1 ... M ) <-> ( ( 1 e. ZZ /\ M e. ZZ /\ M e. ZZ ) /\ ( 1 <_ M /\ M <_ M ) ) )
34	28 32 33	sylanbrc	\|- ( ph -> M e. ( 1 ... M ) )
35		eqid	\|- ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) )
36	2 5 35 20 19	stoweidlem16	\|- ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )
37	6 7 34 12 36 21	fmulcl	\|- ( ph -> X e. Y )
38	25 37	sseldi	\|- ( ph -> X e. A )
39	5	eleq2i	\|- ( X e. Y <-> X e. { h e. A \| A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } )
40		nfcv	\|- F/_ h 1
41		nfrab1	\|- F/_ h { h e. A \| A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
42	5 41	nfcxfr	\|- F/_ h Y
43		nfcv	\|- F/_ h ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) )
44	42 42 43	nfmpo	\|- F/_ h ( f e. Y , g e. Y \|-> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) )
45	6 44	nfcxfr	\|- F/_ h P
46		nfcv	\|- F/_ h U
47	40 45 46	nfseq	\|- F/_ h seq 1 ( P , U )
48		nfcv	\|- F/_ h M
49	47 48	nffv	\|- F/_ h ( seq 1 ( P , U ) ` M )
50	7 49	nfcxfr	\|- F/_ h X
51		nfcv	\|- F/_ h A
52		nfcv	\|- F/_ h T
53		nfcv	\|- F/_ h 0
54		nfcv	\|- F/_ h <_
55		nfcv	\|- F/_ h t
56	50 55	nffv	\|- F/_ h ( X ` t )
57	53 54 56	nfbr	\|- F/ h 0 <_ ( X ` t )
58	56 54 40	nfbr	\|- F/ h ( X ` t ) <_ 1
59	57 58	nfan	\|- F/ h ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 )
60	52 59	nfralw	\|- F/ h A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 )
61		nfcv	\|- F/_ t 1
62		nfra1	\|- F/ t A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 )
63		nfcv	\|- F/_ t A
64	62 63	nfrabw	\|- F/_ t { h e. A \| A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
65	5 64	nfcxfr	\|- F/_ t Y
66		nfmpt1	\|- F/_ t ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) )
67	65 65 66	nfmpo	\|- F/_ t ( f e. Y , g e. Y \|-> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) )
68	6 67	nfcxfr	\|- F/_ t P
69		nfcv	\|- F/_ t U
70	61 68 69	nfseq	\|- F/_ t seq 1 ( P , U )
71		nfcv	\|- F/_ t M
72	70 71	nffv	\|- F/_ t ( seq 1 ( P , U ) ` M )
73	7 72	nfcxfr	\|- F/_ t X
74	73	nfeq2	\|- F/ t h = X
75		fveq1	\|- ( h = X -> ( h ` t ) = ( X ` t ) )
76	75	breq2d	\|- ( h = X -> ( 0 <_ ( h ` t ) <-> 0 <_ ( X ` t ) ) )
77	75	breq1d	\|- ( h = X -> ( ( h ` t ) <_ 1 <-> ( X ` t ) <_ 1 ) )
78	76 77	anbi12d	\|- ( h = X -> ( ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) ) )
79	74 78	ralbid	\|- ( h = X -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) ) )
80	50 51 60 79	elrabf	\|- ( X e. { h e. A \| A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } <-> ( X e. A /\ A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) ) )
81	39 80	bitri	\|- ( X e. Y <-> ( X e. A /\ A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) ) )
82	37 81	sylib	\|- ( ph -> ( X e. A /\ A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) ) )
83	82	simprd	\|- ( ph -> A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) )
84		nfv	\|- F/ t i e. ( 1 ... M )
85	2 84	nfan	\|- F/ t ( ph /\ i e. ( 1 ... M ) )
86	12	ffvelrnda	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> ( U ` i ) e. Y )
87		fveq1	\|- ( h = ( U ` i ) -> ( h ` t ) = ( ( U ` i ) ` t ) )
88	87	breq2d	\|- ( h = ( U ` i ) -> ( 0 <_ ( h ` t ) <-> 0 <_ ( ( U ` i ) ` t ) ) )
89	87	breq1d	\|- ( h = ( U ` i ) -> ( ( h ` t ) <_ 1 <-> ( ( U ` i ) ` t ) <_ 1 ) )
90	88 89	anbi12d	\|- ( h = ( U ` i ) -> ( ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> ( 0 <_ ( ( U ` i ) ` t ) /\ ( ( U ` i ) ` t ) <_ 1 ) ) )
91	90	ralbidv	\|- ( h = ( U ` i ) -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( ( U ` i ) ` t ) /\ ( ( U ` i ) ` t ) <_ 1 ) ) )
92	91 5	elrab2	\|- ( ( U ` i ) e. Y <-> ( ( U ` i ) e. A /\ A. t e. T ( 0 <_ ( ( U ` i ) ` t ) /\ ( ( U ` i ) ` t ) <_ 1 ) ) )
93	92	simplbi	\|- ( ( U ` i ) e. Y -> ( U ` i ) e. A )
94	86 93	syl	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> ( U ` i ) e. A )
95		eleq1	\|- ( f = ( U ` i ) -> ( f e. A <-> ( U ` i ) e. A ) )
96	95	anbi2d	\|- ( f = ( U ` i ) -> ( ( ph /\ f e. A ) <-> ( ph /\ ( U ` i ) e. A ) ) )
97		feq1	\|- ( f = ( U ` i ) -> ( f : T --> RR <-> ( U ` i ) : T --> RR ) )
98	96 97	imbi12d	\|- ( f = ( U ` i ) -> ( ( ( ph /\ f e. A ) -> f : T --> RR ) <-> ( ( ph /\ ( U ` i ) e. A ) -> ( U ` i ) : T --> RR ) ) )
99	20	a1i	\|- ( f e. A -> ( ( ph /\ f e. A ) -> f : T --> RR ) )
100	98 99	vtoclga	\|- ( ( U ` i ) e. A -> ( ( ph /\ ( U ` i ) e. A ) -> ( U ` i ) : T --> RR ) )
101	100	anabsi7	\|- ( ( ph /\ ( U ` i ) e. A ) -> ( U ` i ) : T --> RR )
102	94 101	syldan	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> ( U ` i ) : T --> RR )
103	102	adantr	\|- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> ( U ` i ) : T --> RR )
104	11	ffvelrnda	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> ( W ` i ) e. V )
105		simpl	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> ph )
106	105 104	jca	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> ( ph /\ ( W ` i ) e. V ) )
107	4	nfel2	\|- F/ w ( W ` i ) e. V
108	3 107	nfan	\|- F/ w ( ph /\ ( W ` i ) e. V )
109		nfv	\|- F/ w ( W ` i ) C_ T
110	108 109	nfim	\|- F/ w ( ( ph /\ ( W ` i ) e. V ) -> ( W ` i ) C_ T )
111		eleq1	\|- ( w = ( W ` i ) -> ( w e. V <-> ( W ` i ) e. V ) )
112	111	anbi2d	\|- ( w = ( W ` i ) -> ( ( ph /\ w e. V ) <-> ( ph /\ ( W ` i ) e. V ) ) )
113		sseq1	\|- ( w = ( W ` i ) -> ( w C_ T <-> ( W ` i ) C_ T ) )
114	112 113	imbi12d	\|- ( w = ( W ` i ) -> ( ( ( ph /\ w e. V ) -> w C_ T ) <-> ( ( ph /\ ( W ` i ) e. V ) -> ( W ` i ) C_ T ) ) )
115	110 114 13	vtoclg1f	\|- ( ( W ` i ) e. V -> ( ( ph /\ ( W ` i ) e. V ) -> ( W ` i ) C_ T ) )
116	104 106 115	sylc	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> ( W ` i ) C_ T )
117	116	sselda	\|- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> t e. T )
118	103 117	ffvelrnd	\|- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> ( ( U ` i ) ` t ) e. RR )
119	22	rpred	\|- ( ph -> E e. RR )
120	119	ad2antrr	\|- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> E e. RR )
121	30	ad2antrr	\|- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> M e. RR )
122	10	nnne0d	\|- ( ph -> M =/= 0 )
123	122	ad2antrr	\|- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> M =/= 0 )
124	120 121 123	redivcld	\|- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> ( E / M ) e. RR )
125	17	r19.21bi	\|- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> ( ( U ` i ) ` t ) < ( E / M ) )
126		1red	\|- ( ph -> 1 e. RR )
127		0lt1	\|- 0 < 1
128	127	a1i	\|- ( ph -> 0 < 1 )
129	10	nngt0d	\|- ( ph -> 0 < M )
130	22	rpregt0d	\|- ( ph -> ( E e. RR /\ 0 < E ) )
131		lediv2	\|- ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( M e. RR /\ 0 < M ) /\ ( E e. RR /\ 0 < E ) ) -> ( 1 <_ M <-> ( E / M ) <_ ( E / 1 ) ) )
132	126 128 30 129 130 131	syl221anc	\|- ( ph -> ( 1 <_ M <-> ( E / M ) <_ ( E / 1 ) ) )
133	29 132	mpbid	\|- ( ph -> ( E / M ) <_ ( E / 1 ) )
134	22	rpcnd	\|- ( ph -> E e. CC )
135	134	div1d	\|- ( ph -> ( E / 1 ) = E )
136	133 135	breqtrd	\|- ( ph -> ( E / M ) <_ E )
137	136	ad2antrr	\|- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> ( E / M ) <_ E )
138	118 124 120 125 137	ltletrd	\|- ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> ( ( U ` i ) ` t ) < E )
139	138	ex	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> ( t e. ( W ` i ) -> ( ( U ` i ) ` t ) < E ) )
140	85 139	ralrimi	\|- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. ( W ` i ) ( ( U ` i ) ` t ) < E )
141	1 2 5 6 7 8 9 10 11 12 14 15 140 21 20 19 22	stoweidlem48	\|- ( ph -> A. t e. D ( X ` t ) < E )
142	25	sseli	\|- ( f e. Y -> f e. A )
143	142 20	sylan2	\|- ( ( ph /\ f e. Y ) -> f : T --> RR )
144	1 2 65 6 7 8 9 10 12 18 22 23 143 36 21 16	stoweidlem42	\|- ( ph -> A. t e. B ( 1 - E ) < ( X ` t ) )
145	83 141 144	3jca	\|- ( ph -> ( 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 ) ) )
146	38 145	jca	\|- ( ph -> ( 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 ) ) ) )
147		eleq1	\|- ( x = X -> ( x e. A <-> X e. A ) )
148	73	nfeq2	\|- F/ t x = X
149		fveq1	\|- ( x = X -> ( x ` t ) = ( X ` t ) )
150	149	breq2d	\|- ( x = X -> ( 0 <_ ( x ` t ) <-> 0 <_ ( X ` t ) ) )
151	149	breq1d	\|- ( x = X -> ( ( x ` t ) <_ 1 <-> ( X ` t ) <_ 1 ) )
152	150 151	anbi12d	\|- ( x = X -> ( ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) <-> ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) ) )
153	148 152	ralbid	\|- ( x = X -> ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( X ` t ) /\ ( X ` t ) <_ 1 ) ) )
154	149	breq1d	\|- ( x = X -> ( ( x ` t ) < E <-> ( X ` t ) < E ) )
155	148 154	ralbid	\|- ( x = X -> ( A. t e. D ( x ` t ) < E <-> A. t e. D ( X ` t ) < E ) )
156	149	breq2d	\|- ( x = X -> ( ( 1 - E ) < ( x ` t ) <-> ( 1 - E ) < ( X ` t ) ) )
157	148 156	ralbid	\|- ( x = X -> ( A. t e. B ( 1 - E ) < ( x ` t ) <-> A. t e. B ( 1 - E ) < ( X ` t ) ) )
158	153 155 157	3anbi123d	\|- ( x = X -> ( ( 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 ) ) <-> ( 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 ) ) ) )
159	147 158	anbi12d	\|- ( x = X -> ( ( 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 ) ) ) <-> ( 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 ) ) ) ) )
160	159	spcegv	\|- ( X e. A -> ( ( 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 ) ) ) -> E. x ( 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 ) ) ) ) )
161	38 146 160	sylc	\|- ( ph -> E. x ( 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 stoweidlem51

Proof