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	ffvelrnd	$⊢ φ \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	ffvelrnda	$⊢ (φ \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		elfz4	$⊢ ((1 \in ℤ \land M \in ℤ \land i \in ℤ) \land (1 \leq i \land i \leq M)) \to i \in (1 \dots M)$
111	94 97 99 101 109 110	syl32anc	$⊢ (((φ \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)$
112		simplr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y + 1)) \to t \in T$
113	4	ffvelrnda	$⊢ (φ \land i \in (1 \dots M)) \to G (i) \in A$
114	113	3adant3	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to G (i) \in A$
115		simp1	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to φ$
116	115 114	jca	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to (φ \land G (i) \in A)$
117		eleq1	$⊢ f = G (i) \to (f \in A \leftrightarrow G (i) \in A)$
118	117	anbi2d	$⊢ f = G (i) \to ((φ \land f \in A) \leftrightarrow (φ \land G (i) \in A))$
119		feq1	$⊢ f = G (i) \to (f : T ⟶ ℝ \leftrightarrow G (i) : T ⟶ ℝ)$
120	118 119	imbi12d	$⊢ f = G (i) \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land G (i) \in A) \to G (i) : T ⟶ ℝ))$
121	120 6	vtoclg	$⊢ G (i) \in A \to ((φ \land G (i) \in A) \to G (i) : T ⟶ ℝ)$
122	114 116 121	sylc	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to G (i) : T ⟶ ℝ$
123		simp3	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to t \in T$
124	122 123	ffvelrnd	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to G (i) (t) \in ℝ$
125	124	recnd	$⊢ (φ \land i \in (1 \dots M) \land t \in T) \to G (i) (t) \in ℂ$
126	93 111 112 125	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 ℂ$
127		fveq2	$⊢ i = y + 1 \to G (i) = G (y + 1)$
128	127	fveq1d	$⊢ i = y + 1 \to G (i) (t) = G (y + 1) (t)$
129	92 126 128	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)$
130		simpr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to t \in T$
131		fzfid	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to (1 \dots y) \in Fin$
132		simpll1	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to φ$
133		1zzd	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to 1 \in ℤ$
134	96	ad2antrr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to M \in ℤ$
135		elfzelz	$⊢ i \in (1 \dots y) \to i \in ℤ$
136	135	adantl	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to i \in ℤ$
137		elfzle1	$⊢ i \in (1 \dots y) \to 1 \leq i$
138	137	adantl	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to 1 \leq i$
139	135	zred	$⊢ i \in (1 \dots y) \to i \in ℝ$
140	139	adantl	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to i \in ℝ$
141	78	adantr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to y + 1 \in ℝ$
142	80	adantr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to M \in ℝ$
143	76	adantr	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to y \in ℝ$
144		elfzle2	$⊢ i \in (1 \dots y) \to i \leq y$
145	144	adantl	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to i \leq y$
146		letrp1	$⊢ (i \in ℝ \land y \in ℝ \land i \leq y) \to i \leq y + 1$
147	140 143 145 146	syl3anc	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to i \leq y + 1$
148		simpl3	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to y + 1 \leq M$
149	140 141 142 147 148	letrd	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land i \in (1 \dots y)) \to i \leq M$
150	149	adantlr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to i \leq M$
151	133 134 136 138 150 110	syl32anc	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to i \in (1 \dots M)$
152		simplr	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to t \in T$
153	132 151 152 124	syl3anc	$⊢ (((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \land i \in (1 \dots y)) \to G (i) (t) \in ℝ$
154	131 153	fsumrecl	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to \sum_{i = 1}^{y} G (i) (t) \in ℝ$
155		eqid	$⊢ (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) = (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t))$
156	155	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)$
157	130 154 156	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)$
158	157	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)$
159	129 158	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)$
160	90 159	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))$
161	160	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))$
162		1zzd	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to 1 \in ℤ$
163		peano2nn	$⊢ y \in ℕ \to y + 1 \in ℕ$
164	163	nnzd	$⊢ y \in ℕ \to y + 1 \in ℤ$
165	164	3ad2ant2	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to y + 1 \in ℤ$
166	163	nnge1d	$⊢ y \in ℕ \to 1 \leq y + 1$
167	166	3ad2ant2	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to 1 \leq y + 1$
168		elfz4	$⊢ ((1 \in ℤ \land M \in ℤ \land y + 1 \in ℤ) \land (1 \leq y + 1 \land y + 1 \leq M)) \to y + 1 \in (1 \dots M)$
169	162 96 165 167 82 168	syl32anc	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to y + 1 \in (1 \dots M)$
170	4	ffvelrnda	$⊢ (φ \land y + 1 \in (1 \dots M)) \to G (y + 1) \in A$
171	74 169 170	syl2anc	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to G (y + 1) \in A$
172		eleq1	$⊢ f = G (y + 1) \to (f \in A \leftrightarrow G (y + 1) \in A)$
173	172	anbi2d	$⊢ f = G (y + 1) \to ((φ \land f \in A) \leftrightarrow (φ \land G (y + 1) \in A))$
174		feq1	$⊢ f = G (y + 1) \to (f : T ⟶ ℝ \leftrightarrow G (y + 1) : T ⟶ ℝ)$
175	173 174	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 ⟶ ℝ))$
176	175 6	vtoclg	$⊢ G (y + 1) \in A \to ((φ \land G (y + 1) \in A) \to G (y + 1) : T ⟶ ℝ)$
177	176	anabsi7	$⊢ (φ \land G (y + 1) \in A) \to G (y + 1) : T ⟶ ℝ$
178	74 171 177	syl2anc	$⊢ (φ \land y \in ℕ \land y + 1 \leq M) \to G (y + 1) : T ⟶ ℝ$
179	178	ffvelrnda	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land t \in T) \to G (y + 1) (t) \in ℝ$
180		eqid	$⊢ (t \in T ⟼ G (y + 1) (t)) = (t \in T ⟼ G (y + 1) (t))$
181	180	fvmpt2	$⊢ (t \in T \land G (y + 1) (t) \in ℝ) \to (t \in T ⟼ G (y + 1) (t)) (t) = G (y + 1) (t)$
182	130 179 181	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)$
183	182	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)$
184	90 183	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))$
185	184	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))$
186		simpl1	$⊢ ((φ \land y \in ℕ \land y + 1 \leq M) \land (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t)) \in A) \to φ$
187		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$
188	169	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)$
189	177	feqmptd	$⊢ (φ \land G (y + 1) \in A) \to G (y + 1) = (t \in T ⟼ G (y + 1) (t))$
190	170 189	syldan	$⊢ (φ \land y + 1 \in (1 \dots M)) \to G (y + 1) = (t \in T ⟼ G (y + 1) (t))$
191	190 170	eqeltrrd	$⊢ (φ \land y + 1 \in (1 \dots M)) \to (t \in T ⟼ G (y + 1) (t)) \in A$
192	186 188 191	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$
193		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ \sum_{i = 1}^{y} G (i) (t))$
194		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ G (y + 1) (t))$
195	5 193 194	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$
196	186 187 192 195	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$
197	185 196	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$
198	161 197	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$
199	71 72 73 87 198	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$
200	199	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))$
201	25 32 39 46 70 200	nnind	$⊢ n \in ℕ \to ((φ \land n \leq M) \to (t \in T ⟼ \sum_{i = 1}^{n} G (i) (t)) \in A)$
202	18 201	vtoclg	$⊢ M \in ℕ \to (M \in ℕ \to ((φ \land M \leq M) \to (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t)) \in A))$
203	3 3 9 202	syl3c	$⊢ φ \to (t \in T ⟼ \sum_{i = 1}^{M} G (i) (t)) \in A$
204	2 203	eqeltrid	$⊢ φ \to F \in A$

Metamath Proof Explorer

Theorem stoweidlem20

Proof