stoweidlem55

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

	Ref	Expression
Hypotheses	stoweidlem55.1	$⊢ \underline{Ⅎ} t U$
	stoweidlem55.2	$⊢ Ⅎ t φ$
	stoweidlem55.3	$⊢ K = topGen (ran (.))$
	stoweidlem55.4	$⊢ φ \to J \in Comp$
	stoweidlem55.5	$⊢ T = ⋃ J$
	stoweidlem55.6	$⊢ C = J Cn K$
	stoweidlem55.7	$⊢ φ \to A \subseteq C$
	stoweidlem55.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem55.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem55.10	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem55.11	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
	stoweidlem55.12	$⊢ φ \to U \in J$
	stoweidlem55.13	$⊢ φ \to Z \in U$
	stoweidlem55.14	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
	stoweidlem55.15	$⊢ W = \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
Assertion	stoweidlem55	$⊢ φ \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		stoweidlem55.1	$⊢ \underline{Ⅎ} t U$
2		stoweidlem55.2	$⊢ Ⅎ t φ$
3		stoweidlem55.3	$⊢ K = topGen (ran (.))$
4		stoweidlem55.4	$⊢ φ \to J \in Comp$
5		stoweidlem55.5	$⊢ T = ⋃ J$
6		stoweidlem55.6	$⊢ C = J Cn K$
7		stoweidlem55.7	$⊢ φ \to A \subseteq C$
8		stoweidlem55.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
9		stoweidlem55.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
10		stoweidlem55.10	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
11		stoweidlem55.11	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
12		stoweidlem55.12	$⊢ φ \to U \in J$
13		stoweidlem55.13	$⊢ φ \to Z \in U$
14		stoweidlem55.14	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
15		stoweidlem55.15	$⊢ W = \{w \in J \| \exists h \in Q w = \{t \in T \| 0 < h (t)\}\}$
16		0re	$⊢ 0 \in ℝ$
17	10	stoweidlem4	$⊢ (φ \land 0 \in ℝ) \to (t \in T ⟼ 0) \in A$
18	16 17	mpan2	$⊢ φ \to (t \in T ⟼ 0) \in A$
19	18	adantr	$⊢ (φ \land T ∖ U = \emptyset) \to (t \in T ⟼ 0) \in A$
20		nfcv	$⊢ \underline{Ⅎ} t T$
21	20 1	nfdif	$⊢ \underline{Ⅎ} t (T ∖ U)$
22		nfcv	$⊢ \underline{Ⅎ} t \emptyset$
23	21 22	nfeq	$⊢ Ⅎ t T ∖ U = \emptyset$
24	2 23	nfan	$⊢ Ⅎ t (φ \land T ∖ U = \emptyset)$
25		0le0	$⊢ 0 \leq 0$
26		0cn	$⊢ 0 \in ℂ$
27		eqid	$⊢ (t \in T ⟼ 0) = (t \in T ⟼ 0)$
28	27	fvmpt2	$⊢ (t \in T \land 0 \in ℂ) \to (t \in T ⟼ 0) (t) = 0$
29	26 28	mpan2	$⊢ t \in T \to (t \in T ⟼ 0) (t) = 0$
30	25 29	breqtrrid	$⊢ t \in T \to 0 \leq (t \in T ⟼ 0) (t)$
31	30	adantl	$⊢ ((φ \land T ∖ U = \emptyset) \land t \in T) \to 0 \leq (t \in T ⟼ 0) (t)$
32		0le1	$⊢ 0 \leq 1$
33	29 32	eqbrtrdi	$⊢ t \in T \to (t \in T ⟼ 0) (t) \leq 1$
34	33	adantl	$⊢ ((φ \land T ∖ U = \emptyset) \land t \in T) \to (t \in T ⟼ 0) (t) \leq 1$
35	31 34	jca	$⊢ ((φ \land T ∖ U = \emptyset) \land t \in T) \to (0 \leq (t \in T ⟼ 0) (t) \land (t \in T ⟼ 0) (t) \leq 1)$
36	35	ex	$⊢ (φ \land T ∖ U = \emptyset) \to (t \in T \to (0 \leq (t \in T ⟼ 0) (t) \land (t \in T ⟼ 0) (t) \leq 1))$
37	24 36	ralrimi	$⊢ (φ \land T ∖ U = \emptyset) \to \forall t \in T (0 \leq (t \in T ⟼ 0) (t) \land (t \in T ⟼ 0) (t) \leq 1)$
38	13 12	jca	$⊢ φ \to (Z \in U \land U \in J)$
39		elunii	$⊢ (Z \in U \land U \in J) \to Z \in ⋃ J$
40	39 5	eleqtrrdi	$⊢ (Z \in U \land U \in J) \to Z \in T$
41		eqidd	$⊢ t = Z \to 0 = 0$
42		c0ex	$⊢ 0 \in V$
43	41 27 42	fvmpt	$⊢ Z \in T \to (t \in T ⟼ 0) (Z) = 0$
44	38 40 43	3syl	$⊢ φ \to (t \in T ⟼ 0) (Z) = 0$
45	44	adantr	$⊢ (φ \land T ∖ U = \emptyset) \to (t \in T ⟼ 0) (Z) = 0$
46	23	rzalf	$⊢ T ∖ U = \emptyset \to \forall t \in (T ∖ U) 0 < (t \in T ⟼ 0) (t)$
47	46	adantl	$⊢ (φ \land T ∖ U = \emptyset) \to \forall t \in (T ∖ U) 0 < (t \in T ⟼ 0) (t)$
48		nfcv	$⊢ \underline{Ⅎ} t p$
49		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ 0)$
50	48 49	nfeq	$⊢ Ⅎ t p = (t \in T ⟼ 0)$
51		fveq1	$⊢ p = (t \in T ⟼ 0) \to p (t) = (t \in T ⟼ 0) (t)$
52	51	breq2d	$⊢ p = (t \in T ⟼ 0) \to (0 \leq p (t) \leftrightarrow 0 \leq (t \in T ⟼ 0) (t))$
53	51	breq1d	$⊢ p = (t \in T ⟼ 0) \to (p (t) \leq 1 \leftrightarrow (t \in T ⟼ 0) (t) \leq 1)$
54	52 53	anbi12d	$⊢ p = (t \in T ⟼ 0) \to ((0 \leq p (t) \land p (t) \leq 1) \leftrightarrow (0 \leq (t \in T ⟼ 0) (t) \land (t \in T ⟼ 0) (t) \leq 1))$
55	50 54	ralbid	$⊢ p = (t \in T ⟼ 0) \to (\forall t \in T (0 \leq p (t) \land p (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq (t \in T ⟼ 0) (t) \land (t \in T ⟼ 0) (t) \leq 1))$
56		fveq1	$⊢ p = (t \in T ⟼ 0) \to p (Z) = (t \in T ⟼ 0) (Z)$
57	56	eqeq1d	$⊢ p = (t \in T ⟼ 0) \to (p (Z) = 0 \leftrightarrow (t \in T ⟼ 0) (Z) = 0)$
58	51	breq2d	$⊢ p = (t \in T ⟼ 0) \to (0 < p (t) \leftrightarrow 0 < (t \in T ⟼ 0) (t))$
59	50 58	ralbid	$⊢ p = (t \in T ⟼ 0) \to (\forall t \in (T ∖ U) 0 < p (t) \leftrightarrow \forall t \in (T ∖ U) 0 < (t \in T ⟼ 0) (t))$
60	55 57 59	3anbi123d	$⊢ p = (t \in T ⟼ 0) \to ((\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)) \leftrightarrow (\forall t \in T (0 \leq (t \in T ⟼ 0) (t) \land (t \in T ⟼ 0) (t) \leq 1) \land (t \in T ⟼ 0) (Z) = 0 \land \forall t \in (T ∖ U) 0 < (t \in T ⟼ 0) (t)))$
61	60	rspcev	$⊢ ((t \in T ⟼ 0) \in A \land (\forall t \in T (0 \leq (t \in T ⟼ 0) (t) \land (t \in T ⟼ 0) (t) \leq 1) \land (t \in T ⟼ 0) (Z) = 0 \land \forall t \in (T ∖ U) 0 < (t \in T ⟼ 0) (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))$
62	19 37 45 47 61	syl13anc	$⊢ (φ \land T ∖ U = \emptyset) \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))$
63	23	nfn	$⊢ Ⅎ t \neg T ∖ U = \emptyset$
64	2 63	nfan	$⊢ Ⅎ t (φ \land \neg T ∖ U = \emptyset)$
65	4	adantr	$⊢ (φ \land \neg T ∖ U = \emptyset) \to J \in Comp$
66	7	adantr	$⊢ (φ \land \neg T ∖ U = \emptyset) \to A \subseteq C$
67	8	3adant1r	$⊢ ((φ \land \neg T ∖ U = \emptyset) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
68	9	3adant1r	$⊢ ((φ \land \neg T ∖ U = \emptyset) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
69	10	adantlr	$⊢ ((φ \land \neg T ∖ U = \emptyset) \land x \in ℝ) \to (t \in T ⟼ x) \in A$
70	11	adantlr	$⊢ ((φ \land \neg T ∖ U = \emptyset) \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
71	12	adantr	$⊢ (φ \land \neg T ∖ U = \emptyset) \to U \in J$
72		neqne	$⊢ \neg T ∖ U = \emptyset \to T ∖ U \neq \emptyset$
73	72	adantl	$⊢ (φ \land \neg T ∖ U = \emptyset) \to T ∖ U \neq \emptyset$
74	13	adantr	$⊢ (φ \land \neg T ∖ U = \emptyset) \to Z \in U$
75	1 64 3 14 15 5 6 65 66 67 68 69 70 71 73 74	stoweidlem53	$⊢ (φ \land \neg T ∖ U = \emptyset) \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))$
76	62 75	pm2.61dan	$⊢ φ \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 stoweidlem55

Proof