stoweidlem36

Description: This lemma is used to prove the existence of a function p_t as in Lemma 1 of BrosowskiDeutsh p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function p in the subalgebra, such that p_t ( t_0 ) = 0 , p_t ( t ) > 0, and 0 <= p_t <= 1. Z is used for t_0 , S is used for t e. T - U , h is used for p_t . G is used for (h_t)^2 and the final h is a normalized version of G ( divided by its norm, see the variable N ). (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem36.1	\|- F/_ h Q
	stoweidlem36.2	\|- F/_ t H
	stoweidlem36.3	\|- F/_ t F
	stoweidlem36.4	\|- F/_ t G
	stoweidlem36.5	\|- F/ t ph
	stoweidlem36.6	\|- K = ( topGen ` ran (,) )
	stoweidlem36.7	\|- Q = { h e. A \| ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
	stoweidlem36.8	\|- T = U. J
	stoweidlem36.9	\|- G = ( t e. T \|-> ( ( F ` t ) x. ( F ` t ) ) )
	stoweidlem36.10	\|- N = sup ( ran G , RR , < )
	stoweidlem36.11	\|- H = ( t e. T \|-> ( ( G ` t ) / N ) )
	stoweidlem36.12	\|- ( ph -> J e. Comp )
	stoweidlem36.13	\|- ( ph -> A C_ ( J Cn K ) )
	stoweidlem36.14	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
	stoweidlem36.15	\|- ( ( ph /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
	stoweidlem36.16	\|- ( ph -> S e. T )
	stoweidlem36.17	\|- ( ph -> Z e. T )
	stoweidlem36.18	\|- ( ph -> F e. A )
	stoweidlem36.19	\|- ( ph -> ( F ` S ) =/= ( F ` Z ) )
	stoweidlem36.20	\|- ( ph -> ( F ` Z ) = 0 )
Assertion	stoweidlem36	\|- ( ph -> E. h ( h e. Q /\ 0 < ( h ` S ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem36.1	\|- F/_ h Q
2		stoweidlem36.2	\|- F/_ t H
3		stoweidlem36.3	\|- F/_ t F
4		stoweidlem36.4	\|- F/_ t G
5		stoweidlem36.5	\|- F/ t ph
6		stoweidlem36.6	\|- K = ( topGen ` ran (,) )
7		stoweidlem36.7	\|- Q = { h e. A \| ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
8		stoweidlem36.8	\|- T = U. J
9		stoweidlem36.9	\|- G = ( t e. T \|-> ( ( F ` t ) x. ( F ` t ) ) )
10		stoweidlem36.10	\|- N = sup ( ran G , RR , < )
11		stoweidlem36.11	\|- H = ( t e. T \|-> ( ( G ` t ) / N ) )
12		stoweidlem36.12	\|- ( ph -> J e. Comp )
13		stoweidlem36.13	\|- ( ph -> A C_ ( J Cn K ) )
14		stoweidlem36.14	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
15		stoweidlem36.15	\|- ( ( ph /\ x e. RR ) -> ( t e. T \|-> x ) e. A )
16		stoweidlem36.16	\|- ( ph -> S e. T )
17		stoweidlem36.17	\|- ( ph -> Z e. T )
18		stoweidlem36.18	\|- ( ph -> F e. A )
19		stoweidlem36.19	\|- ( ph -> ( F ` S ) =/= ( F ` Z ) )
20		stoweidlem36.20	\|- ( ph -> ( F ` Z ) = 0 )
21		eqid	\|- ( J Cn K ) = ( J Cn K )
22	3	nfeq2	\|- F/ t f = F
23	3	nfeq2	\|- F/ t g = F
24	22 23 14	stoweidlem6	\|- ( ( ph /\ F e. A /\ F e. A ) -> ( t e. T \|-> ( ( F ` t ) x. ( F ` t ) ) ) e. A )
25	18 18 24	mpd3an23	\|- ( ph -> ( t e. T \|-> ( ( F ` t ) x. ( F ` t ) ) ) e. A )
26	9 25	eqeltrid	\|- ( ph -> G e. A )
27	13 26	sseldd	\|- ( ph -> G e. ( J Cn K ) )
28	6 8 21 27	fcnre	\|- ( ph -> G : T --> RR )
29	28	ffvelrnda	\|- ( ( ph /\ t e. T ) -> ( G ` t ) e. RR )
30	29	recnd	\|- ( ( ph /\ t e. T ) -> ( G ` t ) e. CC )
31	16	ne0d	\|- ( ph -> T =/= (/) )
32	8 6 12 27 31	cncmpmax	\|- ( ph -> ( sup ( ran G , RR , < ) e. ran G /\ sup ( ran G , RR , < ) e. RR /\ A. s e. T ( G ` s ) <_ sup ( ran G , RR , < ) ) )
33	32	simp2d	\|- ( ph -> sup ( ran G , RR , < ) e. RR )
34	10 33	eqeltrid	\|- ( ph -> N e. RR )
35	34	recnd	\|- ( ph -> N e. CC )
36	35	adantr	\|- ( ( ph /\ t e. T ) -> N e. CC )
37		0red	\|- ( ph -> 0 e. RR )
38	28 16	ffvelrnd	\|- ( ph -> ( G ` S ) e. RR )
39	13 18	sseldd	\|- ( ph -> F e. ( J Cn K ) )
40	6 8 21 39	fcnre	\|- ( ph -> F : T --> RR )
41	40 16	ffvelrnd	\|- ( ph -> ( F ` S ) e. RR )
42	19 20	neeqtrd	\|- ( ph -> ( F ` S ) =/= 0 )
43	41 42	msqgt0d	\|- ( ph -> 0 < ( ( F ` S ) x. ( F ` S ) ) )
44	41 41	remulcld	\|- ( ph -> ( ( F ` S ) x. ( F ` S ) ) e. RR )
45		nfcv	\|- F/_ t S
46	3 45	nffv	\|- F/_ t ( F ` S )
47		nfcv	\|- F/_ t x.
48	46 47 46	nfov	\|- F/_ t ( ( F ` S ) x. ( F ` S ) )
49		fveq2	\|- ( t = S -> ( F ` t ) = ( F ` S ) )
50	49 49	oveq12d	\|- ( t = S -> ( ( F ` t ) x. ( F ` t ) ) = ( ( F ` S ) x. ( F ` S ) ) )
51	45 48 50 9	fvmptf	\|- ( ( S e. T /\ ( ( F ` S ) x. ( F ` S ) ) e. RR ) -> ( G ` S ) = ( ( F ` S ) x. ( F ` S ) ) )
52	16 44 51	syl2anc	\|- ( ph -> ( G ` S ) = ( ( F ` S ) x. ( F ` S ) ) )
53	43 52	breqtrrd	\|- ( ph -> 0 < ( G ` S ) )
54	32	simp3d	\|- ( ph -> A. s e. T ( G ` s ) <_ sup ( ran G , RR , < ) )
55		fveq2	\|- ( s = S -> ( G ` s ) = ( G ` S ) )
56	55	breq1d	\|- ( s = S -> ( ( G ` s ) <_ sup ( ran G , RR , < ) <-> ( G ` S ) <_ sup ( ran G , RR , < ) ) )
57	56	rspccva	\|- ( ( A. s e. T ( G ` s ) <_ sup ( ran G , RR , < ) /\ S e. T ) -> ( G ` S ) <_ sup ( ran G , RR , < ) )
58	54 16 57	syl2anc	\|- ( ph -> ( G ` S ) <_ sup ( ran G , RR , < ) )
59	37 38 33 53 58	ltletrd	\|- ( ph -> 0 < sup ( ran G , RR , < ) )
60	59	gt0ne0d	\|- ( ph -> sup ( ran G , RR , < ) =/= 0 )
61	10	neeq1i	\|- ( N =/= 0 <-> sup ( ran G , RR , < ) =/= 0 )
62	60 61	sylibr	\|- ( ph -> N =/= 0 )
63	62	adantr	\|- ( ( ph /\ t e. T ) -> N =/= 0 )
64	30 36 63	divrecd	\|- ( ( ph /\ t e. T ) -> ( ( G ` t ) / N ) = ( ( G ` t ) x. ( 1 / N ) ) )
65		simpr	\|- ( ( ph /\ t e. T ) -> t e. T )
66	34 62	rereccld	\|- ( ph -> ( 1 / N ) e. RR )
67	66	adantr	\|- ( ( ph /\ t e. T ) -> ( 1 / N ) e. RR )
68		eqid	\|- ( t e. T \|-> ( 1 / N ) ) = ( t e. T \|-> ( 1 / N ) )
69	68	fvmpt2	\|- ( ( t e. T /\ ( 1 / N ) e. RR ) -> ( ( t e. T \|-> ( 1 / N ) ) ` t ) = ( 1 / N ) )
70	65 67 69	syl2anc	\|- ( ( ph /\ t e. T ) -> ( ( t e. T \|-> ( 1 / N ) ) ` t ) = ( 1 / N ) )
71	70	oveq2d	\|- ( ( ph /\ t e. T ) -> ( ( G ` t ) x. ( ( t e. T \|-> ( 1 / N ) ) ` t ) ) = ( ( G ` t ) x. ( 1 / N ) ) )
72	64 71	eqtr4d	\|- ( ( ph /\ t e. T ) -> ( ( G ` t ) / N ) = ( ( G ` t ) x. ( ( t e. T \|-> ( 1 / N ) ) ` t ) ) )
73	5 72	mpteq2da	\|- ( ph -> ( t e. T \|-> ( ( G ` t ) / N ) ) = ( t e. T \|-> ( ( G ` t ) x. ( ( t e. T \|-> ( 1 / N ) ) ` t ) ) ) )
74	11 73	syl5eq	\|- ( ph -> H = ( t e. T \|-> ( ( G ` t ) x. ( ( t e. T \|-> ( 1 / N ) ) ` t ) ) ) )
75	15	stoweidlem4	\|- ( ( ph /\ ( 1 / N ) e. RR ) -> ( t e. T \|-> ( 1 / N ) ) e. A )
76	66 75	mpdan	\|- ( ph -> ( t e. T \|-> ( 1 / N ) ) e. A )
77	4	nfeq2	\|- F/ t f = G
78		nfmpt1	\|- F/_ t ( t e. T \|-> ( 1 / N ) )
79	78	nfeq2	\|- F/ t g = ( t e. T \|-> ( 1 / N ) )
80	77 79 14	stoweidlem6	\|- ( ( ph /\ G e. A /\ ( t e. T \|-> ( 1 / N ) ) e. A ) -> ( t e. T \|-> ( ( G ` t ) x. ( ( t e. T \|-> ( 1 / N ) ) ` t ) ) ) e. A )
81	26 76 80	mpd3an23	\|- ( ph -> ( t e. T \|-> ( ( G ` t ) x. ( ( t e. T \|-> ( 1 / N ) ) ` t ) ) ) e. A )
82	74 81	eqeltrd	\|- ( ph -> H e. A )
83	28 17	ffvelrnd	\|- ( ph -> ( G ` Z ) e. RR )
84	83 34 62	redivcld	\|- ( ph -> ( ( G ` Z ) / N ) e. RR )
85		nfcv	\|- F/_ t Z
86	4 85	nffv	\|- F/_ t ( G ` Z )
87		nfcv	\|- F/_ t /
88		nfcv	\|- F/_ t N
89	86 87 88	nfov	\|- F/_ t ( ( G ` Z ) / N )
90		fveq2	\|- ( t = Z -> ( G ` t ) = ( G ` Z ) )
91	90	oveq1d	\|- ( t = Z -> ( ( G ` t ) / N ) = ( ( G ` Z ) / N ) )
92	85 89 91 11	fvmptf	\|- ( ( Z e. T /\ ( ( G ` Z ) / N ) e. RR ) -> ( H ` Z ) = ( ( G ` Z ) / N ) )
93	17 84 92	syl2anc	\|- ( ph -> ( H ` Z ) = ( ( G ` Z ) / N ) )
94		0re	\|- 0 e. RR
95	20 94	eqeltrdi	\|- ( ph -> ( F ` Z ) e. RR )
96	95 95	remulcld	\|- ( ph -> ( ( F ` Z ) x. ( F ` Z ) ) e. RR )
97	3 85	nffv	\|- F/_ t ( F ` Z )
98	97 47 97	nfov	\|- F/_ t ( ( F ` Z ) x. ( F ` Z ) )
99		fveq2	\|- ( t = Z -> ( F ` t ) = ( F ` Z ) )
100	99 99	oveq12d	\|- ( t = Z -> ( ( F ` t ) x. ( F ` t ) ) = ( ( F ` Z ) x. ( F ` Z ) ) )
101	85 98 100 9	fvmptf	\|- ( ( Z e. T /\ ( ( F ` Z ) x. ( F ` Z ) ) e. RR ) -> ( G ` Z ) = ( ( F ` Z ) x. ( F ` Z ) ) )
102	17 96 101	syl2anc	\|- ( ph -> ( G ` Z ) = ( ( F ` Z ) x. ( F ` Z ) ) )
103	20 20	oveq12d	\|- ( ph -> ( ( F ` Z ) x. ( F ` Z ) ) = ( 0 x. 0 ) )
104		0cn	\|- 0 e. CC
105	104	mul02i	\|- ( 0 x. 0 ) = 0
106	103 105	eqtrdi	\|- ( ph -> ( ( F ` Z ) x. ( F ` Z ) ) = 0 )
107	102 106	eqtrd	\|- ( ph -> ( G ` Z ) = 0 )
108	107	oveq1d	\|- ( ph -> ( ( G ` Z ) / N ) = ( 0 / N ) )
109	35 62	div0d	\|- ( ph -> ( 0 / N ) = 0 )
110	93 108 109	3eqtrd	\|- ( ph -> ( H ` Z ) = 0 )
111	40	ffvelrnda	\|- ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
112	111	msqge0d	\|- ( ( ph /\ t e. T ) -> 0 <_ ( ( F ` t ) x. ( F ` t ) ) )
113	111 111	remulcld	\|- ( ( ph /\ t e. T ) -> ( ( F ` t ) x. ( F ` t ) ) e. RR )
114	9	fvmpt2	\|- ( ( t e. T /\ ( ( F ` t ) x. ( F ` t ) ) e. RR ) -> ( G ` t ) = ( ( F ` t ) x. ( F ` t ) ) )
115	65 113 114	syl2anc	\|- ( ( ph /\ t e. T ) -> ( G ` t ) = ( ( F ` t ) x. ( F ` t ) ) )
116	112 115	breqtrrd	\|- ( ( ph /\ t e. T ) -> 0 <_ ( G ` t ) )
117	34	adantr	\|- ( ( ph /\ t e. T ) -> N e. RR )
118	59 10	breqtrrdi	\|- ( ph -> 0 < N )
119	118	adantr	\|- ( ( ph /\ t e. T ) -> 0 < N )
120		divge0	\|- ( ( ( ( G ` t ) e. RR /\ 0 <_ ( G ` t ) ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( ( G ` t ) / N ) )
121	29 116 117 119 120	syl22anc	\|- ( ( ph /\ t e. T ) -> 0 <_ ( ( G ` t ) / N ) )
122	29 117 63	redivcld	\|- ( ( ph /\ t e. T ) -> ( ( G ` t ) / N ) e. RR )
123	11	fvmpt2	\|- ( ( t e. T /\ ( ( G ` t ) / N ) e. RR ) -> ( H ` t ) = ( ( G ` t ) / N ) )
124	65 122 123	syl2anc	\|- ( ( ph /\ t e. T ) -> ( H ` t ) = ( ( G ` t ) / N ) )
125	121 124	breqtrrd	\|- ( ( ph /\ t e. T ) -> 0 <_ ( H ` t ) )
126	30	div1d	\|- ( ( ph /\ t e. T ) -> ( ( G ` t ) / 1 ) = ( G ` t ) )
127		fveq2	\|- ( s = t -> ( G ` s ) = ( G ` t ) )
128	127	breq1d	\|- ( s = t -> ( ( G ` s ) <_ sup ( ran G , RR , < ) <-> ( G ` t ) <_ sup ( ran G , RR , < ) ) )
129	128	rspccva	\|- ( ( A. s e. T ( G ` s ) <_ sup ( ran G , RR , < ) /\ t e. T ) -> ( G ` t ) <_ sup ( ran G , RR , < ) )
130	54 129	sylan	\|- ( ( ph /\ t e. T ) -> ( G ` t ) <_ sup ( ran G , RR , < ) )
131	130 10	breqtrrdi	\|- ( ( ph /\ t e. T ) -> ( G ` t ) <_ N )
132	126 131	eqbrtrd	\|- ( ( ph /\ t e. T ) -> ( ( G ` t ) / 1 ) <_ N )
133		1red	\|- ( ( ph /\ t e. T ) -> 1 e. RR )
134		0lt1	\|- 0 < 1
135	134	a1i	\|- ( ( ph /\ t e. T ) -> 0 < 1 )
136		lediv23	\|- ( ( ( G ` t ) e. RR /\ ( N e. RR /\ 0 < N ) /\ ( 1 e. RR /\ 0 < 1 ) ) -> ( ( ( G ` t ) / N ) <_ 1 <-> ( ( G ` t ) / 1 ) <_ N ) )
137	29 117 119 133 135 136	syl122anc	\|- ( ( ph /\ t e. T ) -> ( ( ( G ` t ) / N ) <_ 1 <-> ( ( G ` t ) / 1 ) <_ N ) )
138	132 137	mpbird	\|- ( ( ph /\ t e. T ) -> ( ( G ` t ) / N ) <_ 1 )
139	124 138	eqbrtrd	\|- ( ( ph /\ t e. T ) -> ( H ` t ) <_ 1 )
140	125 139	jca	\|- ( ( ph /\ t e. T ) -> ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) )
141	140	ex	\|- ( ph -> ( t e. T -> ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) ) )
142	5 141	ralrimi	\|- ( ph -> A. t e. T ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) )
143	110 142	jca	\|- ( ph -> ( ( H ` Z ) = 0 /\ A. t e. T ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) ) )
144		fveq1	\|- ( h = H -> ( h ` Z ) = ( H ` Z ) )
145	144	eqeq1d	\|- ( h = H -> ( ( h ` Z ) = 0 <-> ( H ` Z ) = 0 ) )
146	2	nfeq2	\|- F/ t h = H
147		fveq1	\|- ( h = H -> ( h ` t ) = ( H ` t ) )
148	147	breq2d	\|- ( h = H -> ( 0 <_ ( h ` t ) <-> 0 <_ ( H ` t ) ) )
149	147	breq1d	\|- ( h = H -> ( ( h ` t ) <_ 1 <-> ( H ` t ) <_ 1 ) )
150	148 149	anbi12d	\|- ( h = H -> ( ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) ) )
151	146 150	ralbid	\|- ( h = H -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) ) )
152	145 151	anbi12d	\|- ( h = H -> ( ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) <-> ( ( H ` Z ) = 0 /\ A. t e. T ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) ) ) )
153	152	elrab	\|- ( H e. { h e. A \| ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) } <-> ( H e. A /\ ( ( H ` Z ) = 0 /\ A. t e. T ( 0 <_ ( H ` t ) /\ ( H ` t ) <_ 1 ) ) ) )
154	82 143 153	sylanbrc	\|- ( ph -> H e. { h e. A \| ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) } )
155	154 7	eleqtrrdi	\|- ( ph -> H e. Q )
156	38 34 53 118	divgt0d	\|- ( ph -> 0 < ( ( G ` S ) / N ) )
157	38 34 62	redivcld	\|- ( ph -> ( ( G ` S ) / N ) e. RR )
158	4 45	nffv	\|- F/_ t ( G ` S )
159	158 87 88	nfov	\|- F/_ t ( ( G ` S ) / N )
160		fveq2	\|- ( t = S -> ( G ` t ) = ( G ` S ) )
161	160	oveq1d	\|- ( t = S -> ( ( G ` t ) / N ) = ( ( G ` S ) / N ) )
162	45 159 161 11	fvmptf	\|- ( ( S e. T /\ ( ( G ` S ) / N ) e. RR ) -> ( H ` S ) = ( ( G ` S ) / N ) )
163	16 157 162	syl2anc	\|- ( ph -> ( H ` S ) = ( ( G ` S ) / N ) )
164	156 163	breqtrrd	\|- ( ph -> 0 < ( H ` S ) )
165		nfcv	\|- F/_ h H
166	1	nfel2	\|- F/ h H e. Q
167		nfv	\|- F/ h 0 < ( H ` S )
168	166 167	nfan	\|- F/ h ( H e. Q /\ 0 < ( H ` S ) )
169		eleq1	\|- ( h = H -> ( h e. Q <-> H e. Q ) )
170		fveq1	\|- ( h = H -> ( h ` S ) = ( H ` S ) )
171	170	breq2d	\|- ( h = H -> ( 0 < ( h ` S ) <-> 0 < ( H ` S ) ) )
172	169 171	anbi12d	\|- ( h = H -> ( ( h e. Q /\ 0 < ( h ` S ) ) <-> ( H e. Q /\ 0 < ( H ` S ) ) ) )
173	165 168 172	spcegf	\|- ( H e. Q -> ( ( H e. Q /\ 0 < ( H ` S ) ) -> E. h ( h e. Q /\ 0 < ( h ` S ) ) ) )
174	173	anabsi5	\|- ( ( H e. Q /\ 0 < ( H ` S ) ) -> E. h ( h e. Q /\ 0 < ( h ` S ) ) )
175	155 164 174	syl2anc	\|- ( ph -> E. h ( h e. Q /\ 0 < ( h ` S ) ) )

Metamath Proof Explorer

Theorem stoweidlem36

Proof