stoweidlem53

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

	Ref	Expression
Hypotheses	stoweidlem53.1	\|- F/_ t U
	stoweidlem53.2	\|- F/ t ph
	stoweidlem53.3	\|- K = ( topGen ` ran (,) )
	stoweidlem53.4	\|- Q = { h e. A \| ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
	stoweidlem53.5	\|- W = { w e. J \| E. h e. Q w = { t e. T \| 0 < ( h ` t ) } }
	stoweidlem53.6	\|- T = U. J
	stoweidlem53.7	\|- C = ( J Cn K )
	stoweidlem53.8	\|- ( ph -> J e. Comp )
	stoweidlem53.9	\|- ( ph -> A C_ C )
	stoweidlem53.10	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
	stoweidlem53.11	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
	stoweidlem53.12	\|- ( ( ph /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
	stoweidlem53.13	\|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
	stoweidlem53.14	\|- ( ph -> U e. J )
	stoweidlem53.15	\|- ( ph -> ( T \ U ) =/= (/) )
	stoweidlem53.16	\|- ( ph -> Z e. U )
Assertion	stoweidlem53	\|- ( ph -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem53.1	\|- F/_ t U
2		stoweidlem53.2	\|- F/ t ph
3		stoweidlem53.3	\|- K = ( topGen ` ran (,) )
4		stoweidlem53.4	\|- Q = { h e. A \| ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
5		stoweidlem53.5	\|- W = { w e. J \| E. h e. Q w = { t e. T \| 0 < ( h ` t ) } }
6		stoweidlem53.6	\|- T = U. J
7		stoweidlem53.7	\|- C = ( J Cn K )
8		stoweidlem53.8	\|- ( ph -> J e. Comp )
9		stoweidlem53.9	\|- ( ph -> A C_ C )
10		stoweidlem53.10	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
11		stoweidlem53.11	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
12		stoweidlem53.12	\|- ( ( ph /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
13		stoweidlem53.13	\|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
14		stoweidlem53.14	\|- ( ph -> U e. J )
15		stoweidlem53.15	\|- ( ph -> ( T \ U ) =/= (/) )
16		stoweidlem53.16	\|- ( ph -> Z e. U )
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14 16	stoweidlem50	\|- ( ph -> E. u ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) )
18		nfv	\|- F/ t u e. Fin
19		nfcv	\|- F/_ t u
20		nfv	\|- F/ t ( h ` Z ) = 0
21		nfra1	\|- F/ t A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 )
22	20 21	nfan	\|- F/ t ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) )
23		nfcv	\|- F/_ t A
24	22 23	nfrabw	\|- F/_ t { h e. A \| ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
25	4 24	nfcxfr	\|- F/_ t Q
26		nfrab1	\|- F/_ t { t e. T \| 0 < ( h ` t ) }
27	26	nfeq2	\|- F/ t w = { t e. T \| 0 < ( h ` t ) }
28	25 27	nfrexw	\|- F/ t E. h e. Q w = { t e. T \| 0 < ( h ` t ) }
29		nfcv	\|- F/_ t J
30	28 29	nfrabw	\|- F/_ t { w e. J \| E. h e. Q w = { t e. T \| 0 < ( h ` t ) } }
31	5 30	nfcxfr	\|- F/_ t W
32	19 31	nfss	\|- F/ t u C_ W
33		nfcv	\|- F/_ t T
34	33 1	nfdif	\|- F/_ t ( T \ U )
35		nfcv	\|- F/_ t U. u
36	34 35	nfss	\|- F/ t ( T \ U ) C_ U. u
37	18 32 36	nf3an	\|- F/ t ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u )
38	2 37	nfan	\|- F/ t ( ph /\ ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) )
39		nfv	\|- F/ w ph
40		nfv	\|- F/ w u e. Fin
41		nfcv	\|- F/_ w u
42		nfrab1	\|- F/_ w { w e. J \| E. h e. Q w = { t e. T \| 0 < ( h ` t ) } }
43	5 42	nfcxfr	\|- F/_ w W
44	41 43	nfss	\|- F/ w u C_ W
45		nfv	\|- F/ w ( T \ U ) C_ U. u
46	40 44 45	nf3an	\|- F/ w ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u )
47	39 46	nfan	\|- F/ w ( ph /\ ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) )
48		nfv	\|- F/ h ph
49		nfv	\|- F/ h u e. Fin
50		nfcv	\|- F/_ h u
51		nfre1	\|- F/ h E. h e. Q w = { t e. T \| 0 < ( h ` t ) }
52		nfcv	\|- F/_ h J
53	51 52	nfrabw	\|- F/_ h { w e. J \| E. h e. Q w = { t e. T \| 0 < ( h ` t ) } }
54	5 53	nfcxfr	\|- F/_ h W
55	50 54	nfss	\|- F/ h u C_ W
56		nfv	\|- F/ h ( T \ U ) C_ U. u
57	49 55 56	nf3an	\|- F/ h ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u )
58	48 57	nfan	\|- F/ h ( ph /\ ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) )
59		eqid	\|- ( w e. u \|-> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) = ( w e. u \|-> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
60		cmptop	\|- ( J e. Comp -> J e. Top )
61	8 60	syl	\|- ( ph -> J e. Top )
62		retop	\|- ( topGen ` ran (,) ) e. Top
63	3 62	eqeltri	\|- K e. Top
64		cnfex	\|- ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) e. _V )
65	61 63 64	sylancl	\|- ( ph -> ( J Cn K ) e. _V )
66	9 7	sseqtrdi	\|- ( ph -> A C_ ( J Cn K ) )
67	65 66	ssexd	\|- ( ph -> A e. _V )
68	67	adantr	\|- ( ( ph /\ ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) -> A e. _V )
69		simpr1	\|- ( ( ph /\ ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) -> u e. Fin )
70		simpr2	\|- ( ( ph /\ ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) -> u C_ W )
71		simpr3	\|- ( ( ph /\ ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) -> ( T \ U ) C_ U. u )
72	15	adantr	\|- ( ( ph /\ ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) -> ( T \ U ) =/= (/) )
73	38 47 58 4 5 59 68 69 70 71 72	stoweidlem35	\|- ( ( ph /\ ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) -> E. m E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
74	17 73	exlimddv	\|- ( ph -> E. m E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
75		nfv	\|- F/ i ph
76		nfv	\|- F/ i m e. NN
77		nfv	\|- F/ i q : ( 1 ... m ) --> Q
78		nfcv	\|- F/_ i ( T \ U )
79		nfre1	\|- F/ i E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t )
80	78 79	nfralw	\|- F/ i A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t )
81	77 80	nfan	\|- F/ i ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) )
82	76 81	nfan	\|- F/ i ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) )
83	75 82	nfan	\|- F/ i ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
84		nfv	\|- F/ t m e. NN
85		nfcv	\|- F/_ t q
86		nfcv	\|- F/_ t ( 1 ... m )
87	85 86 25	nff	\|- F/ t q : ( 1 ... m ) --> Q
88		nfra1	\|- F/ t A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t )
89	87 88	nfan	\|- F/ t ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) )
90	84 89	nfan	\|- F/ t ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) )
91	2 90	nfan	\|- F/ t ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
92		eqid	\|- ( t e. T \|-> ( ( 1 / m ) x. sum_ y e. ( 1 ... m ) ( ( q ` y ) ` t ) ) ) = ( t e. T \|-> ( ( 1 / m ) x. sum_ y e. ( 1 ... m ) ( ( q ` y ) ` t ) ) )
93		simprl	\|- ( ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) -> m e. NN )
94		simprrl	\|- ( ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) -> q : ( 1 ... m ) --> Q )
95		simprrr	\|- ( ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) -> A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) )
96	66	adantr	\|- ( ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) -> A C_ ( J Cn K ) )
97	10	3adant1r	\|- ( ( ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
98	11	3adant1r	\|- ( ( ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
99	12	adantlr	\|- ( ( ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
100		elssuni	\|- ( U e. J -> U C_ U. J )
101	100 6	sseqtrrdi	\|- ( U e. J -> U C_ T )
102	14 101	syl	\|- ( ph -> U C_ T )
103	102 16	sseldd	\|- ( ph -> Z e. T )
104	103	adantr	\|- ( ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) -> Z e. T )
105	83 91 3 4 92 93 94 95 6 96 97 98 99 104	stoweidlem44	\|- ( ( ph /\ ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )
106	105	ex	\|- ( ph -> ( ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) ) )
107	106	exlimdvv	\|- ( ph -> ( E. m E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) ) )
108	74 107	mpd	\|- ( ph -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )

Metamath Proof Explorer

Theorem stoweidlem53

Proof