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	\|- F/ t ph
	stoweidlem20.2	\|- F = ( t e. T \|-> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) )
	stoweidlem20.3	\|- ( ph -> M e. NN )
	stoweidlem20.4	\|- ( ph -> G : ( 1 ... M ) --> A )
	stoweidlem20.5	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
	stoweidlem20.6	\|- ( ( ph /\ f e. A ) -> f : T --> RR )
Assertion	stoweidlem20	\|- ( ph -> F e. A )

Proof

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

Metamath Proof Explorer

Theorem stoweidlem20

Proof