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

Metamath Proof Explorer

Theorem stoweidlem20

Proof