stoweidlem43

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_t in the subalgebra, such that p_t( t_0 ) = 0 , p_t ( t ) > 0, and 0 <= p_t <= 1. Hera Z is used for t_0 , S is used for t e. T - U , h is used for p_t. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem43.1	$⊢ Ⅎ g φ$
	stoweidlem43.2	$⊢ Ⅎ t φ$
	stoweidlem43.3	$⊢ \underline{Ⅎ} h Q$
	stoweidlem43.4	$⊢ K = topGen (ran (.))$
	stoweidlem43.5	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
	stoweidlem43.6	$⊢ T = ⋃ J$
	stoweidlem43.7	$⊢ φ \to J \in Comp$
	stoweidlem43.8	$⊢ φ \to A \subseteq J Cn K$
	stoweidlem43.9	$⊢ (φ \land f \in A \land l \in A) \to (t \in T ⟼ f (t) + l (t)) \in A$
	stoweidlem43.10	$⊢ (φ \land f \in A \land l \in A) \to (t \in T ⟼ f (t) l (t)) \in A$
	stoweidlem43.11	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem43.12	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists g \in A g (r) \neq g (t)$
	stoweidlem43.13	$⊢ φ \to U \in J$
	stoweidlem43.14	$⊢ φ \to Z \in U$
	stoweidlem43.15	$⊢ φ \to S \in (T ∖ U)$
Assertion	stoweidlem43	$⊢ φ \to \exists h (h \in Q \land 0 < h (S))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem43.1	$⊢ Ⅎ g φ$
2		stoweidlem43.2	$⊢ Ⅎ t φ$
3		stoweidlem43.3	$⊢ \underline{Ⅎ} h Q$
4		stoweidlem43.4	$⊢ K = topGen (ran (.))$
5		stoweidlem43.5	$⊢ Q = \{h \in A \| (h (Z) = 0 \land \forall t \in T (0 \leq h (t) \land h (t) \leq 1))\}$
6		stoweidlem43.6	$⊢ T = ⋃ J$
7		stoweidlem43.7	$⊢ φ \to J \in Comp$
8		stoweidlem43.8	$⊢ φ \to A \subseteq J Cn K$
9		stoweidlem43.9	$⊢ (φ \land f \in A \land l \in A) \to (t \in T ⟼ f (t) + l (t)) \in A$
10		stoweidlem43.10	$⊢ (φ \land f \in A \land l \in A) \to (t \in T ⟼ f (t) l (t)) \in A$
11		stoweidlem43.11	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
12		stoweidlem43.12	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists g \in A g (r) \neq g (t)$
13		stoweidlem43.13	$⊢ φ \to U \in J$
14		stoweidlem43.14	$⊢ φ \to Z \in U$
15		stoweidlem43.15	$⊢ φ \to S \in (T ∖ U)$
16		nfv	$⊢ Ⅎ g \exists f (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)$
17	15	eldifad	$⊢ φ \to S \in T$
18		elunii	$⊢ (Z \in U \land U \in J) \to Z \in ⋃ J$
19	14 13 18	syl2anc	$⊢ φ \to Z \in ⋃ J$
20	19 6	eleqtrrdi	$⊢ φ \to Z \in T$
21	15	eldifbd	$⊢ φ \to \neg S \in U$
22		nelne2	$⊢ (Z \in U \land \neg S \in U) \to Z \neq S$
23	14 21 22	syl2anc	$⊢ φ \to Z \neq S$
24	23	necomd	$⊢ φ \to S \neq Z$
25	17 20 24	3jca	$⊢ φ \to (S \in T \land Z \in T \land S \neq Z)$
26		simpr2	$⊢ (φ \land (S \in T \land Z \in T \land S \neq Z)) \to Z \in T$
27		nfv	$⊢ Ⅎ t (S \in T \land Z \in T \land S \neq Z)$
28	2 27	nfan	$⊢ Ⅎ t (φ \land (S \in T \land Z \in T \land S \neq Z))$
29		nfv	$⊢ Ⅎ t \exists g \in A g (S) \neq g (Z)$
30	28 29	nfim	$⊢ Ⅎ t ((φ \land (S \in T \land Z \in T \land S \neq Z)) \to \exists g \in A g (S) \neq g (Z))$
31		eleq1	$⊢ t = Z \to (t \in T \leftrightarrow Z \in T)$
32		neeq2	$⊢ t = Z \to (S \neq t \leftrightarrow S \neq Z)$
33	31 32	3anbi23d	$⊢ t = Z \to ((S \in T \land t \in T \land S \neq t) \leftrightarrow (S \in T \land Z \in T \land S \neq Z))$
34	33	anbi2d	$⊢ t = Z \to ((φ \land (S \in T \land t \in T \land S \neq t)) \leftrightarrow (φ \land (S \in T \land Z \in T \land S \neq Z)))$
35		fveq2	$⊢ t = Z \to g (t) = g (Z)$
36	35	neeq2d	$⊢ t = Z \to (g (S) \neq g (t) \leftrightarrow g (S) \neq g (Z))$
37	36	rexbidv	$⊢ t = Z \to (\exists g \in A g (S) \neq g (t) \leftrightarrow \exists g \in A g (S) \neq g (Z))$
38	34 37	imbi12d	$⊢ t = Z \to (((φ \land (S \in T \land t \in T \land S \neq t)) \to \exists g \in A g (S) \neq g (t)) \leftrightarrow ((φ \land (S \in T \land Z \in T \land S \neq Z)) \to \exists g \in A g (S) \neq g (Z)))$
39		simpr1	$⊢ (φ \land (S \in T \land t \in T \land S \neq t)) \to S \in T$
40		eleq1	$⊢ r = S \to (r \in T \leftrightarrow S \in T)$
41		neeq1	$⊢ r = S \to (r \neq t \leftrightarrow S \neq t)$
42	40 41	3anbi13d	$⊢ r = S \to ((r \in T \land t \in T \land r \neq t) \leftrightarrow (S \in T \land t \in T \land S \neq t))$
43	42	anbi2d	$⊢ r = S \to ((φ \land (r \in T \land t \in T \land r \neq t)) \leftrightarrow (φ \land (S \in T \land t \in T \land S \neq t)))$
44		fveq2	$⊢ r = S \to g (r) = g (S)$
45	44	neeq1d	$⊢ r = S \to (g (r) \neq g (t) \leftrightarrow g (S) \neq g (t))$
46	45	rexbidv	$⊢ r = S \to (\exists g \in A g (r) \neq g (t) \leftrightarrow \exists g \in A g (S) \neq g (t))$
47	43 46	imbi12d	$⊢ r = S \to (((φ \land (r \in T \land t \in T \land r \neq t)) \to \exists g \in A g (r) \neq g (t)) \leftrightarrow ((φ \land (S \in T \land t \in T \land S \neq t)) \to \exists g \in A g (S) \neq g (t)))$
48	12	a1i	$⊢ r \in T \to ((φ \land (r \in T \land t \in T \land r \neq t)) \to \exists g \in A g (r) \neq g (t))$
49	47 48	vtoclga	$⊢ S \in T \to ((φ \land (S \in T \land t \in T \land S \neq t)) \to \exists g \in A g (S) \neq g (t))$
50	39 49	mpcom	$⊢ (φ \land (S \in T \land t \in T \land S \neq t)) \to \exists g \in A g (S) \neq g (t)$
51	30 38 50	vtoclg1f	$⊢ Z \in T \to ((φ \land (S \in T \land Z \in T \land S \neq Z)) \to \exists g \in A g (S) \neq g (Z))$
52	26 51	mpcom	$⊢ (φ \land (S \in T \land Z \in T \land S \neq Z)) \to \exists g \in A g (S) \neq g (Z)$
53		df-rex	$⊢ \exists g \in A g (S) \neq g (Z) \leftrightarrow \exists g (g \in A \land g (S) \neq g (Z))$
54	52 53	sylib	$⊢ (φ \land (S \in T \land Z \in T \land S \neq Z)) \to \exists g (g \in A \land g (S) \neq g (Z))$
55	25 54	mpdan	$⊢ φ \to \exists g (g \in A \land g (S) \neq g (Z))$
56		nfv	$⊢ Ⅎ t (g \in A \land g (S) \neq g (Z))$
57	2 56	nfan	$⊢ Ⅎ t (φ \land (g \in A \land g (S) \neq g (Z)))$
58		nfcv	$⊢ \underline{Ⅎ} t g$
59		eqid	$⊢ (t \in T ⟼ g (t) - g (Z)) = (t \in T ⟼ g (t) - g (Z))$
60		eqid	$⊢ J Cn K = J Cn K$
61	8	sselda	$⊢ (φ \land f \in A) \to f \in (J Cn K)$
62	4 6 60 61	fcnre	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
63	62	adantlr	$⊢ ((φ \land (g \in A \land g (S) \neq g (Z))) \land f \in A) \to f : T ⟶ ℝ$
64	9	3adant1r	$⊢ ((φ \land (g \in A \land g (S) \neq g (Z))) \land f \in A \land l \in A) \to (t \in T ⟼ f (t) + l (t)) \in A$
65	11	adantlr	$⊢ ((φ \land (g \in A \land g (S) \neq g (Z))) \land x \in ℝ) \to (t \in T ⟼ x) \in A$
66	17	adantr	$⊢ (φ \land (g \in A \land g (S) \neq g (Z))) \to S \in T$
67	20	adantr	$⊢ (φ \land (g \in A \land g (S) \neq g (Z))) \to Z \in T$
68		simprl	$⊢ (φ \land (g \in A \land g (S) \neq g (Z))) \to g \in A$
69		simprr	$⊢ (φ \land (g \in A \land g (S) \neq g (Z))) \to g (S) \neq g (Z)$
70	57 58 59 63 64 65 66 67 68 69	stoweidlem23	$⊢ (φ \land (g \in A \land g (S) \neq g (Z))) \to ((t \in T ⟼ g (t) - g (Z)) \in A \land (t \in T ⟼ g (t) - g (Z)) (S) \neq (t \in T ⟼ g (t) - g (Z)) (Z) \land (t \in T ⟼ g (t) - g (Z)) (Z) = 0)$
71		eleq1	$⊢ f = (t \in T ⟼ g (t) - g (Z)) \to (f \in A \leftrightarrow (t \in T ⟼ g (t) - g (Z)) \in A)$
72		fveq1	$⊢ f = (t \in T ⟼ g (t) - g (Z)) \to f (S) = (t \in T ⟼ g (t) - g (Z)) (S)$
73		fveq1	$⊢ f = (t \in T ⟼ g (t) - g (Z)) \to f (Z) = (t \in T ⟼ g (t) - g (Z)) (Z)$
74	72 73	neeq12d	$⊢ f = (t \in T ⟼ g (t) - g (Z)) \to (f (S) \neq f (Z) \leftrightarrow (t \in T ⟼ g (t) - g (Z)) (S) \neq (t \in T ⟼ g (t) - g (Z)) (Z))$
75	73	eqeq1d	$⊢ f = (t \in T ⟼ g (t) - g (Z)) \to (f (Z) = 0 \leftrightarrow (t \in T ⟼ g (t) - g (Z)) (Z) = 0)$
76	71 74 75	3anbi123d	$⊢ f = (t \in T ⟼ g (t) - g (Z)) \to ((f \in A \land f (S) \neq f (Z) \land f (Z) = 0) \leftrightarrow ((t \in T ⟼ g (t) - g (Z)) \in A \land (t \in T ⟼ g (t) - g (Z)) (S) \neq (t \in T ⟼ g (t) - g (Z)) (Z) \land (t \in T ⟼ g (t) - g (Z)) (Z) = 0))$
77	76	spcegv	$⊢ (t \in T ⟼ g (t) - g (Z)) \in A \to (((t \in T ⟼ g (t) - g (Z)) \in A \land (t \in T ⟼ g (t) - g (Z)) (S) \neq (t \in T ⟼ g (t) - g (Z)) (Z) \land (t \in T ⟼ g (t) - g (Z)) (Z) = 0) \to \exists f (f \in A \land f (S) \neq f (Z) \land f (Z) = 0))$
78	77	3ad2ant1	$⊢ ((t \in T ⟼ g (t) - g (Z)) \in A \land (t \in T ⟼ g (t) - g (Z)) (S) \neq (t \in T ⟼ g (t) - g (Z)) (Z) \land (t \in T ⟼ g (t) - g (Z)) (Z) = 0) \to (((t \in T ⟼ g (t) - g (Z)) \in A \land (t \in T ⟼ g (t) - g (Z)) (S) \neq (t \in T ⟼ g (t) - g (Z)) (Z) \land (t \in T ⟼ g (t) - g (Z)) (Z) = 0) \to \exists f (f \in A \land f (S) \neq f (Z) \land f (Z) = 0))$
79	78	pm2.43i	$⊢ ((t \in T ⟼ g (t) - g (Z)) \in A \land (t \in T ⟼ g (t) - g (Z)) (S) \neq (t \in T ⟼ g (t) - g (Z)) (Z) \land (t \in T ⟼ g (t) - g (Z)) (Z) = 0) \to \exists f (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)$
80	70 79	syl	$⊢ (φ \land (g \in A \land g (S) \neq g (Z))) \to \exists f (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)$
81	1 16 55 80	exlimdd	$⊢ φ \to \exists f (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)$
82		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ \frac{(s \in T ⟼ f (s) f (s)) (t)}{sup (ran (s \in T ⟼ f (s) f (s)) ℝ <)})$
83		nfcv	$⊢ \underline{Ⅎ} t f$
84		nfcv	$⊢ \underline{Ⅎ} t (s \in T ⟼ f (s) f (s))$
85		nfv	$⊢ Ⅎ t (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)$
86	2 85	nfan	$⊢ Ⅎ t (φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0))$
87		fveq2	$⊢ s = t \to f (s) = f (t)$
88	87 87	oveq12d	$⊢ s = t \to f (s) f (s) = f (t) f (t)$
89	88	cbvmptv	$⊢ (s \in T ⟼ f (s) f (s)) = (t \in T ⟼ f (t) f (t))$
90		eqid	$⊢ sup (ran (s \in T ⟼ f (s) f (s)) ℝ <) = sup (ran (s \in T ⟼ f (s) f (s)) ℝ <)$
91		eqid	$⊢ (t \in T ⟼ \frac{(s \in T ⟼ f (s) f (s)) (t)}{sup (ran (s \in T ⟼ f (s) f (s)) ℝ <)}) = (t \in T ⟼ \frac{(s \in T ⟼ f (s) f (s)) (t)}{sup (ran (s \in T ⟼ f (s) f (s)) ℝ <)})$
92	7	adantr	$⊢ (φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)) \to J \in Comp$
93	8	adantr	$⊢ (φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)) \to A \subseteq J Cn K$
94		eleq1	$⊢ f = k \to (f \in A \leftrightarrow k \in A)$
95	94	3anbi2d	$⊢ f = k \to ((φ \land f \in A \land l \in A) \leftrightarrow (φ \land k \in A \land l \in A))$
96		fveq1	$⊢ f = k \to f (t) = k (t)$
97	96	oveq1d	$⊢ f = k \to f (t) l (t) = k (t) l (t)$
98	97	mpteq2dv	$⊢ f = k \to (t \in T ⟼ f (t) l (t)) = (t \in T ⟼ k (t) l (t))$
99	98	eleq1d	$⊢ f = k \to ((t \in T ⟼ f (t) l (t)) \in A \leftrightarrow (t \in T ⟼ k (t) l (t)) \in A)$
100	95 99	imbi12d	$⊢ f = k \to (((φ \land f \in A \land l \in A) \to (t \in T ⟼ f (t) l (t)) \in A) \leftrightarrow ((φ \land k \in A \land l \in A) \to (t \in T ⟼ k (t) l (t)) \in A))$
101	100 10	chvarvv	$⊢ (φ \land k \in A \land l \in A) \to (t \in T ⟼ k (t) l (t)) \in A$
102	101	3adant1r	$⊢ ((φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)) \land k \in A \land l \in A) \to (t \in T ⟼ k (t) l (t)) \in A$
103	11	adantlr	$⊢ ((φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)) \land x \in ℝ) \to (t \in T ⟼ x) \in A$
104	17	adantr	$⊢ (φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)) \to S \in T$
105	20	adantr	$⊢ (φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)) \to Z \in T$
106		simpr1	$⊢ (φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)) \to f \in A$
107		simpr2	$⊢ (φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)) \to f (S) \neq f (Z)$
108		simpr3	$⊢ (φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)) \to f (Z) = 0$
109	3 82 83 84 86 4 5 6 89 90 91 92 93 102 103 104 105 106 107 108	stoweidlem36	$⊢ (φ \land (f \in A \land f (S) \neq f (Z) \land f (Z) = 0)) \to \exists h (h \in Q \land 0 < h (S))$
110	109	ex	$⊢ φ \to ((f \in A \land f (S) \neq f (Z) \land f (Z) = 0) \to \exists h (h \in Q \land 0 < h (S)))$
111	110	exlimdv	$⊢ φ \to (\exists f (f \in A \land f (S) \neq f (Z) \land f (Z) = 0) \to \exists h (h \in Q \land 0 < h (S)))$
112	81 111	mpd	$⊢ φ \to \exists h (h \in Q \land 0 < h (S))$

Metamath Proof Explorer

Theorem stoweidlem43

Proof