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