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	$⊢ \underline{Ⅎ} t U$
	stoweidlem53.2	$⊢ Ⅎ t φ$
	stoweidlem53.3	$⊢ K = topGen (ran (.))$
	stoweidlem53.4	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
	stoweidlem53.5	$⊢ W = \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
	stoweidlem53.6	$⊢ T = ⋃ J$
	stoweidlem53.7	$⊢ C = J Cn K$
	stoweidlem53.8	$⊢ φ \to J \in Comp$
	stoweidlem53.9	$⊢ φ \to A \subseteq C$
	stoweidlem53.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem53.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem53.12	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem53.13	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
	stoweidlem53.14	$⊢ φ \to U \in J$
	stoweidlem53.15	$⊢ φ \to T ∖ U \neq \emptyset$
	stoweidlem53.16	$⊢ φ \to Z \in U$
Assertion	stoweidlem53	$⊢ φ \to \exists p \in A (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \land p (Z) = 0 \land \forall t \in (T ∖ U) 0 < p (t))$

Proof

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

Metamath Proof Explorer

Theorem stoweidlem53

Proof