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	$⊢ \underline{Ⅎ} h Q$
	stoweidlem36.2	$⊢ \underline{Ⅎ} t H$
	stoweidlem36.3	$⊢ \underline{Ⅎ} t F$
	stoweidlem36.4	$⊢ \underline{Ⅎ} t G$
	stoweidlem36.5	$⊢ Ⅎ t φ$
	stoweidlem36.6	$⊢ K = topGen (ran (.))$
	stoweidlem36.7	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
	stoweidlem36.8	$⊢ T = ⋃ J$
	stoweidlem36.9	$⊢ G = (t \in T ⟼ F (t) F (t))$
	stoweidlem36.10	$⊢ N = sup (ran G ℝ <)$
	stoweidlem36.11	$⊢ H = (t \in T ⟼ \frac{G (t)}{N})$
	stoweidlem36.12	$⊢ φ \to J \in Comp$
	stoweidlem36.13	$⊢ φ \to A \subseteq J Cn K$
	stoweidlem36.14	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem36.15	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem36.16	$⊢ φ \to S \in T$
	stoweidlem36.17	$⊢ φ \to Z \in T$
	stoweidlem36.18	$⊢ φ \to F \in A$
	stoweidlem36.19	$⊢ φ \to F (S) \neq F (Z)$
	stoweidlem36.20	$⊢ φ \to F (Z) = 0$
Assertion	stoweidlem36	$⊢ φ \to \exists h (h \in Q \land 0 < h (S))$

Proof

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

Metamath Proof Explorer

Theorem stoweidlem36

Proof