Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem20 Structured version   Unicode version

Theorem stoweidlem20 27745
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.)
Hypotheses
Ref Expression
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
Ref Expression
stoweidlem20  |-  ( ph  ->  F  e.  A )
Distinct variable groups:    f, g,
i, t, G    A, f, g    T, f, g, i, t    ph, f,
g, i    i, M, t
Allowed substitution hints:    ph( t)    A( t, i)    F( t, f, g, i)    M( f, g)

Proof of Theorem stoweidlem20
Dummy variables  y  n  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem20.2 . 2  |-  F  =  ( t  e.  T  |-> 
sum_ i  e.  ( 1 ... M ) ( ( G `  i ) `  t
) )
2 stoweidlem20.3 . . 3  |-  ( ph  ->  M  e.  NN )
32nnred 10015 . . . . 5  |-  ( ph  ->  M  e.  RR )
43leidd 9593 . . . 4  |-  ( ph  ->  M  <_  M )
54ancli 535 . . 3  |-  ( ph  ->  ( ph  /\  M  <_  M ) )
6 eleq1 2496 . . . . 5  |-  ( n  =  M  ->  (
n  e.  NN  <->  M  e.  NN ) )
7 breq1 4215 . . . . . . 7  |-  ( n  =  M  ->  (
n  <_  M  <->  M  <_  M ) )
87anbi2d 685 . . . . . 6  |-  ( n  =  M  ->  (
( ph  /\  n  <_  M )  <->  ( ph  /\  M  <_  M )
) )
9 oveq2 6089 . . . . . . . . 9  |-  ( n  =  M  ->  (
1 ... n )  =  ( 1 ... M
) )
109sumeq1d 12495 . . . . . . . 8  |-  ( n  =  M  ->  sum_ i  e.  ( 1 ... n
) ( ( G `
 i ) `  t )  =  sum_ i  e.  ( 1 ... M ) ( ( G `  i
) `  t )
)
1110mpteq2dv 4296 . . . . . . 7  |-  ( n  =  M  ->  (
t  e.  T  |->  sum_ i  e.  ( 1 ... n ) ( ( G `  i
) `  t )
)  =  ( t  e.  T  |->  sum_ i  e.  ( 1 ... M
) ( ( G `
 i ) `  t ) ) )
1211eleq1d 2502 . . . . . 6  |-  ( 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 ) )
138, 12imbi12d 312 . . . . 5  |-  ( 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
) ) )
146, 13imbi12d 312 . . . 4  |-  ( 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 ) ) ) )
15 breq1 4215 . . . . . . 7  |-  ( x  =  1  ->  (
x  <_  M  <->  1  <_  M ) )
1615anbi2d 685 . . . . . 6  |-  ( x  =  1  ->  (
( ph  /\  x  <_  M )  <->  ( ph  /\  1  <_  M )
) )
17 oveq2 6089 . . . . . . . . 9  |-  ( x  =  1  ->  (
1 ... x )  =  ( 1 ... 1
) )
1817sumeq1d 12495 . . . . . . . 8  |-  ( x  =  1  ->  sum_ i  e.  ( 1 ... x
) ( ( G `
 i ) `  t )  =  sum_ i  e.  ( 1 ... 1 ) ( ( G `  i
) `  t )
)
1918mpteq2dv 4296 . . . . . . 7  |-  ( x  =  1  ->  (
t  e.  T  |->  sum_ i  e.  ( 1 ... x ) ( ( G `  i
) `  t )
)  =  ( t  e.  T  |->  sum_ i  e.  ( 1 ... 1
) ( ( G `
 i ) `  t ) ) )
2019eleq1d 2502 . . . . . 6  |-  ( 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 ) )
2116, 20imbi12d 312 . . . . 5  |-  ( 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
) ) )
22 breq1 4215 . . . . . . 7  |-  ( x  =  y  ->  (
x  <_  M  <->  y  <_  M ) )
2322anbi2d 685 . . . . . 6  |-  ( x  =  y  ->  (
( ph  /\  x  <_  M )  <->  ( ph  /\  y  <_  M )
) )
24 oveq2 6089 . . . . . . . . 9  |-  ( x  =  y  ->  (
1 ... x )  =  ( 1 ... y
) )
2524sumeq1d 12495 . . . . . . . 8  |-  ( x  =  y  ->  sum_ i  e.  ( 1 ... x
) ( ( G `
 i ) `  t )  =  sum_ i  e.  ( 1 ... y ) ( ( G `  i
) `  t )
)
2625mpteq2dv 4296 . . . . . . 7  |-  ( x  =  y  ->  (
t  e.  T  |->  sum_ i  e.  ( 1 ... x ) ( ( G `  i
) `  t )
)  =  ( t  e.  T  |->  sum_ i  e.  ( 1 ... y
) ( ( G `
 i ) `  t ) ) )
2726eleq1d 2502 . . . . . 6  |-  ( 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 ) )
2823, 27imbi12d 312 . . . . 5  |-  ( 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
) ) )
29 breq1 4215 . . . . . . 7  |-  ( x  =  ( y  +  1 )  ->  (
x  <_  M  <->  ( y  +  1 )  <_  M ) )
3029anbi2d 685 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
( ph  /\  x  <_  M )  <->  ( ph  /\  ( y  +  1 )  <_  M )
) )
31 oveq2 6089 . . . . . . . . 9  |-  ( x  =  ( y  +  1 )  ->  (
1 ... x )  =  ( 1 ... (
y  +  1 ) ) )
3231sumeq1d 12495 . . . . . . . 8  |-  ( x  =  ( y  +  1 )  ->  sum_ i  e.  ( 1 ... x
) ( ( G `
 i ) `  t )  =  sum_ i  e.  ( 1 ... ( y  +  1 ) ) ( ( G `  i
) `  t )
)
3332mpteq2dv 4296 . . . . . . 7  |-  ( 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 ) ) )
3433eleq1d 2502 . . . . . 6  |-  ( 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 ) )
3530, 34imbi12d 312 . . . . 5  |-  ( 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
) ) )
36 breq1 4215 . . . . . . 7  |-  ( x  =  n  ->  (
x  <_  M  <->  n  <_  M ) )
3736anbi2d 685 . . . . . 6  |-  ( x  =  n  ->  (
( ph  /\  x  <_  M )  <->  ( ph  /\  n  <_  M )
) )
38 oveq2 6089 . . . . . . . . 9  |-  ( x  =  n  ->  (
1 ... x )  =  ( 1 ... n
) )
3938sumeq1d 12495 . . . . . . . 8  |-  ( x  =  n  ->  sum_ i  e.  ( 1 ... x
) ( ( G `
 i ) `  t )  =  sum_ i  e.  ( 1 ... n ) ( ( G `  i
) `  t )
)
4039mpteq2dv 4296 . . . . . . 7  |-  ( x  =  n  ->  (
t  e.  T  |->  sum_ i  e.  ( 1 ... x ) ( ( G `  i
) `  t )
)  =  ( t  e.  T  |->  sum_ i  e.  ( 1 ... n
) ( ( G `
 i ) `  t ) ) )
4140eleq1d 2502 . . . . . 6  |-  ( 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 ) )
4237, 41imbi12d 312 . . . . 5  |-  ( 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
) ) )
43 stoweidlem20.1 . . . . . . . . 9  |-  F/ t
ph
44 1z 10311 . . . . . . . . . 10  |-  1  e.  ZZ
45 stoweidlem20.4 . . . . . . . . . . . . . 14  |-  ( ph  ->  G : ( 1 ... M ) --> A )
46 nnuz 10521 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
472, 46syl6eleq 2526 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
48 eluzfz1 11064 . . . . . . . . . . . . . . 15  |-  ( M  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... M
) )
4947, 48syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  ( 1 ... M ) )
5045, 49ffvelrnd 5871 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G `  1
)  e.  A )
5150ancli 535 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ph  /\  ( G `  1 )  e.  A ) )
52 eleq1 2496 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( G ` 
1 )  ->  (
f  e.  A  <->  ( G `  1 )  e.  A ) )
5352anbi2d 685 . . . . . . . . . . . . . . 15  |-  ( f  =  ( G ` 
1 )  ->  (
( ph  /\  f  e.  A )  <->  ( ph  /\  ( G `  1
)  e.  A ) ) )
54 feq1 5576 . . . . . . . . . . . . . . 15  |-  ( f  =  ( G ` 
1 )  ->  (
f : T --> RR  <->  ( G `  1 ) : T --> RR ) )
5553, 54imbi12d 312 . . . . . . . . . . . . . 14  |-  ( f  =  ( G ` 
1 )  ->  (
( ( ph  /\  f  e.  A )  ->  f : T --> RR )  <-> 
( ( ph  /\  ( G `  1 )  e.  A )  -> 
( G `  1
) : T --> RR ) ) )
56 stoweidlem20.6 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f  e.  A )  ->  f : T --> RR )
5755, 56vtoclg 3011 . . . . . . . . . . . . 13  |-  ( ( G `  1 )  e.  A  ->  (
( ph  /\  ( G `  1 )  e.  A )  ->  ( G `  1 ) : T --> RR ) )
5850, 51, 57sylc 58 . . . . . . . . . . . 12  |-  ( ph  ->  ( G `  1
) : T --> RR )
5958ffvelrnda 5870 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  T )  ->  (
( G `  1
) `  t )  e.  RR )
6059recnd 9114 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  T )  ->  (
( G `  1
) `  t )  e.  CC )
61 fveq2 5728 . . . . . . . . . . . 12  |-  ( i  =  1  ->  ( G `  i )  =  ( G ` 
1 ) )
6261fveq1d 5730 . . . . . . . . . . 11  |-  ( i  =  1  ->  (
( G `  i
) `  t )  =  ( ( G `
 1 ) `  t ) )
6362fsum1 12535 . . . . . . . . . 10  |-  ( ( 1  e.  ZZ  /\  ( ( G ` 
1 ) `  t
)  e.  CC )  ->  sum_ i  e.  ( 1 ... 1 ) ( ( G `  i ) `  t
)  =  ( ( G `  1 ) `
 t ) )
6444, 60, 63sylancr 645 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  T )  ->  sum_ i  e.  ( 1 ... 1
) ( ( G `
 i ) `  t )  =  ( ( G `  1
) `  t )
)
6543, 64mpteq2da 4294 . . . . . . . 8  |-  ( ph  ->  ( t  e.  T  |-> 
sum_ i  e.  ( 1 ... 1 ) ( ( G `  i ) `  t
) )  =  ( t  e.  T  |->  ( ( G `  1
) `  t )
) )
6658feqmptd 5779 . . . . . . . 8  |-  ( ph  ->  ( G `  1
)  =  ( t  e.  T  |->  ( ( G `  1 ) `
 t ) ) )
6765, 66eqtr4d 2471 . . . . . . 7  |-  ( ph  ->  ( t  e.  T  |-> 
sum_ i  e.  ( 1 ... 1 ) ( ( G `  i ) `  t
) )  =  ( G `  1 ) )
6867, 50eqeltrd 2510 . . . . . 6  |-  ( ph  ->  ( t  e.  T  |-> 
sum_ i  e.  ( 1 ... 1 ) ( ( G `  i ) `  t
) )  e.  A
)
6968adantr 452 . . . . 5  |-  ( (
ph  /\  1  <_  M )  ->  ( t  e.  T  |->  sum_ i  e.  ( 1 ... 1
) ( ( G `
 i ) `  t ) )  e.  A )
70 simprl 733 . . . . . . . 8  |-  ( ( ( y  e.  NN  /\  ( ( ph  /\  y  <_  M )  -> 
( t  e.  T  |-> 
sum_ i  e.  ( 1 ... y ) ( ( G `  i ) `  t
) )  e.  A
) )  /\  ( ph  /\  ( y  +  1 )  <_  M
) )  ->  ph )
71 simpll 731 . . . . . . . 8  |-  ( ( ( 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 )
72 simprr 734 . . . . . . . 8  |-  ( ( ( 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 )
7370, 71, 723jca 1134 . . . . . . 7  |-  ( ( ( 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  e.  NN  /\  ( y  +  1 )  <_  M )
)
74 simp1 957 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  ph )
75 nnre 10007 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  y  e.  RR )
76753ad2ant2 979 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  y  e.  RR )
77 1re 9090 . . . . . . . . . . . . 13  |-  1  e.  RR
7877a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  1  e.  RR )
7976, 78readdcld 9115 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  ( y  +  1 )  e.  RR )
8023ad2ant1 978 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  M  e.  NN )
8180nnred 10015 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  M  e.  RR )
8276lep1d 9942 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  y  <_  ( y  +  1 ) )
83 simp3 959 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  ( y  +  1 )  <_  M )
8476, 79, 81, 82, 83letrd 9227 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  y  <_  M )
8574, 84jca 519 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  ( ph  /\  y  <_  M )
)
8670, 71, 72, 85syl3anc 1184 . . . . . . . 8  |-  ( ( ( 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
) )
87 simplr 732 . . . . . . . 8  |-  ( ( ( 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 ) )
8886, 87mpd 15 . . . . . . 7  |-  ( ( ( 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 )
89 nfv 1629 . . . . . . . . . . 11  |-  F/ t  y  e.  NN
90 nfv 1629 . . . . . . . . . . 11  |-  F/ t ( y  +  1 )  <_  M
9143, 89, 90nf3an 1849 . . . . . . . . . 10  |-  F/ t ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )
92 simpl2 961 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  t  e.  T )  ->  y  e.  NN )
9392, 46syl6eleq 2526 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  t  e.  T )  ->  y  e.  ( ZZ>= `  1 )
)
94 simpll1 996 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  ph )
9544a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  1  e.  ZZ )
962nnzd 10374 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  ZZ )
97963ad2ant1 978 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  M  e.  ZZ )
9897ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  M  e.  ZZ )
99 elfzelz 11059 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... ( y  +  1 ) )  ->  i  e.  ZZ )
10099adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  i  e.  ZZ )
101 elfzle1 11060 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... ( y  +  1 ) )  ->  1  <_  i )
102101adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  1  <_  i
)
10399zred 10375 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... ( y  +  1 ) )  ->  i  e.  RR )
104103adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  i  e.  RR )
10579ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  ( y  +  1 )  e.  RR )
10681ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  M  e.  RR )
107 elfzle2 11061 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... ( y  +  1 ) )  ->  i  <_  ( y  +  1 ) )
108107adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  i  <_  (
y  +  1 ) )
109 simpll3 998 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  ( y  +  1 )  <_  M
)
110104, 105, 106, 108, 109letrd 9227 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  i  <_  M
)
111 elfz4 11052 . . . . . . . . . . . . . 14  |-  ( ( ( 1  e.  ZZ  /\  M  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  M ) )  ->  i  e.  ( 1 ... M
) )
11295, 98, 100, 102, 110, 111syl32anc 1192 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  i  e.  ( 1 ... M ) )
113 simplr 732 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  t  e.  T
)
11445ffvelrnda 5870 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( G `  i )  e.  A )
1151143adant3 977 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
)  /\  t  e.  T )  ->  ( G `  i )  e.  A )
116 simp1 957 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
)  /\  t  e.  T )  ->  ph )
117116, 115jca 519 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
)  /\  t  e.  T )  ->  ( ph  /\  ( G `  i )  e.  A
) )
118 eleq1 2496 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( G `  i )  ->  (
f  e.  A  <->  ( G `  i )  e.  A
) )
119118anbi2d 685 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( G `  i )  ->  (
( ph  /\  f  e.  A )  <->  ( ph  /\  ( G `  i
)  e.  A ) ) )
120 feq1 5576 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( G `  i )  ->  (
f : T --> RR  <->  ( G `  i ) : T --> RR ) )
121119, 120imbi12d 312 . . . . . . . . . . . . . . . . 17  |-  ( f  =  ( G `  i )  ->  (
( ( ph  /\  f  e.  A )  ->  f : T --> RR )  <-> 
( ( ph  /\  ( G `  i )  e.  A )  -> 
( G `  i
) : T --> RR ) ) )
122121, 56vtoclg 3011 . . . . . . . . . . . . . . . 16  |-  ( ( G `  i )  e.  A  ->  (
( ph  /\  ( G `  i )  e.  A )  ->  ( G `  i ) : T --> RR ) )
123115, 117, 122sylc 58 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
)  /\  t  e.  T )  ->  ( G `  i ) : T --> RR )
124 simp3 959 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
)  /\  t  e.  T )  ->  t  e.  T )
125123, 124ffvelrnd 5871 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
)  /\  t  e.  T )  ->  (
( G `  i
) `  t )  e.  RR )
126125recnd 9114 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
)  /\  t  e.  T )  ->  (
( G `  i
) `  t )  e.  CC )
12794, 112, 113, 126syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... ( y  +  1 ) ) )  ->  ( ( G `
 i ) `  t )  e.  CC )
128 fveq2 5728 . . . . . . . . . . . . 13  |-  ( i  =  ( y  +  1 )  ->  ( G `  i )  =  ( G `  ( y  +  1 ) ) )
129128fveq1d 5730 . . . . . . . . . . . 12  |-  ( i  =  ( y  +  1 )  ->  (
( G `  i
) `  t )  =  ( ( G `
 ( y  +  1 ) ) `  t ) )
13093, 127, 129fsump1 12540 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
131 simpr 448 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  t  e.  T )  ->  t  e.  T )
132 fzfid 11312 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  t  e.  T )  ->  (
1 ... y )  e. 
Fin )
133 simpll1 996 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... y ) )  ->  ph )
13444a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... y ) )  ->  1  e.  ZZ )
13597ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... y ) )  ->  M  e.  ZZ )
136 elfzelz 11059 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... y )  ->  i  e.  ZZ )
137136adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... y ) )  ->  i  e.  ZZ )
138 elfzle1 11060 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... y )  ->  1  <_  i )
139138adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... y ) )  ->  1  <_  i
)
140136zred 10375 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... y )  ->  i  e.  RR )
141140adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  i  e.  ( 1 ... y
) )  ->  i  e.  RR )
14279adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  i  e.  ( 1 ... y
) )  ->  (
y  +  1 )  e.  RR )
14381adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  i  e.  ( 1 ... y
) )  ->  M  e.  RR )
14476adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  i  e.  ( 1 ... y
) )  ->  y  e.  RR )
145 elfzle2 11061 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( 1 ... y )  ->  i  <_  y )
146145adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  i  e.  ( 1 ... y
) )  ->  i  <_  y )
147 letrp1 9852 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  RR  /\  y  e.  RR  /\  i  <_  y )  ->  i  <_  ( y  +  1 ) )
148141, 144, 146, 147syl3anc 1184 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  i  e.  ( 1 ... y
) )  ->  i  <_  ( y  +  1 ) )
149 simpl3 962 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  i  e.  ( 1 ... y
) )  ->  (
y  +  1 )  <_  M )
150141, 142, 143, 148, 149letrd 9227 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  i  e.  ( 1 ... y
) )  ->  i  <_  M )
151150adantlr 696 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... y ) )  ->  i  <_  M
)
152134, 135, 137, 139, 151, 111syl32anc 1192 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... y ) )  ->  i  e.  ( 1 ... M ) )
153 simplr 732 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... y ) )  ->  t  e.  T
)
154133, 152, 153, 125syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  NN  /\  (
y  +  1 )  <_  M )  /\  t  e.  T )  /\  i  e.  (
1 ... y ) )  ->  ( ( G `
 i ) `  t )  e.  RR )
155132, 154fsumrecl 12528 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  t  e.  T )  ->  sum_ i  e.  ( 1 ... y
) ( ( G `
 i ) `  t )  e.  RR )
156 eqid 2436 . . . . . . . . . . . . . 14  |-  ( t  e.  T  |->  sum_ i  e.  ( 1 ... y
) ( ( G `
 i ) `  t ) )  =  ( t  e.  T  |-> 
sum_ i  e.  ( 1 ... y ) ( ( G `  i ) `  t
) )
157156fvmpt2 5812 . . . . . . . . . . . . 13  |-  ( ( 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 ) )
158131, 155, 157syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
159158oveq1d 6096 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
160130, 159eqtr4d 2471 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
16191, 160mpteq2da 4294 . . . . . . . . 9  |-  ( (
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 ) ) ) )
162161adantr 452 . . . . . . . 8  |-  ( ( ( 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 ) ) ) )
16344a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  1  e.  ZZ )
164 peano2nn 10012 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
165164nnzd 10374 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  ZZ )
1661653ad2ant2 979 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  ( y  +  1 )  e.  ZZ )
167164nnge1d 10042 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  1  <_  ( y  +  1 ) )
1681673ad2ant2 979 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  1  <_  ( y  +  1 ) )
169 elfz4 11052 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1  e.  ZZ  /\  M  e.  ZZ  /\  ( y  +  1 )  e.  ZZ )  /\  ( 1  <_ 
( y  +  1 )  /\  ( y  +  1 )  <_  M ) )  -> 
( y  +  1 )  e.  ( 1 ... M ) )
170163, 97, 166, 168, 83, 169syl32anc 1192 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  ( y  +  1 )  e.  ( 1 ... M
) )
17145ffvelrnda 5870 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( y  +  1 )  e.  ( 1 ... M
) )  ->  ( G `  ( y  +  1 ) )  e.  A )
17274, 170, 171syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  ( G `  ( y  +  1 ) )  e.  A
)
173 eleq1 2496 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  ( G `  ( y  +  1 ) )  ->  (
f  e.  A  <->  ( G `  ( y  +  1 ) )  e.  A
) )
174173anbi2d 685 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( G `  ( y  +  1 ) )  ->  (
( ph  /\  f  e.  A )  <->  ( ph  /\  ( G `  (
y  +  1 ) )  e.  A ) ) )
175 feq1 5576 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( G `  ( y  +  1 ) )  ->  (
f : T --> RR  <->  ( G `  ( y  +  1 ) ) : T --> RR ) )
176174, 175imbi12d 312 . . . . . . . . . . . . . . . . 17  |-  ( f  =  ( G `  ( y  +  1 ) )  ->  (
( ( ph  /\  f  e.  A )  ->  f : T --> RR )  <-> 
( ( ph  /\  ( G `  ( y  +  1 ) )  e.  A )  -> 
( G `  (
y  +  1 ) ) : T --> RR ) ) )
177176, 56vtoclg 3011 . . . . . . . . . . . . . . . 16  |-  ( ( G `  ( y  +  1 ) )  e.  A  ->  (
( ph  /\  ( G `  ( y  +  1 ) )  e.  A )  -> 
( G `  (
y  +  1 ) ) : T --> RR ) )
178177anabsi7 793 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( G `  ( y  +  1 ) )  e.  A
)  ->  ( G `  ( y  +  1 ) ) : T --> RR )
17974, 172, 178syl2anc 643 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M
)  ->  ( G `  ( y  +  1 ) ) : T --> RR )
180179ffvelrnda 5870 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  t  e.  T )  ->  (
( G `  (
y  +  1 ) ) `  t )  e.  RR )
181 eqid 2436 . . . . . . . . . . . . . 14  |-  ( t  e.  T  |->  ( ( G `  ( y  +  1 ) ) `
 t ) )  =  ( t  e.  T  |->  ( ( G `
 ( y  +  1 ) ) `  t ) )
182181fvmpt2 5812 . . . . . . . . . . . . 13  |-  ( ( t  e.  T  /\  ( ( G `  ( y  +  1 ) ) `  t
)  e.  RR )  ->  ( ( t  e.  T  |->  ( ( G `  ( y  +  1 ) ) `
 t ) ) `
 t )  =  ( ( G `  ( y  +  1 ) ) `  t
) )
183131, 180, 182syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  t  e.  T )  ->  (
( t  e.  T  |->  ( ( G `  ( y  +  1 ) ) `  t
) ) `  t
)  =  ( ( G `  ( y  +  1 ) ) `
 t ) )
184183oveq2d 6097 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
18591, 184mpteq2da 4294 . . . . . . . . . 10  |-  ( (
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 ) ) ) )
186185adantr 452 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) )
187 simpl1 960 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  NN  /\  ( y  +  1 )  <_  M )  /\  (
t  e.  T  |->  sum_ i  e.  ( 1 ... y ) ( ( G `  i
) `  t )
)  e.  A )  ->  ph )
188 simpr 448 . . . . . . . . . 10  |-  ( ( ( 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
)
189170adantr 452 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
190178feqmptd 5779 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( G `  ( y  +  1 ) )  e.  A
)  ->  ( G `  ( y  +  1 ) )  =  ( t  e.  T  |->  ( ( G `  (
y  +  1 ) ) `  t ) ) )
191171, 190syldan 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  +  1 )  e.  ( 1 ... M
) )  ->  ( G `  ( y  +  1 ) )  =  ( t  e.  T  |->  ( ( G `
 ( y  +  1 ) ) `  t ) ) )
192191, 171eqeltrrd 2511 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  +  1 )  e.  ( 1 ... M
) )  ->  (
t  e.  T  |->  ( ( G `  (
y  +  1 ) ) `  t ) )  e.  A )
193187, 189, 192syl2anc 643 . . . . . . . . . 10  |-  ( ( ( 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 )
194 stoweidlem20.5 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A )
195 nfmpt1 4298 . . . . . . . . . . 11  |-  F/_ t
( t  e.  T  |-> 
sum_ i  e.  ( 1 ... y ) ( ( G `  i ) `  t
) )
196 nfmpt1 4298 . . . . . . . . . . 11  |-  F/_ t
( t  e.  T  |->  ( ( G `  ( y  +  1 ) ) `  t
) )
197194, 195, 196stoweidlem8 27733 . . . . . . . . . 10  |-  ( (
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 )
198187, 188, 193, 197syl3anc 1184 . . . . . . . . 9  |-  ( ( ( 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 )
199186, 198eqeltrrd 2511 . . . . . . . 8  |-  ( ( ( 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 )
200162, 199eqeltrd 2510 . . . . . . 7  |-  ( ( ( 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
)
20173, 88, 200syl2anc 643 . . . . . 6  |-  ( ( ( 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 )
202201exp31 588 . . . . 5  |-  ( 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 ) ) )
20321, 28, 35, 42, 69, 202nnind 10018 . . . 4  |-  ( n  e.  NN  ->  (
( ph  /\  n  <_  M )  ->  (
t  e.  T  |->  sum_ i  e.  ( 1 ... n ) ( ( G `  i
) `  t )
)  e.  A ) )
20414, 203vtoclg 3011 . . 3  |-  ( M  e.  NN  ->  ( M  e.  NN  ->  ( ( ph  /\  M  <_  M )  ->  (
t  e.  T  |->  sum_ i  e.  ( 1 ... M ) ( ( G `  i
) `  t )
)  e.  A ) ) )
2052, 2, 5, 204syl3c 59 . 2  |-  ( ph  ->  ( t  e.  T  |-> 
sum_ i  e.  ( 1 ... M ) ( ( G `  i ) `  t
) )  e.  A
)
2061, 205syl5eqel 2520 1  |-  ( ph  ->  F  e.  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936   F/wnf 1553    = wceq 1652    e. wcel 1725   class class class wbr 4212    e. cmpt 4266   -->wf 5450   ` cfv 5454  (class class class)co 6081   CCcc 8988   RRcr 8989   1c1 8991    + caddc 8993    <_ cle 9121   NNcn 10000   ZZcz 10282   ZZ>=cuz 10488   ...cfz 11043   sum_csu 12479
This theorem is referenced by:  stoweidlem32  27757
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-inf2 7596  ax-cnex 9046  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-mulcom 9054  ax-addass 9055  ax-mulass 9056  ax-distr 9057  ax-i2m1 9058  ax-1ne0 9059  ax-1rid 9060  ax-rnegex 9061  ax-rrecex 9062  ax-cnre 9063  ax-pre-lttri 9064  ax-pre-lttrn 9065  ax-pre-ltadd 9066  ax-pre-mulgt0 9067  ax-pre-sup 9068
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-int 4051  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-se 4542  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-isom 5463  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-1st 6349  df-2nd 6350  df-riota 6549  df-recs 6633  df-rdg 6668  df-1o 6724  df-oadd 6728  df-er 6905  df-en 7110  df-dom 7111  df-sdom 7112  df-fin 7113  df-sup 7446  df-oi 7479  df-card 7826  df-pnf 9122  df-mnf 9123  df-xr 9124  df-ltxr 9125  df-le 9126  df-sub 9293  df-neg 9294  df-div 9678  df-nn 10001  df-2 10058  df-3 10059  df-n0 10222  df-z 10283  df-uz 10489  df-rp 10613  df-fz 11044  df-fzo 11136  df-seq 11324  df-exp 11383  df-hash 11619  df-cj 11904  df-re 11905  df-im 11906  df-sqr 12040  df-abs 12041  df-clim 12282  df-sum 12480
  Copyright terms: Public domain W3C validator