stoweidlem27

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

	Ref	Expression
Hypotheses	stoweidlem27.1	$⊢ G = (w \in X ⟼ \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
	stoweidlem27.2	$⊢ φ \to Q \in V$
	stoweidlem27.3	$⊢ φ \to M \in ℕ$
	stoweidlem27.4	$⊢ φ \to Y Fn ran G$
	stoweidlem27.5	$⊢ φ \to ran G \in V$
	stoweidlem27.6	$⊢ (φ \land l \in ran G) \to Y (l) \in l$
	stoweidlem27.7	$⊢ φ \to F : (1 \dots M) \underset{1-1 onto}{⟶} ran G$
	stoweidlem27.8	$⊢ φ \to T ∖ U \subseteq ⋃ X$
	stoweidlem27.9	$⊢ Ⅎ t φ$
	stoweidlem27.10	$⊢ Ⅎ w φ$
	stoweidlem27.11	$⊢ \underline{Ⅎ} h Q$
Assertion	stoweidlem27	$⊢ φ \to \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)))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem27.1	$⊢ G = (w \in X ⟼ \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
2		stoweidlem27.2	$⊢ φ \to Q \in V$
3		stoweidlem27.3	$⊢ φ \to M \in ℕ$
4		stoweidlem27.4	$⊢ φ \to Y Fn ran G$
5		stoweidlem27.5	$⊢ φ \to ran G \in V$
6		stoweidlem27.6	$⊢ (φ \land l \in ran G) \to Y (l) \in l$
7		stoweidlem27.7	$⊢ φ \to F : (1 \dots M) \underset{1-1 onto}{⟶} ran G$
8		stoweidlem27.8	$⊢ φ \to T ∖ U \subseteq ⋃ X$
9		stoweidlem27.9	$⊢ Ⅎ t φ$
10		stoweidlem27.10	$⊢ Ⅎ w φ$
11		stoweidlem27.11	$⊢ \underline{Ⅎ} h Q$
12		fnex	$⊢ (Y Fn ran G \land ran G \in V) \to Y \in V$
13	4 5 12	syl2anc	$⊢ φ \to Y \in V$
14		f1ofn	$⊢ F : (1 \dots M) \underset{1-1 onto}{⟶} ran G \to F Fn (1 \dots M)$
15	7 14	syl	$⊢ φ \to F Fn (1 \dots M)$
16		ovex	$⊢ (1 \dots M) \in V$
17		fnex	$⊢ (F Fn (1 \dots M) \land (1 \dots M) \in V) \to F \in V$
18	15 16 17	sylancl	$⊢ φ \to F \in V$
19		coexg	$⊢ (Y \in V \land F \in V) \to Y \circ F \in V$
20	13 18 19	syl2anc	$⊢ φ \to Y \circ F \in V$
21		f1of	$⊢ F : (1 \dots M) \underset{1-1 onto}{⟶} ran G \to F : (1 \dots M) ⟶ ran G$
22	7 21	syl	$⊢ φ \to F : (1 \dots M) ⟶ ran G$
23		fnfco	$⊢ (Y Fn ran G \land F : (1 \dots M) ⟶ ran G) \to (Y \circ F) Fn (1 \dots M)$
24	4 22 23	syl2anc	$⊢ φ \to (Y \circ F) Fn (1 \dots M)$
25		rncoss	$⊢ ran (Y \circ F) \subseteq ran Y$
26		fvelrnb	$⊢ Y Fn ran G \to (k \in ran Y \leftrightarrow \exists l \in ran G Y (l) = k)$
27	4 26	syl	$⊢ φ \to (k \in ran Y \leftrightarrow \exists l \in ran G Y (l) = k)$
28	27	biimpa	$⊢ (φ \land k \in ran Y) \to \exists l \in ran G Y (l) = k$
29		nfmpt1	$⊢ \underline{Ⅎ} w (w \in X ⟼ \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
30	1 29	nfcxfr	$⊢ \underline{Ⅎ} w G$
31	30	nfrn	$⊢ \underline{Ⅎ} w ran G$
32	31	nfcri	$⊢ Ⅎ w l \in ran G$
33	10 32	nfan	$⊢ Ⅎ w (φ \land l \in ran G)$
34	6	ad2antrr	$⊢ (((φ \land l \in ran G) \land w \in X) \land l = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) \to Y (l) \in l$
35		simpr	$⊢ (((φ \land l \in ran G) \land w \in X) \land l = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) \to l = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
36	34 35	eleqtrd	$⊢ (((φ \land l \in ran G) \land w \in X) \land l = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) \to Y (l) \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
37		nfcv	$⊢ \underline{Ⅎ} h Y (l)$
38		nfv	$⊢ Ⅎ h w = \{t \in T \| 0 < Y (l) (t)\}$
39		fveq1	$⊢ h = Y (l) \to h (t) = Y (l) (t)$
40	39	breq2d	$⊢ h = Y (l) \to (0 < h (t) \leftrightarrow 0 < Y (l) (t))$
41	40	rabbidv	$⊢ h = Y (l) \to \{t \in T \| 0 < h (t)\} = \{t \in T \| 0 < Y (l) (t)\}$
42	41	eqeq2d	$⊢ h = Y (l) \to (w = \{t \in T \| 0 < h (t)\} \leftrightarrow w = \{t \in T \| 0 < Y (l) (t)\})$
43	37 11 38 42	elrabf	$⊢ Y (l) \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \leftrightarrow (Y (l) \in Q \land w = \{t \in T \| 0 < Y (l) (t)\})$
44	36 43	sylib	$⊢ (((φ \land l \in ran G) \land w \in X) \land l = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) \to (Y (l) \in Q \land w = \{t \in T \| 0 < Y (l) (t)\})$
45	44	simpld	$⊢ (((φ \land l \in ran G) \land w \in X) \land l = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) \to Y (l) \in Q$
46		simpr	$⊢ (φ \land l \in ran G) \to l \in ran G$
47	1	elrnmpt	$⊢ l \in ran G \to (l \in ran G \leftrightarrow \exists w \in X l = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
48	46 47	syl	$⊢ (φ \land l \in ran G) \to (l \in ran G \leftrightarrow \exists w \in X l = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
49	46 48	mpbid	$⊢ (φ \land l \in ran G) \to \exists w \in X l = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
50	33 45 49	r19.29af	$⊢ (φ \land l \in ran G) \to Y (l) \in Q$
51	50	adantlr	$⊢ ((φ \land k \in ran Y) \land l \in ran G) \to Y (l) \in Q$
52		eleq1	$⊢ Y (l) = k \to (Y (l) \in Q \leftrightarrow k \in Q)$
53	51 52	syl5ibcom	$⊢ ((φ \land k \in ran Y) \land l \in ran G) \to (Y (l) = k \to k \in Q)$
54	53	reximdva	$⊢ (φ \land k \in ran Y) \to (\exists l \in ran G Y (l) = k \to \exists l \in ran G k \in Q)$
55	28 54	mpd	$⊢ (φ \land k \in ran Y) \to \exists l \in ran G k \in Q$
56		idd	$⊢ l \in ran G \to (k \in Q \to k \in Q)$
57	56	a1i	$⊢ (φ \land k \in ran Y) \to (l \in ran G \to (k \in Q \to k \in Q))$
58	57	rexlimdv	$⊢ (φ \land k \in ran Y) \to (\exists l \in ran G k \in Q \to k \in Q)$
59	55 58	mpd	$⊢ (φ \land k \in ran Y) \to k \in Q$
60	59	ex	$⊢ φ \to (k \in ran Y \to k \in Q)$
61	60	ssrdv	$⊢ φ \to ran Y \subseteq Q$
62	25 61	sstrid	$⊢ φ \to ran (Y \circ F) \subseteq Q$
63		df-f	$⊢ (Y \circ F) : (1 \dots M) ⟶ Q \leftrightarrow ((Y \circ F) Fn (1 \dots M) \land ran (Y \circ F) \subseteq Q)$
64	24 62 63	sylanbrc	$⊢ φ \to (Y \circ F) : (1 \dots M) ⟶ Q$
65		nfv	$⊢ Ⅎ w t \in (T ∖ U)$
66	10 65	nfan	$⊢ Ⅎ w (φ \land t \in (T ∖ U))$
67		nfv	$⊢ Ⅎ w \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t)$
68	8	sselda	$⊢ (φ \land t \in (T ∖ U)) \to t \in ⋃ X$
69		eluni	$⊢ t \in ⋃ X \leftrightarrow \exists w (t \in w \land w \in X)$
70	68 69	sylib	$⊢ (φ \land t \in (T ∖ U)) \to \exists w (t \in w \land w \in X)$
71	1	funmpt2	$⊢ Fun G$
72	1	dmeqi	$⊢ dom G = dom (w \in X ⟼ \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
73	11	rabexgf	$⊢ Q \in V \to \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \in V$
74	2 73	syl	$⊢ φ \to \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \in V$
75	74	adantr	$⊢ (φ \land w \in X) \to \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \in V$
76	75	ex	$⊢ φ \to (w \in X \to \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \in V)$
77	10 76	ralrimi	$⊢ φ \to \forall w \in X \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \in V$
78		dmmptg	$⊢ \forall w \in X \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \in V \to dom (w \in X ⟼ \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) = X$
79	77 78	syl	$⊢ φ \to dom (w \in X ⟼ \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}) = X$
80	72 79	syl5eq	$⊢ φ \to dom G = X$
81	80	eleq2d	$⊢ φ \to (w \in dom G \leftrightarrow w \in X)$
82	81	biimpar	$⊢ (φ \land w \in X) \to w \in dom G$
83		fvelrn	$⊢ (Fun G \land w \in dom G) \to G (w) \in ran G$
84	71 82 83	sylancr	$⊢ (φ \land w \in X) \to G (w) \in ran G$
85	84	adantrl	$⊢ (φ \land (t \in w \land w \in X)) \to G (w) \in ran G$
86	22	ad2antrr	$⊢ ((φ \land G (w) \in ran G) \land (i \in (1 \dots M) \land F (i) = G (w))) \to F : (1 \dots M) ⟶ ran G$
87		simprl	$⊢ ((φ \land G (w) \in ran G) \land (i \in (1 \dots M) \land F (i) = G (w))) \to i \in (1 \dots M)$
88		fvco3	$⊢ (F : (1 \dots M) ⟶ ran G \land i \in (1 \dots M)) \to (Y \circ F) (i) = Y (F (i))$
89	86 87 88	syl2anc	$⊢ ((φ \land G (w) \in ran G) \land (i \in (1 \dots M) \land F (i) = G (w))) \to (Y \circ F) (i) = Y (F (i))$
90		fveq2	$⊢ F (i) = G (w) \to Y (F (i)) = Y (G (w))$
91	90	ad2antll	$⊢ ((φ \land G (w) \in ran G) \land (i \in (1 \dots M) \land F (i) = G (w))) \to Y (F (i)) = Y (G (w))$
92	89 91	eqtrd	$⊢ ((φ \land G (w) \in ran G) \land (i \in (1 \dots M) \land F (i) = G (w))) \to (Y \circ F) (i) = Y (G (w))$
93		eleq1	$⊢ l = G (w) \to (l \in ran G \leftrightarrow G (w) \in ran G)$
94	93	anbi2d	$⊢ l = G (w) \to ((φ \land l \in ran G) \leftrightarrow (φ \land G (w) \in ran G))$
95		eleq2	$⊢ l = G (w) \to (Y (l) \in l \leftrightarrow Y (l) \in G (w))$
96		fveq2	$⊢ l = G (w) \to Y (l) = Y (G (w))$
97	96	eleq1d	$⊢ l = G (w) \to (Y (l) \in G (w) \leftrightarrow Y (G (w)) \in G (w))$
98	95 97	bitrd	$⊢ l = G (w) \to (Y (l) \in l \leftrightarrow Y (G (w)) \in G (w))$
99	94 98	imbi12d	$⊢ l = G (w) \to (((φ \land l \in ran G) \to Y (l) \in l) \leftrightarrow ((φ \land G (w) \in ran G) \to Y (G (w)) \in G (w)))$
100	99 6	vtoclg	$⊢ G (w) \in ran G \to ((φ \land G (w) \in ran G) \to Y (G (w)) \in G (w))$
101	100	anabsi7	$⊢ (φ \land G (w) \in ran G) \to Y (G (w)) \in G (w)$
102	101	adantr	$⊢ ((φ \land G (w) \in ran G) \land (i \in (1 \dots M) \land F (i) = G (w))) \to Y (G (w)) \in G (w)$
103	92 102	eqeltrd	$⊢ ((φ \land G (w) \in ran G) \land (i \in (1 \dots M) \land F (i) = G (w))) \to (Y \circ F) (i) \in G (w)$
104		f1ofo	$⊢ F : (1 \dots M) \underset{1-1 onto}{⟶} ran G \to F : (1 \dots M) \underset{onto}{⟶} ran G$
105		forn	$⊢ F : (1 \dots M) \underset{onto}{⟶} ran G \to ran F = ran G$
106	7 104 105	3syl	$⊢ φ \to ran F = ran G$
107	106	eleq2d	$⊢ φ \to (G (w) \in ran F \leftrightarrow G (w) \in ran G)$
108	107	biimpar	$⊢ (φ \land G (w) \in ran G) \to G (w) \in ran F$
109	15	adantr	$⊢ (φ \land G (w) \in ran G) \to F Fn (1 \dots M)$
110		fvelrnb	$⊢ F Fn (1 \dots M) \to (G (w) \in ran F \leftrightarrow \exists i \in (1 \dots M) F (i) = G (w))$
111	109 110	syl	$⊢ (φ \land G (w) \in ran G) \to (G (w) \in ran F \leftrightarrow \exists i \in (1 \dots M) F (i) = G (w))$
112	108 111	mpbid	$⊢ (φ \land G (w) \in ran G) \to \exists i \in (1 \dots M) F (i) = G (w)$
113	103 112	reximddv	$⊢ (φ \land G (w) \in ran G) \to \exists i \in (1 \dots M) (Y \circ F) (i) \in G (w)$
114	85 113	syldan	$⊢ (φ \land (t \in w \land w \in X)) \to \exists i \in (1 \dots M) (Y \circ F) (i) \in G (w)$
115		simplrl	$⊢ ((φ \land (t \in w \land w \in X)) \land (Y \circ F) (i) \in G (w)) \to t \in w$
116		simpr	$⊢ (φ \land w \in X) \to w \in X$
117	1	fvmpt2	$⊢ (w \in X \land \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \in V) \to G (w) = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
118	116 75 117	syl2anc	$⊢ (φ \land w \in X) \to G (w) = \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
119	118	eleq2d	$⊢ (φ \land w \in X) \to ((Y \circ F) (i) \in G (w) \leftrightarrow (Y \circ F) (i) \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\})$
120	119	biimpa	$⊢ ((φ \land w \in X) \land (Y \circ F) (i) \in G (w)) \to (Y \circ F) (i) \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
121	120	adantlrl	$⊢ ((φ \land (t \in w \land w \in X)) \land (Y \circ F) (i) \in G (w)) \to (Y \circ F) (i) \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\}$
122		nfcv	$⊢ \underline{Ⅎ} h (Y \circ F) (i)$
123		nfv	$⊢ Ⅎ h w = \{t \in T \| 0 < (Y \circ F) (i) (t)\}$
124		fveq1	$⊢ h = (Y \circ F) (i) \to h (t) = (Y \circ F) (i) (t)$
125	124	breq2d	$⊢ h = (Y \circ F) (i) \to (0 < h (t) \leftrightarrow 0 < (Y \circ F) (i) (t))$
126	125	rabbidv	$⊢ h = (Y \circ F) (i) \to \{t \in T \| 0 < h (t)\} = \{t \in T \| 0 < (Y \circ F) (i) (t)\}$
127	126	eqeq2d	$⊢ h = (Y \circ F) (i) \to (w = \{t \in T \| 0 < h (t)\} \leftrightarrow w = \{t \in T \| 0 < (Y \circ F) (i) (t)\})$
128	122 11 123 127	elrabf	$⊢ (Y \circ F) (i) \in \{h \in Q \| w = \{t \in T \| 0 < h (t)\}\} \leftrightarrow ((Y \circ F) (i) \in Q \land w = \{t \in T \| 0 < (Y \circ F) (i) (t)\})$
129	121 128	sylib	$⊢ ((φ \land (t \in w \land w \in X)) \land (Y \circ F) (i) \in G (w)) \to ((Y \circ F) (i) \in Q \land w = \{t \in T \| 0 < (Y \circ F) (i) (t)\})$
130	129	simprd	$⊢ ((φ \land (t \in w \land w \in X)) \land (Y \circ F) (i) \in G (w)) \to w = \{t \in T \| 0 < (Y \circ F) (i) (t)\}$
131	115 130	eleqtrd	$⊢ ((φ \land (t \in w \land w \in X)) \land (Y \circ F) (i) \in G (w)) \to t \in \{t \in T \| 0 < (Y \circ F) (i) (t)\}$
132		rabid	$⊢ t \in \{t \in T \| 0 < (Y \circ F) (i) (t)\} \leftrightarrow (t \in T \land 0 < (Y \circ F) (i) (t))$
133	131 132	sylib	$⊢ ((φ \land (t \in w \land w \in X)) \land (Y \circ F) (i) \in G (w)) \to (t \in T \land 0 < (Y \circ F) (i) (t))$
134	133	simprd	$⊢ ((φ \land (t \in w \land w \in X)) \land (Y \circ F) (i) \in G (w)) \to 0 < (Y \circ F) (i) (t)$
135	134	ex	$⊢ (φ \land (t \in w \land w \in X)) \to ((Y \circ F) (i) \in G (w) \to 0 < (Y \circ F) (i) (t))$
136	135	reximdv	$⊢ (φ \land (t \in w \land w \in X)) \to (\exists i \in (1 \dots M) (Y \circ F) (i) \in G (w) \to \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t))$
137	114 136	mpd	$⊢ (φ \land (t \in w \land w \in X)) \to \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t)$
138	137	ex	$⊢ φ \to ((t \in w \land w \in X) \to \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t))$
139	138	adantr	$⊢ (φ \land t \in (T ∖ U)) \to ((t \in w \land w \in X) \to \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t))$
140	66 67 70 139	exlimimdd	$⊢ (φ \land t \in (T ∖ U)) \to \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t)$
141	140	ex	$⊢ φ \to (t \in (T ∖ U) \to \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t))$
142	9 141	ralrimi	$⊢ φ \to \forall t \in (T ∖ U) \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t)$
143	3 64 142	jca32	$⊢ φ \to (M \in ℕ \land ((Y \circ F) : (1 \dots M) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t)))$
144		feq1	$⊢ q = Y \circ F \to (q : (1 \dots M) ⟶ Q \leftrightarrow (Y \circ F) : (1 \dots M) ⟶ Q)$
145		fveq1	$⊢ q = Y \circ F \to q (i) = (Y \circ F) (i)$
146	145	fveq1d	$⊢ q = Y \circ F \to q (i) (t) = (Y \circ F) (i) (t)$
147	146	breq2d	$⊢ q = Y \circ F \to (0 < q (i) (t) \leftrightarrow 0 < (Y \circ F) (i) (t))$
148	147	rexbidv	$⊢ q = Y \circ F \to (\exists i \in (1 \dots M) 0 < q (i) (t) \leftrightarrow \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t))$
149	148	ralbidv	$⊢ q = Y \circ F \to (\forall t \in (T ∖ U) \exists i \in (1 \dots M) 0 < q (i) (t) \leftrightarrow \forall t \in (T ∖ U) \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t))$
150	144 149	anbi12d	$⊢ q = Y \circ F \to ((q : (1 \dots M) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots M) 0 < q (i) (t)) \leftrightarrow ((Y \circ F) : (1 \dots M) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t)))$
151	150	anbi2d	$⊢ q = Y \circ F \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))) \leftrightarrow (M \in ℕ \land ((Y \circ F) : (1 \dots M) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t))))$
152	151	spcegv	$⊢ Y \circ F \in V \to ((M \in ℕ \land ((Y \circ F) : (1 \dots M) ⟶ Q \land \forall t \in (T ∖ U) \exists i \in (1 \dots M) 0 < (Y \circ F) (i) (t))) \to \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))))$
153	20 143 152	sylc	$⊢ φ \to \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)))$

Metamath Proof Explorer

Theorem stoweidlem27

Proof