stoweidlem48

Description: This lemma is used to prove that x built as in Lemma 2 of BrosowskiDeutsh p. 91, is such that x < ε on A . Here X is used to represent x in the paper, E is used to represent ε in the paper, and D is used to represent A in the paper (because A is always used to represent the subalgebra). (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem48.1	$⊢ Ⅎ i φ$
	stoweidlem48.2	$⊢ Ⅎ t φ$
	stoweidlem48.3	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
	stoweidlem48.4	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
	stoweidlem48.5	$⊢ X = seq 1 (P, U) (M)$
	stoweidlem48.6	$⊢ F = (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
	stoweidlem48.7	$⊢ Z = (t \in T ⟼ seq 1 (\times F (t)) (M))$
	stoweidlem48.8	$⊢ φ \to M \in ℕ$
	stoweidlem48.9	$⊢ φ \to W : (1 \dots M) ⟶ V$
	stoweidlem48.10	$⊢ φ \to U : (1 \dots M) ⟶ Y$
	stoweidlem48.11	$⊢ φ \to D \subseteq ⋃ ran W$
	stoweidlem48.12	$⊢ φ \to D \subseteq T$
	stoweidlem48.13	$⊢ (φ \land i \in (1 \dots M)) \to \forall t \in W (i) U (i) (t) < E$
	stoweidlem48.14	$⊢ φ \to T \in V$
	stoweidlem48.15	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
	stoweidlem48.16	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem48.17	$⊢ φ \to E \in ℝ^{+}$
Assertion	stoweidlem48	$⊢ φ \to \forall t \in D X (t) < E$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem48.1	$⊢ Ⅎ i φ$
2		stoweidlem48.2	$⊢ Ⅎ t φ$
3		stoweidlem48.3	$⊢ Y = \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
4		stoweidlem48.4	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
5		stoweidlem48.5	$⊢ X = seq 1 (P, U) (M)$
6		stoweidlem48.6	$⊢ F = (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
7		stoweidlem48.7	$⊢ Z = (t \in T ⟼ seq 1 (\times F (t)) (M))$
8		stoweidlem48.8	$⊢ φ \to M \in ℕ$
9		stoweidlem48.9	$⊢ φ \to W : (1 \dots M) ⟶ V$
10		stoweidlem48.10	$⊢ φ \to U : (1 \dots M) ⟶ Y$
11		stoweidlem48.11	$⊢ φ \to D \subseteq ⋃ ran W$
12		stoweidlem48.12	$⊢ φ \to D \subseteq T$
13		stoweidlem48.13	$⊢ (φ \land i \in (1 \dots M)) \to \forall t \in W (i) U (i) (t) < E$
14		stoweidlem48.14	$⊢ φ \to T \in V$
15		stoweidlem48.15	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
16		stoweidlem48.16	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
17		stoweidlem48.17	$⊢ φ \to E \in ℝ^{+}$
18	12	sselda	$⊢ (φ \land t \in D) \to t \in T$
19		nfra1	$⊢ Ⅎ t \forall t \in T (0 \leq h (t) \land h (t) \leq 1)$
20		nfcv	$⊢ \underline{Ⅎ} t A$
21	19 20	nfrabw	$⊢ \underline{Ⅎ} t \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
22	3 21	nfcxfr	$⊢ \underline{Ⅎ} t Y$
23	3	eleq2i	$⊢ f \in Y \leftrightarrow f \in \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\}$
24		fveq1	$⊢ h = f \to h (t) = f (t)$
25	24	breq2d	$⊢ h = f \to (0 \leq h (t) \leftrightarrow 0 \leq f (t))$
26	24	breq1d	$⊢ h = f \to (h (t) \leq 1 \leftrightarrow f (t) \leq 1)$
27	25 26	anbi12d	$⊢ h = f \to ((0 \leq h (t) \land h (t) \leq 1) \leftrightarrow (0 \leq f (t) \land f (t) \leq 1))$
28	27	ralbidv	$⊢ h = f \to (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq f (t) \land f (t) \leq 1))$
29	28	elrab	$⊢ f \in \{h \in A \| \forall t \in T (0 \leq h (t) \land h (t) \leq 1)\} \leftrightarrow (f \in A \land \forall t \in T (0 \leq f (t) \land f (t) \leq 1))$
30	23 29	sylbb	$⊢ f \in Y \to (f \in A \land \forall t \in T (0 \leq f (t) \land f (t) \leq 1))$
31	30	simpld	$⊢ f \in Y \to f \in A$
32	31 15	sylan2	$⊢ (φ \land f \in Y) \to f : T ⟶ ℝ$
33		eqid	$⊢ (t \in T ⟼ f (t) g (t)) = (t \in T ⟼ f (t) g (t))$
34	2 3 33 15 16	stoweidlem16	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y$
35	1 22 4 5 6 7 14 8 10 32 34	fmuldfeq	$⊢ (φ \land t \in T) \to X (t) = Z (t)$
36	18 35	syldan	$⊢ (φ \land t \in D) \to X (t) = Z (t)$
37		elnnuz	$⊢ M \in ℕ \leftrightarrow M \in ℤ_{\geq 1}$
38	8 37	sylib	$⊢ φ \to M \in ℤ_{\geq 1}$
39	38	adantr	$⊢ (φ \land t \in D) \to M \in ℤ_{\geq 1}$
40		nfv	$⊢ Ⅎ i t \in T$
41	1 40	nfan	$⊢ Ⅎ i (φ \land t \in T)$
42	10	ffvelrnda	$⊢ (φ \land i \in (1 \dots M)) \to U (i) \in Y$
43		fveq1	$⊢ h = U (i) \to h (t) = U (i) (t)$
44	43	breq2d	$⊢ h = U (i) \to (0 \leq h (t) \leftrightarrow 0 \leq U (i) (t))$
45	43	breq1d	$⊢ h = U (i) \to (h (t) \leq 1 \leftrightarrow U (i) (t) \leq 1)$
46	44 45	anbi12d	$⊢ h = U (i) \to ((0 \leq h (t) \land h (t) \leq 1) \leftrightarrow (0 \leq U (i) (t) \land U (i) (t) \leq 1))$
47	46	ralbidv	$⊢ h = U (i) \to (\forall t \in T (0 \leq h (t) \land h (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq U (i) (t) \land U (i) (t) \leq 1))$
48	47 3	elrab2	$⊢ U (i) \in Y \leftrightarrow (U (i) \in A \land \forall t \in T (0 \leq U (i) (t) \land U (i) (t) \leq 1))$
49	42 48	sylib	$⊢ (φ \land i \in (1 \dots M)) \to (U (i) \in A \land \forall t \in T (0 \leq U (i) (t) \land U (i) (t) \leq 1))$
50	49	simpld	$⊢ (φ \land i \in (1 \dots M)) \to U (i) \in A$
51		simpl	$⊢ (φ \land i \in (1 \dots M)) \to φ$
52	51 50	jca	$⊢ (φ \land i \in (1 \dots M)) \to (φ \land U (i) \in A)$
53		eleq1	$⊢ f = U (i) \to (f \in A \leftrightarrow U (i) \in A)$
54	53	anbi2d	$⊢ f = U (i) \to ((φ \land f \in A) \leftrightarrow (φ \land U (i) \in A))$
55		feq1	$⊢ f = U (i) \to (f : T ⟶ ℝ \leftrightarrow U (i) : T ⟶ ℝ)$
56	54 55	imbi12d	$⊢ f = U (i) \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land U (i) \in A) \to U (i) : T ⟶ ℝ))$
57	56 15	vtoclg	$⊢ U (i) \in A \to ((φ \land U (i) \in A) \to U (i) : T ⟶ ℝ)$
58	50 52 57	sylc	$⊢ (φ \land i \in (1 \dots M)) \to U (i) : T ⟶ ℝ$
59	58	adantlr	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to U (i) : T ⟶ ℝ$
60		simplr	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to t \in T$
61	59 60	ffvelrnd	$⊢ ((φ \land t \in T) \land i \in (1 \dots M)) \to U (i) (t) \in ℝ$
62		eqid	$⊢ (i \in (1 \dots M) ⟼ U (i) (t)) = (i \in (1 \dots M) ⟼ U (i) (t))$
63	41 61 62	fmptdf	$⊢ (φ \land t \in T) \to (i \in (1 \dots M) ⟼ U (i) (t)) : (1 \dots M) ⟶ ℝ$
64		simpr	$⊢ (φ \land t \in T) \to t \in T$
65		ovex	$⊢ (1 \dots M) \in V$
66		mptexg	$⊢ (1 \dots M) \in V \to (i \in (1 \dots M) ⟼ U (i) (t)) \in V$
67	65 66	mp1i	$⊢ (φ \land t \in T) \to (i \in (1 \dots M) ⟼ U (i) (t)) \in V$
68	6	fvmpt2	$⊢ (t \in T \land (i \in (1 \dots M) ⟼ U (i) (t)) \in V) \to F (t) = (i \in (1 \dots M) ⟼ U (i) (t))$
69	64 67 68	syl2anc	$⊢ (φ \land t \in T) \to F (t) = (i \in (1 \dots M) ⟼ U (i) (t))$
70	69	feq1d	$⊢ (φ \land t \in T) \to (F (t) : (1 \dots M) ⟶ ℝ \leftrightarrow (i \in (1 \dots M) ⟼ U (i) (t)) : (1 \dots M) ⟶ ℝ)$
71	63 70	mpbird	$⊢ (φ \land t \in T) \to F (t) : (1 \dots M) ⟶ ℝ$
72	18 71	syldan	$⊢ (φ \land t \in D) \to F (t) : (1 \dots M) ⟶ ℝ$
73	72	ffvelrnda	$⊢ ((φ \land t \in D) \land k \in (1 \dots M)) \to F (t) (k) \in ℝ$
74		remulcl	$⊢ (k \in ℝ \land j \in ℝ) \to k j \in ℝ$
75	74	adantl	$⊢ ((φ \land t \in D) \land (k \in ℝ \land j \in ℝ)) \to k j \in ℝ$
76	39 73 75	seqcl	$⊢ (φ \land t \in D) \to seq 1 (\times F (t)) (M) \in ℝ$
77	7	fvmpt2	$⊢ (t \in T \land seq 1 (\times F (t)) (M) \in ℝ) \to Z (t) = seq 1 (\times F (t)) (M)$
78	18 76 77	syl2anc	$⊢ (φ \land t \in D) \to Z (t) = seq 1 (\times F (t)) (M)$
79		nfcv	$⊢ \underline{Ⅎ} i T$
80		nfmpt1	$⊢ \underline{Ⅎ} i (i \in (1 \dots M) ⟼ U (i) (t))$
81	79 80	nfmpt	$⊢ \underline{Ⅎ} i (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
82	6 81	nfcxfr	$⊢ \underline{Ⅎ} i F$
83		nfcv	$⊢ \underline{Ⅎ} i t$
84	82 83	nffv	$⊢ \underline{Ⅎ} i F (t)$
85		nfv	$⊢ Ⅎ i t \in D$
86	1 85	nfan	$⊢ Ⅎ i (φ \land t \in D)$
87		nfcv	$⊢ \underline{Ⅎ} j seq 1 (\times F (t))$
88		eqid	$⊢ seq 1 (\times F (t)) = seq 1 (\times F (t))$
89	8	adantr	$⊢ (φ \land t \in D) \to M \in ℕ$
90		simpll	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to φ$
91		simpr	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to i \in (1 \dots M)$
92	18	adantr	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to t \in T$
93	49	simprd	$⊢ (φ \land i \in (1 \dots M)) \to \forall t \in T (0 \leq U (i) (t) \land U (i) (t) \leq 1)$
94	93	r19.21bi	$⊢ ((φ \land i \in (1 \dots M)) \land t \in T) \to (0 \leq U (i) (t) \land U (i) (t) \leq 1)$
95	94	simpld	$⊢ ((φ \land i \in (1 \dots M)) \land t \in T) \to 0 \leq U (i) (t)$
96	90 91 92 95	syl21anc	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to 0 \leq U (i) (t)$
97	69	fveq1d	$⊢ (φ \land t \in T) \to F (t) (i) = (i \in (1 \dots M) ⟼ U (i) (t)) (i)$
98	90 92 97	syl2anc	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to F (t) (i) = (i \in (1 \dots M) ⟼ U (i) (t)) (i)$
99	90 92 91 61	syl21anc	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to U (i) (t) \in ℝ$
100	62	fvmpt2	$⊢ (i \in (1 \dots M) \land U (i) (t) \in ℝ) \to (i \in (1 \dots M) ⟼ U (i) (t)) (i) = U (i) (t)$
101	91 99 100	syl2anc	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to (i \in (1 \dots M) ⟼ U (i) (t)) (i) = U (i) (t)$
102	98 101	eqtrd	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to F (t) (i) = U (i) (t)$
103	96 102	breqtrrd	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to 0 \leq F (t) (i)$
104	94	simprd	$⊢ ((φ \land i \in (1 \dots M)) \land t \in T) \to U (i) (t) \leq 1$
105	90 91 92 104	syl21anc	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to U (i) (t) \leq 1$
106	102 105	eqbrtrd	$⊢ ((φ \land t \in D) \land i \in (1 \dots M)) \to F (t) (i) \leq 1$
107	17	adantr	$⊢ (φ \land t \in D) \to E \in ℝ^{+}$
108	11	sselda	$⊢ (φ \land t \in D) \to t \in ⋃ ran W$
109		eluni	$⊢ t \in ⋃ ran W \leftrightarrow \exists w (t \in w \land w \in ran W)$
110	108 109	sylib	$⊢ (φ \land t \in D) \to \exists w (t \in w \land w \in ran W)$
111		ffn	$⊢ W : (1 \dots M) ⟶ V \to W Fn (1 \dots M)$
112		fvelrnb	$⊢ W Fn (1 \dots M) \to (w \in ran W \leftrightarrow \exists j \in (1 \dots M) W (j) = w)$
113	9 111 112	3syl	$⊢ φ \to (w \in ran W \leftrightarrow \exists j \in (1 \dots M) W (j) = w)$
114	113	biimpa	$⊢ (φ \land w \in ran W) \to \exists j \in (1 \dots M) W (j) = w$
115	114	adantrl	$⊢ (φ \land (t \in w \land w \in ran W)) \to \exists j \in (1 \dots M) W (j) = w$
116		simplr	$⊢ ((φ \land t \in w) \land W (j) = w) \to t \in w$
117		simpr	$⊢ ((φ \land t \in w) \land W (j) = w) \to W (j) = w$
118	116 117	eleqtrrd	$⊢ ((φ \land t \in w) \land W (j) = w) \to t \in W (j)$
119	118	ex	$⊢ (φ \land t \in w) \to (W (j) = w \to t \in W (j))$
120	119	reximdv	$⊢ (φ \land t \in w) \to (\exists j \in (1 \dots M) W (j) = w \to \exists j \in (1 \dots M) t \in W (j))$
121	120	adantrr	$⊢ (φ \land (t \in w \land w \in ran W)) \to (\exists j \in (1 \dots M) W (j) = w \to \exists j \in (1 \dots M) t \in W (j))$
122	115 121	mpd	$⊢ (φ \land (t \in w \land w \in ran W)) \to \exists j \in (1 \dots M) t \in W (j)$
123	122	ex	$⊢ φ \to ((t \in w \land w \in ran W) \to \exists j \in (1 \dots M) t \in W (j))$
124	123	exlimdv	$⊢ φ \to (\exists w (t \in w \land w \in ran W) \to \exists j \in (1 \dots M) t \in W (j))$
125	124	adantr	$⊢ (φ \land t \in D) \to (\exists w (t \in w \land w \in ran W) \to \exists j \in (1 \dots M) t \in W (j))$
126	110 125	mpd	$⊢ (φ \land t \in D) \to \exists j \in (1 \dots M) t \in W (j)$
127		simplll	$⊢ (((φ \land t \in D) \land j \in (1 \dots M)) \land t \in W (j)) \to φ$
128		simplr	$⊢ (((φ \land t \in D) \land j \in (1 \dots M)) \land t \in W (j)) \to j \in (1 \dots M)$
129		simpr	$⊢ (((φ \land t \in D) \land j \in (1 \dots M)) \land t \in W (j)) \to t \in W (j)$
130		nfv	$⊢ Ⅎ i j \in (1 \dots M)$
131		nfv	$⊢ Ⅎ i t \in W (j)$
132	1 130 131	nf3an	$⊢ Ⅎ i (φ \land j \in (1 \dots M) \land t \in W (j))$
133		nfv	$⊢ Ⅎ i U (j) (t) < E$
134	132 133	nfim	$⊢ Ⅎ i ((φ \land j \in (1 \dots M) \land t \in W (j)) \to U (j) (t) < E)$
135		eleq1	$⊢ i = j \to (i \in (1 \dots M) \leftrightarrow j \in (1 \dots M))$
136		fveq2	$⊢ i = j \to W (i) = W (j)$
137	136	eleq2d	$⊢ i = j \to (t \in W (i) \leftrightarrow t \in W (j))$
138	135 137	3anbi23d	$⊢ i = j \to ((φ \land i \in (1 \dots M) \land t \in W (i)) \leftrightarrow (φ \land j \in (1 \dots M) \land t \in W (j)))$
139		fveq2	$⊢ i = j \to U (i) = U (j)$
140	139	fveq1d	$⊢ i = j \to U (i) (t) = U (j) (t)$
141	140	breq1d	$⊢ i = j \to (U (i) (t) < E \leftrightarrow U (j) (t) < E)$
142	138 141	imbi12d	$⊢ i = j \to (((φ \land i \in (1 \dots M) \land t \in W (i)) \to U (i) (t) < E) \leftrightarrow ((φ \land j \in (1 \dots M) \land t \in W (j)) \to U (j) (t) < E))$
143	13	r19.21bi	$⊢ ((φ \land i \in (1 \dots M)) \land t \in W (i)) \to U (i) (t) < E$
144	143	3impa	$⊢ (φ \land i \in (1 \dots M) \land t \in W (i)) \to U (i) (t) < E$
145	134 142 144	chvarfv	$⊢ (φ \land j \in (1 \dots M) \land t \in W (j)) \to U (j) (t) < E$
146	127 128 129 145	syl3anc	$⊢ (((φ \land t \in D) \land j \in (1 \dots M)) \land t \in W (j)) \to U (j) (t) < E$
147	146	ex	$⊢ ((φ \land t \in D) \land j \in (1 \dots M)) \to (t \in W (j) \to U (j) (t) < E)$
148	147	reximdva	$⊢ (φ \land t \in D) \to (\exists j \in (1 \dots M) t \in W (j) \to \exists j \in (1 \dots M) U (j) (t) < E)$
149	126 148	mpd	$⊢ (φ \land t \in D) \to \exists j \in (1 \dots M) U (j) (t) < E$
150	86 130	nfan	$⊢ Ⅎ i ((φ \land t \in D) \land j \in (1 \dots M))$
151		nfcv	$⊢ \underline{Ⅎ} i j$
152	84 151	nffv	$⊢ \underline{Ⅎ} i F (t) (j)$
153	152	nfeq1	$⊢ Ⅎ i F (t) (j) = U (j) (t)$
154	150 153	nfim	$⊢ Ⅎ i (((φ \land t \in D) \land j \in (1 \dots M)) \to F (t) (j) = U (j) (t))$
155	135	anbi2d	$⊢ i = j \to (((φ \land t \in D) \land i \in (1 \dots M)) \leftrightarrow ((φ \land t \in D) \land j \in (1 \dots M)))$
156		fveq2	$⊢ i = j \to F (t) (i) = F (t) (j)$
157	156 140	eqeq12d	$⊢ i = j \to (F (t) (i) = U (i) (t) \leftrightarrow F (t) (j) = U (j) (t))$
158	155 157	imbi12d	$⊢ i = j \to ((((φ \land t \in D) \land i \in (1 \dots M)) \to F (t) (i) = U (i) (t)) \leftrightarrow (((φ \land t \in D) \land j \in (1 \dots M)) \to F (t) (j) = U (j) (t)))$
159	154 158 102	chvarfv	$⊢ ((φ \land t \in D) \land j \in (1 \dots M)) \to F (t) (j) = U (j) (t)$
160	159	breq1d	$⊢ ((φ \land t \in D) \land j \in (1 \dots M)) \to (F (t) (j) < E \leftrightarrow U (j) (t) < E)$
161	160	biimprd	$⊢ ((φ \land t \in D) \land j \in (1 \dots M)) \to (U (j) (t) < E \to F (t) (j) < E)$
162	161	reximdva	$⊢ (φ \land t \in D) \to (\exists j \in (1 \dots M) U (j) (t) < E \to \exists j \in (1 \dots M) F (t) (j) < E)$
163	149 162	mpd	$⊢ (φ \land t \in D) \to \exists j \in (1 \dots M) F (t) (j) < E$
164	84 86 87 88 89 72 103 106 107 163	fmul01lt1	$⊢ (φ \land t \in D) \to seq 1 (\times F (t)) (M) < E$
165	78 164	eqbrtrd	$⊢ (φ \land t \in D) \to Z (t) < E$
166	36 165	eqbrtrd	$⊢ (φ \land t \in D) \to X (t) < E$
167	166	ex	$⊢ φ \to (t \in D \to X (t) < E)$
168	2 167	ralrimi	$⊢ φ \to \forall t \in D X (t) < E$

Metamath Proof Explorer

Theorem stoweidlem48

Proof