stoweidlem20

Description: If a set A of real functions from a common domain T is closed under the sum of two functions, then it is closed under the sum of a finite number of functions, indexed by G. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem20.1	$⊢ Ⅎ t φ$
	stoweidlem20.2	$⊢ F = (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t))$
	stoweidlem20.3	$⊢ φ \to M \in ℕ$
	stoweidlem20.4	$⊢ φ \to G : (1 \dots M) ⟶ A$
	stoweidlem20.5	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem20.6	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
Assertion	stoweidlem20	$⊢ φ \to F \in A$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem20.1	$⊢ Ⅎ t φ$
2		stoweidlem20.2	$⊢ F = (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t))$
3		stoweidlem20.3	$⊢ φ \to M \in ℕ$
4		stoweidlem20.4	$⊢ φ \to G : (1 \dots M) ⟶ A$
5		stoweidlem20.5	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
6		stoweidlem20.6	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
7	3	nnred	$⊢ φ \to M \in ℝ$
8	7	leidd	$⊢ φ \to M \leq M$
9	8	ancli	$⊢ φ \to (φ \land M \leq M)$
10		eleq1	$⊢ n = M \to (n \in ℕ \leftrightarrow M \in ℕ)$
11		breq1	$⊢ n = M \to (n \leq M \leftrightarrow M \leq M)$
12	11	anbi2d	$⊢ n = M \to ((φ \land n \leq M) \leftrightarrow (φ \land M \leq M))$
13		oveq2	$⊢ n = M \to (1 \dots n) = (1 \dots M)$
14	13	sumeq1d	$⊢ n = M \to \sum_{i = 1}^{n} G (i) (t) = \sum_{i = 1}^{M} G (i) (t)$
15	14	mpteq2dv	$⊢ n = M \to (t \in T ⟼ \sum_{i = 1}^{n} G (i) (t)) = (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t))$
16	15	eleq1d	$⊢ n = M \to ((t \in T ⟼ \sum_{i = 1}^{n} G (i) (t)) \in A \leftrightarrow (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t)) \in A)$
17	12 16	imbi12d	$⊢ n = M \to (((φ \land n \leq M) \to (t \in T ⟼ \sum_{i = 1}^{n} G (i) (t)) \in A) \leftrightarrow ((φ \land M \leq M) \to (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t)) \in A))$
18	10 17	imbi12d	$⊢ n = M \to ((n \in ℕ \to ((φ \land n \leq M) \to (t \in T ⟼ \sum_{i = 1}^{n} G (i) (t)) \in A)) \leftrightarrow (M \in ℕ \to ((φ \land M \leq M) \to (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t)) \in A)))$
19		breq1	$⊢ x = 1 \to (x \leq M \leftrightarrow 1 \leq M)$
20	19	anbi2d	$⊢ x = 1 \to ((φ \land x \leq M) \leftrightarrow (φ \land 1 \leq M))$
21		oveq2	$⊢ x = 1 \to (1 \dots x) = (1 \dots 1)$
22	21	sumeq1d	$⊢ x = 1 \to \sum_{i = 1}^{x} G (i) (t) = \sum_{i = 1}^{1} G (i) (t)$
23	22	mpteq2dv	$⊢ x = 1 \to (t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) = (t \in T ⟼ \sum_{i = 1}^{1} G (i) (t))$
24	23	eleq1d	$⊢ x = 1 \to ((t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) \in A \leftrightarrow (t \in T ⟼ \sum_{i = 1}^{1} G (i) (t)) \in A)$
25	20 24	imbi12d	$⊢ x = 1 \to (((φ \land x \leq M) \to (t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) \in A) \leftrightarrow ((φ \land 1 \leq M) \to (t \in T ⟼ \sum_{i = 1}^{1} G (i) (t)) \in A))$
26		breq1	$⊢ x = y \to (x \leq M \leftrightarrow y \leq M)$
27	26	anbi2d	$⊢ x = y \to ((φ \land x \leq M) \leftrightarrow (φ \land y \leq M))$
28		oveq2	$⊢ x = y \to (1 \dots x) = (1 \dots y)$
29	28	sumeq1d	$⊢ x = y \to \sum_{i = 1}^{x} G (i) (t) = \sum_{i = 1}^{y} G (i) (t)$
30	29	mpteq2dv	$⊢ x = y \to (t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) = (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t))$
31	30	eleq1d	$⊢ x = y \to ((t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) \in A \leftrightarrow (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A)$
32	27 31	imbi12d	$⊢ x = y \to (((φ \land x \leq M) \to (t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) \in A) \leftrightarrow ((φ \land y \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A))$
33		breq1	$⊢ x = y + 1 \to (x \leq M \leftrightarrow y + 1 \leq M)$
34	33	anbi2d	$⊢ x = y + 1 \to ((φ \land x \leq M) \leftrightarrow (φ \land y + 1 \leq M))$
35		oveq2	$⊢ x = y + 1 \to (1 \dots x) = (1 \dots y + 1)$
36	35	sumeq1d	$⊢ x = y + 1 \to \sum_{i = 1}^{x} G (i) (t) = \sum_{i = 1}^{y + 1} G (i) (t)$
37	36	mpteq2dv	$⊢ x = y + 1 \to (t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) = (t \in T ⟼ \sum_{i = 1}^{y + 1} G (i) (t))$
38	37	eleq1d	$⊢ x = y + 1 \to ((t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) \in A \leftrightarrow (t \in T ⟼ \sum_{i = 1}^{y + 1} G (i) (t)) \in A)$
39	34 38	imbi12d	$⊢ x = y + 1 \to (((φ \land x \leq M) \to (t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) \in A) \leftrightarrow ((φ \land y + 1 \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y + 1} G (i) (t)) \in A))$
40		breq1	$⊢ x = n \to (x \leq M \leftrightarrow n \leq M)$
41	40	anbi2d	$⊢ x = n \to ((φ \land x \leq M) \leftrightarrow (φ \land n \leq M))$
42		oveq2	$⊢ x = n \to (1 \dots x) = (1 \dots n)$
43	42	sumeq1d	$⊢ x = n \to \sum_{i = 1}^{x} G (i) (t) = \sum_{i = 1}^{n} G (i) (t)$
44	43	mpteq2dv	$⊢ x = n \to (t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) = (t \in T ⟼ \sum_{i = 1}^{n} G (i) (t))$
45	44	eleq1d	$⊢ x = n \to ((t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) \in A \leftrightarrow (t \in T ⟼ \sum_{i = 1}^{n} G (i) (t)) \in A)$
46	41 45	imbi12d	$⊢ x = n \to (((φ \land x \leq M) \to (t \in T ⟼ \sum_{i = 1}^{x} G (i) (t)) \in A) \leftrightarrow ((φ \land n \leq M) \to (t \in T ⟼ \sum_{i = 1}^{n} G (i) (t)) \in A))$
47		1z	$⊢ 1 \in ℤ$
48		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
49	3 48	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
50		eluzfz1	$⊢ M \in ℤ_{\geq 1} \to 1 \in (1 \dots M)$
51	49 50	syl	$⊢ φ \to 1 \in (1 \dots M)$
52	4 51	ffvelcdmd	$⊢ φ \to G (1) \in A$
53	52	ancli	$⊢ φ \to (φ \land G (1) \in A)$
54		eleq1	$⊢ f = G (1) \to (f \in A \leftrightarrow G (1) \in A)$
55	54	anbi2d	$⊢ f = G (1) \to ((φ \land f \in A) \leftrightarrow (φ \land G (1) \in A))$
56		feq1	$⊢ f = G (1) \to (f : T ⟶ ℝ \leftrightarrow G (1) : T ⟶ ℝ)$
57	55 56	imbi12d	$⊢ f = G (1) \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land G (1) \in A) \to G (1) : T ⟶ ℝ))$
58	57 6	vtoclg	$⊢ G (1) \in A \to ((φ \land G (1) \in A) \to G (1) : T ⟶ ℝ)$
59	52 53 58	sylc	$⊢ φ \to G (1) : T ⟶ ℝ$
60	59	ffvelcdmda	$⊢ (φ \land t \in T) \to G (1) (t) \in ℝ$
61	60	recnd	$⊢ (φ \land t \in T) \to G (1) (t) \in ℂ$
62		fveq2	$⊢ i = 1 \to G (i) = G (1)$
63	62	fveq1d	$⊢ i = 1 \to G (i) (t) = G (1) (t)$
64	63	fsum1	$⊢ (1 \in ℤ \land G (1) (t) \in ℂ) \to \sum_{i = 1}^{1} G (i) (t) = G (1) (t)$
65	47 61 64	sylancr	$⊢ (φ \land t \in T) \to \sum_{i = 1}^{1} G (i) (t) = G (1) (t)$
66	1 65	mpteq2da	$⊢ φ \to (t \in T ⟼ \sum_{i = 1}^{1} G (i) (t)) = (t \in T ⟼ G (1) (t))$
67	59	feqmptd	$⊢ φ \to G (1) = (t \in T ⟼ G (1) (t))$
68	66 67	eqtr4d	$⊢ φ \to (t \in T ⟼ \sum_{i = 1}^{1} G (i) (t)) = G (1)$
69	68 52	eqeltrd	$⊢ φ \to (t \in T ⟼ \sum_{i = 1}^{1} G (i) (t)) \in A$
70	69	adantr	$⊢ (φ \land 1 \leq M) \to (t \in T ⟼ \sum_{i = 1}^{1} G (i) (t)) \in A$
71		simprl	$⊢ ((y \in ℕ \land ((φ \land y \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A)) \land (φ \land y + 1 \leq M)) \to φ$
72		simpll	$⊢ ((y \in ℕ \land ((φ \land y \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A)) \land (φ \land y + 1 \leq M)) \to y \in ℕ$
73		simprr	$⊢ ((y \in ℕ \land ((φ \land y \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A)) \land (φ \land y + 1 \leq M)) \to y + 1 \leq M$
74		simp1	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to φ$
75		nnre	$⊢ y \in ℕ \to y \in ℝ$
76	75	3ad2ant2	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to y \in ℝ$
77		1red	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to 1 \in ℝ$
78	76 77	readdcld	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to y + 1 \in ℝ$
79	3	3ad2ant1	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to M \in ℕ$
80	79	nnred	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to M \in ℝ$
81	76	lep1d	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to y \leq y + 1$
82		simp3	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to y + 1 \leq M$
83	76 78 80 81 82	letrd	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to y \leq M$
84	74 83	jca	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to (φ \land y \leq M)$
85	71 72 73 84	syl3anc	$⊢ ((y \in ℕ \land ((φ \land y \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A)) \land (φ \land y + 1 \leq M)) \to (φ \land y \leq M)$
86		simplr	$⊢ ((y \in ℕ \land ((φ \land y \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A)) \land (φ \land y + 1 \leq M)) \to ((φ \land y \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A)$
87	85 86	mpd	$⊢ ((y \in ℕ \land ((φ \land y \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A)) \land (φ \land y + 1 \leq M)) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A$
88		nfv	$⊢ Ⅎ t y \in ℕ$
89		nfv	$⊢ Ⅎ t y + 1 \leq M$
90	1 88 89	nf3an	$⊢ Ⅎ t (φ \land y \in ℕ \land y + 1 \leq M)$
91		simpl2	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to y \in ℕ$
92	91 48	eleqtrdi	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to y \in ℤ_{\geq 1}$
93		simpll1	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to φ$
94		1zzd	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to 1 \in ℤ$
95	3	nnzd	$⊢ φ \to M \in ℤ$
96	95	3ad2ant1	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to M \in ℤ$
97	96	ad2antrr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to M \in ℤ$
98		elfzelz	$⊢ i \in (1 \dots y + 1) \to i \in ℤ$
99	98	adantl	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to i \in ℤ$
100		elfzle1	$⊢ i \in (1 \dots y + 1) \to 1 \leq i$
101	100	adantl	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to 1 \leq i$
102	98	zred	$⊢ i \in (1 \dots y + 1) \to i \in ℝ$
103	102	adantl	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to i \in ℝ$
104	78	ad2antrr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to y + 1 \in ℝ$
105	80	ad2antrr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to M \in ℝ$
106		elfzle2	$⊢ i \in (1 \dots y + 1) \to i \leq y + 1$
107	106	adantl	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to i \leq y + 1$
108		simpll3	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to y + 1 \leq M$
109	103 104 105 107 108	letrd	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to i \leq M$
110	94 97 99 101 109	elfzd	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to i \in (1 \dots M)$
111		simplr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to t \in T$
112	4	ffvelcdmda	$⊢ (φ \land i \in (1 \dots M)) \to G (i) \in A$
113	112	3adant3	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to G (i) \in A$
114		simp1	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to φ$
115	114 113	jca	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to (φ \land G (i) \in A)$
116		eleq1	$⊢ f = G (i) \to (f \in A \leftrightarrow G (i) \in A)$
117	116	anbi2d	$⊢ f = G (i) \to ((φ \land f \in A) \leftrightarrow (φ \land G (i) \in A))$
118		feq1	$⊢ f = G (i) \to (f : T ⟶ ℝ \leftrightarrow G (i) : T ⟶ ℝ)$
119	117 118	imbi12d	$⊢ f = G (i) \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land G (i) \in A) \to G (i) : T ⟶ ℝ))$
120	119 6	vtoclg	$⊢ G (i) \in A \to ((φ \land G (i) \in A) \to G (i) : T ⟶ ℝ)$
121	113 115 120	sylc	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to G (i) : T ⟶ ℝ$
122		simp3	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to t \in T$
123	121 122	ffvelcdmd	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to G (i) (t) \in ℝ$
124	123	recnd	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to G (i) (t) \in ℂ$
125	93 110 111 124	syl3anc	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to G (i) (t) \in ℂ$
126		fveq2	$⊢ i = y + 1 \to G (i) = G (y + 1)$
127	126	fveq1d	$⊢ i = y + 1 \to G (i) (t) = G (y + 1) (t)$
128	92 125 127	fsump1	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to \sum_{i = 1}^{y + 1} G (i) (t) = \sum_{i = 1}^{y} G (i) (t) + G (y + 1) (t)$
129		simpr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to t \in T$
130		fzfid	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to (1 \dots y) \in Fin$
131		simpll1	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to φ$
132		1zzd	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to 1 \in ℤ$
133	96	ad2antrr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to M \in ℤ$
134		elfzelz	$⊢ i \in (1 \dots y) \to i \in ℤ$
135	134	adantl	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to i \in ℤ$
136		elfzle1	$⊢ i \in (1 \dots y) \to 1 \leq i$
137	136	adantl	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to 1 \leq i$
138	134	zred	$⊢ i \in (1 \dots y) \to i \in ℝ$
139	138	adantl	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to i \in ℝ$
140	78	adantr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to y + 1 \in ℝ$
141	80	adantr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to M \in ℝ$
142	76	adantr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to y \in ℝ$
143		elfzle2	$⊢ i \in (1 \dots y) \to i \leq y$
144	143	adantl	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to i \leq y$
145		letrp1	$⊢ (i \in ℝ \land y \in ℝ \land i \leq y) \to i \leq y + 1$
146	139 142 144 145	syl3anc	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to i \leq y + 1$
147		simpl3	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to y + 1 \leq M$
148	139 140 141 146 147	letrd	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to i \leq M$
149	148	adantlr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to i \leq M$
150	132 133 135 137 149	elfzd	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to i \in (1 \dots M)$
151		simplr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to t \in T$
152	131 150 151 123	syl3anc	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to G (i) (t) \in ℝ$
153	130 152	fsumrecl	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to \sum_{i = 1}^{y} G (i) (t) \in ℝ$
154		eqid	$⊢ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) = (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t))$
155	154	fvmpt2	$⊢ (t \in T \land \sum_{i = 1}^{y} G (i) (t) \in ℝ) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) = \sum_{i = 1}^{y} G (i) (t)$
156	129 153 155	syl2anc	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) = \sum_{i = 1}^{y} G (i) (t)$
157	156	oveq1d	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + G (y + 1) (t) = \sum_{i = 1}^{y} G (i) (t) + G (y + 1) (t)$
158	128 157	eqtr4d	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to \sum_{i = 1}^{y + 1} G (i) (t) = (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + G (y + 1) (t)$
159	90 158	mpteq2da	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y + 1} G (i) (t)) = (t \in T ⟼ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + G (y + 1) (t))$
160	159	adantr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to (t \in T ⟼ \sum_{i = 1}^{y + 1} G (i) (t)) = (t \in T ⟼ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + G (y + 1) (t))$
161		1zzd	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to 1 \in ℤ$
162		peano2nn	$⊢ y \in ℕ \to y + 1 \in ℕ$
163	162	nnzd	$⊢ y \in ℕ \to y + 1 \in ℤ$
164	163	3ad2ant2	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to y + 1 \in ℤ$
165	162	nnge1d	$⊢ y \in ℕ \to 1 \leq y + 1$
166	165	3ad2ant2	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to 1 \leq y + 1$
167	161 96 164 166 82	elfzd	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to y + 1 \in (1 \dots M)$
168	4	ffvelcdmda	$⊢ (φ \land y + 1 \in (1 \dots M)) \to G (y + 1) \in A$
169	74 167 168	syl2anc	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to G (y + 1) \in A$
170		eleq1	$⊢ f = G (y + 1) \to (f \in A \leftrightarrow G (y + 1) \in A)$
171	170	anbi2d	$⊢ f = G (y + 1) \to ((φ \land f \in A) \leftrightarrow (φ \land G (y + 1) \in A))$
172		feq1	$⊢ f = G (y + 1) \to (f : T ⟶ ℝ \leftrightarrow G (y + 1) : T ⟶ ℝ)$
173	171 172	imbi12d	$⊢ f = G (y + 1) \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land G (y + 1) \in A) \to G (y + 1) : T ⟶ ℝ))$
174	173 6	vtoclg	$⊢ G (y + 1) \in A \to ((φ \land G (y + 1) \in A) \to G (y + 1) : T ⟶ ℝ)$
175	174	anabsi7	$⊢ (φ \land G (y + 1) \in A) \to G (y + 1) : T ⟶ ℝ$
176	74 169 175	syl2anc	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to G (y + 1) : T ⟶ ℝ$
177	176	ffvelcdmda	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to G (y + 1) (t) \in ℝ$
178		eqid	$⊢ (t \in T ⟼ G (y + 1) (t)) = (t \in T ⟼ G (y + 1) (t))$
179	178	fvmpt2	$⊢ (t \in T \land G (y + 1) (t) \in ℝ) \to (t \in T ⟼ G (y + 1) (t)) (t) = G (y + 1) (t)$
180	129 177 179	syl2anc	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to (t \in T ⟼ G (y + 1) (t)) (t) = G (y + 1) (t)$
181	180	oveq2d	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + (t \in T ⟼ G (y + 1) (t)) (t) = (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + G (y + 1) (t)$
182	90 181	mpteq2da	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to (t \in T ⟼ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + (t \in T ⟼ G (y + 1) (t)) (t)) = (t \in T ⟼ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + G (y + 1) (t))$
183	182	adantr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to (t \in T ⟼ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + (t \in T ⟼ G (y + 1) (t)) (t)) = (t \in T ⟼ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + G (y + 1) (t))$
184		simpl1	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to φ$
185		simpr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A$
186	167	adantr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to y + 1 \in (1 \dots M)$
187	175	feqmptd	$⊢ (φ \land G (y + 1) \in A) \to G (y + 1) = (t \in T ⟼ G (y + 1) (t))$
188	168 187	syldan	$⊢ (φ \land y + 1 \in (1 \dots M)) \to G (y + 1) = (t \in T ⟼ G (y + 1) (t))$
189	188 168	eqeltrrd	$⊢ (φ \land y + 1 \in (1 \dots M)) \to (t \in T ⟼ G (y + 1) (t)) \in A$
190	184 186 189	syl2anc	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to (t \in T ⟼ G (y + 1) (t)) \in A$
191		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t))$
192		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ G (y + 1) (t))$
193	5 191 192	stoweidlem8	$⊢ (φ \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A \land (t \in T ⟼ G (y + 1) (t)) \in A) \to (t \in T ⟼ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + (t \in T ⟼ G (y + 1) (t)) (t)) \in A$
194	184 185 190 193	syl3anc	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to (t \in T ⟼ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + (t \in T ⟼ G (y + 1) (t)) (t)) \in A$
195	183 194	eqeltrrd	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to (t \in T ⟼ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) (t) + G (y + 1) (t)) \in A$
196	160 195	eqeltrd	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to (t \in T ⟼ \sum_{i = 1}^{y + 1} G (i) (t)) \in A$
197	71 72 73 87 196	syl31anc	$⊢ ((y \in ℕ \land ((φ \land y \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A)) \land (φ \land y + 1 \leq M)) \to (t \in T ⟼ \sum_{i = 1}^{y + 1} G (i) (t)) \in A$
198	197	exp31	$⊢ y \in ℕ \to (((φ \land y \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to ((φ \land y + 1 \leq M) \to (t \in T ⟼ \sum_{i = 1}^{y + 1} G (i) (t)) \in A))$
199	25 32 39 46 70 198	nnind	$⊢ n \in ℕ \to ((φ \land n \leq M) \to (t \in T ⟼ \sum_{i = 1}^{n} G (i) (t)) \in A)$
200	18 199	vtoclg	$⊢ M \in ℕ \to (M \in ℕ \to ((φ \land M \leq M) \to (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t)) \in A))$
201	3 3 9 200	syl3c	$⊢ φ \to (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t)) \in A$
202	2 201	eqeltrid	$⊢ φ \to F \in A$

Metamath Proof Explorer

Theorem stoweidlem20

Proof