Metamath Proof Explorer

Theorem stoweidlem17

Description: This lemma proves that the function g (as defined in BrosowskiDeutsh p. 91, at the end of page 91) belongs to the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem17.1 
|- F/ t ph
stoweidlem17.2 
|- ( ph -> N e. NN )
stoweidlem17.3 
|- ( ph -> X : ( 0 ... N ) --> A )
stoweidlem17.4 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem17.5 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem17.6 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem17.7 
|- ( ph -> E e. RR )
stoweidlem17.8 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
Assertion stoweidlem17 
|- ( ph -> ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) e. A )

Proof

Step Hyp Ref Expression
1 stoweidlem17.1 
 |-  F/ t ph
2 stoweidlem17.2 
 |-  ( ph -> N e. NN )
3 stoweidlem17.3 
 |-  ( ph -> X : ( 0 ... N ) --> A )
4 stoweidlem17.4 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
5 stoweidlem17.5 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
6 stoweidlem17.6 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
7 stoweidlem17.7 
 |-  ( ph -> E e. RR )
8 stoweidlem17.8 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
9 2 nnnn0d 
 |-  ( ph -> N e. NN0 )
10 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
11 9 10 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
12 eluzfz2 
 |-  ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) )
13 11 12 syl 
 |-  ( ph -> N e. ( 0 ... N ) )
14 13 ancli 
 |-  ( ph -> ( ph /\ N e. ( 0 ... N ) ) )
15 eleq1 
 |-  ( n = 0 -> ( n e. ( 0 ... N ) <-> 0 e. ( 0 ... N ) ) )
16 15 anbi2d 
 |-  ( n = 0 -> ( ( ph /\ n e. ( 0 ... N ) ) <-> ( ph /\ 0 e. ( 0 ... N ) ) ) )
17 oveq2 
 |-  ( n = 0 -> ( 0 ... n ) = ( 0 ... 0 ) )
18 17 sumeq1d 
 |-  ( n = 0 -> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) = sum_ i e. ( 0 ... 0 ) ( E x. ( ( X ` i ) ` t ) ) )
19 18 mpteq2dv 
 |-  ( n = 0 -> ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> sum_ i e. ( 0 ... 0 ) ( E x. ( ( X ` i ) ` t ) ) ) )
20 19 eleq1d 
 |-  ( n = 0 -> ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) e. A <-> ( t e. T |-> sum_ i e. ( 0 ... 0 ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) )
21 16 20 imbi12d 
 |-  ( n = 0 -> ( ( ( ph /\ n e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) <-> ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... 0 ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) )
22 eleq1 
 |-  ( n = m -> ( n e. ( 0 ... N ) <-> m e. ( 0 ... N ) ) )
23 22 anbi2d 
 |-  ( n = m -> ( ( ph /\ n e. ( 0 ... N ) ) <-> ( ph /\ m e. ( 0 ... N ) ) ) )
24 oveq2 
 |-  ( n = m -> ( 0 ... n ) = ( 0 ... m ) )
25 24 sumeq1d 
 |-  ( n = m -> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) = sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) )
26 25 mpteq2dv 
 |-  ( n = m -> ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) )
27 26 eleq1d 
 |-  ( n = m -> ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) e. A <-> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) )
28 23 27 imbi12d 
 |-  ( n = m -> ( ( ( ph /\ n e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) <-> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) )
29 eleq1 
 |-  ( n = ( m + 1 ) -> ( n e. ( 0 ... N ) <-> ( m + 1 ) e. ( 0 ... N ) ) )
30 29 anbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ph /\ n e. ( 0 ... N ) ) <-> ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) )
31 oveq2 
 |-  ( n = ( m + 1 ) -> ( 0 ... n ) = ( 0 ... ( m + 1 ) ) )
32 31 sumeq1d 
 |-  ( n = ( m + 1 ) -> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) = sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) )
33 32 mpteq2dv 
 |-  ( n = ( m + 1 ) -> ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) ) )
34 33 eleq1d 
 |-  ( n = ( m + 1 ) -> ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) e. A <-> ( t e. T |-> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) )
35 30 34 imbi12d 
 |-  ( n = ( m + 1 ) -> ( ( ( ph /\ n e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) <-> ( ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) )
36 eleq1 
 |-  ( n = N -> ( n e. ( 0 ... N ) <-> N e. ( 0 ... N ) ) )
37 36 anbi2d 
 |-  ( n = N -> ( ( ph /\ n e. ( 0 ... N ) ) <-> ( ph /\ N e. ( 0 ... N ) ) ) )
38 oveq2 
 |-  ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
39 38 sumeq1d 
 |-  ( n = N -> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) )
40 39 mpteq2dv 
 |-  ( n = N -> ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) )
41 40 eleq1d 
 |-  ( n = N -> ( ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) e. A <-> ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) )
42 37 41 imbi12d 
 |-  ( n = N -> ( ( ( ph /\ n e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... n ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) <-> ( ( ph /\ N e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) )
43 0z 
 |-  0 e. ZZ
44 fzsn 
 |-  ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
45 43 44 ax-mp 
 |-  ( 0 ... 0 ) = { 0 }
46 45 sumeq1i 
 |-  sum_ i e. ( 0 ... 0 ) ( E x. ( ( X ` i ) ` t ) ) = sum_ i e. { 0 } ( E x. ( ( X ` i ) ` t ) )
47 46 mpteq2i 
 |-  ( t e. T |-> sum_ i e. ( 0 ... 0 ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> sum_ i e. { 0 } ( E x. ( ( X ` i ) ` t ) ) )
48 7 adantr 
 |-  ( ( ph /\ t e. T ) -> E e. RR )
49 48 recnd 
 |-  ( ( ph /\ t e. T ) -> E e. CC )
50 nnz 
 |-  ( N e. NN -> N e. ZZ )
51 nngt0 
 |-  ( N e. NN -> 0 < N )
52 0re 
 |-  0 e. RR
53 nnre 
 |-  ( N e. NN -> N e. RR )
54 ltle 
 |-  ( ( 0 e. RR /\ N e. RR ) -> ( 0 < N -> 0 <_ N ) )
55 52 53 54 sylancr 
 |-  ( N e. NN -> ( 0 < N -> 0 <_ N ) )
56 51 55 mpd 
 |-  ( N e. NN -> 0 <_ N )
57 50 56 jca 
 |-  ( N e. NN -> ( N e. ZZ /\ 0 <_ N ) )
58 2 57 syl 
 |-  ( ph -> ( N e. ZZ /\ 0 <_ N ) )
59 43 eluz1i 
 |-  ( N e. ( ZZ>= ` 0 ) <-> ( N e. ZZ /\ 0 <_ N ) )
60 58 59 sylibr 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
61 eluzfz1 
 |-  ( N e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... N ) )
62 60 61 syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
63 3 62 ffvelrnd 
 |-  ( ph -> ( X ` 0 ) e. A )
64 feq1 
 |-  ( f = ( X ` 0 ) -> ( f : T --> RR <-> ( X ` 0 ) : T --> RR ) )
65 64 imbi2d 
 |-  ( f = ( X ` 0 ) -> ( ( ph -> f : T --> RR ) <-> ( ph -> ( X ` 0 ) : T --> RR ) ) )
66 8 expcom 
 |-  ( f e. A -> ( ph -> f : T --> RR ) )
67 65 66 vtoclga 
 |-  ( ( X ` 0 ) e. A -> ( ph -> ( X ` 0 ) : T --> RR ) )
68 63 67 mpcom 
 |-  ( ph -> ( X ` 0 ) : T --> RR )
69 68 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( ( X ` 0 ) ` t ) e. RR )
70 69 recnd 
 |-  ( ( ph /\ t e. T ) -> ( ( X ` 0 ) ` t ) e. CC )
71 49 70 mulcld 
 |-  ( ( ph /\ t e. T ) -> ( E x. ( ( X ` 0 ) ` t ) ) e. CC )
72 fveq2 
 |-  ( i = 0 -> ( X ` i ) = ( X ` 0 ) )
73 72 fveq1d 
 |-  ( i = 0 -> ( ( X ` i ) ` t ) = ( ( X ` 0 ) ` t ) )
74 73 oveq2d 
 |-  ( i = 0 -> ( E x. ( ( X ` i ) ` t ) ) = ( E x. ( ( X ` 0 ) ` t ) ) )
75 74 sumsn 
 |-  ( ( 0 e. ZZ /\ ( E x. ( ( X ` 0 ) ` t ) ) e. CC ) -> sum_ i e. { 0 } ( E x. ( ( X ` i ) ` t ) ) = ( E x. ( ( X ` 0 ) ` t ) ) )
76 43 71 75 sylancr 
 |-  ( ( ph /\ t e. T ) -> sum_ i e. { 0 } ( E x. ( ( X ` i ) ` t ) ) = ( E x. ( ( X ` 0 ) ` t ) ) )
77 1 76 mpteq2da 
 |-  ( ph -> ( t e. T |-> sum_ i e. { 0 } ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> ( E x. ( ( X ` 0 ) ` t ) ) ) )
78 47 77 syl5eq 
 |-  ( ph -> ( t e. T |-> sum_ i e. ( 0 ... 0 ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> ( E x. ( ( X ` 0 ) ` t ) ) ) )
79 1 5 6 8 7 63 stoweidlem2 
 |-  ( ph -> ( t e. T |-> ( E x. ( ( X ` 0 ) ` t ) ) ) e. A )
80 78 79 eqeltrd 
 |-  ( ph -> ( t e. T |-> sum_ i e. ( 0 ... 0 ) ( E x. ( ( X ` i ) ` t ) ) ) e. A )
81 80 adantr 
 |-  ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... 0 ) ( E x. ( ( X ` i ) ` t ) ) ) e. A )
82 eqidd 
 |-  ( r = t -> E = E )
83 82 cbvmptv 
 |-  ( r e. T |-> E ) = ( t e. T |-> E )
84 83 eqcomi 
 |-  ( t e. T |-> E ) = ( r e. T |-> E )
85 simpr 
 |-  ( ( ph /\ t e. T ) -> t e. T )
86 84 82 85 48 fvmptd3 
 |-  ( ( ph /\ t e. T ) -> ( ( t e. T |-> E ) ` t ) = E )
87 86 oveq1d 
 |-  ( ( ph /\ t e. T ) -> ( ( ( t e. T |-> E ) ` t ) x. ( ( X ` ( m + 1 ) ) ` t ) ) = ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) )
88 1 87 mpteq2da 
 |-  ( ph -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( ( X ` ( m + 1 ) ) ` t ) ) ) = ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) )
89 88 adantr 
 |-  ( ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( ( X ` ( m + 1 ) ) ` t ) ) ) = ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) )
90 3 ffvelrnda 
 |-  ( ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( X ` ( m + 1 ) ) e. A )
91 simpl 
 |-  ( ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ph )
92 id 
 |-  ( x = E -> x = E )
93 92 mpteq2dv 
 |-  ( x = E -> ( t e. T |-> x ) = ( t e. T |-> E ) )
94 93 eleq1d 
 |-  ( x = E -> ( ( t e. T |-> x ) e. A <-> ( t e. T |-> E ) e. A ) )
95 94 imbi2d 
 |-  ( x = E -> ( ( ph -> ( t e. T |-> x ) e. A ) <-> ( ph -> ( t e. T |-> E ) e. A ) ) )
96 6 expcom 
 |-  ( x e. RR -> ( ph -> ( t e. T |-> x ) e. A ) )
97 95 96 vtoclga 
 |-  ( E e. RR -> ( ph -> ( t e. T |-> E ) e. A ) )
98 7 97 mpcom 
 |-  ( ph -> ( t e. T |-> E ) e. A )
99 98 adantr 
 |-  ( ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( t e. T |-> E ) e. A )
100 fveq1 
 |-  ( g = ( X ` ( m + 1 ) ) -> ( g ` t ) = ( ( X ` ( m + 1 ) ) ` t ) )
101 100 oveq2d 
 |-  ( g = ( X ` ( m + 1 ) ) -> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) = ( ( ( t e. T |-> E ) ` t ) x. ( ( X ` ( m + 1 ) ) ` t ) ) )
102 101 mpteq2dv 
 |-  ( g = ( X ` ( m + 1 ) ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( ( X ` ( m + 1 ) ) ` t ) ) ) )
103 102 eleq1d 
 |-  ( g = ( X ` ( m + 1 ) ) -> ( ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) e. A <-> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( ( X ` ( m + 1 ) ) ` t ) ) ) e. A ) )
104 103 imbi2d 
 |-  ( g = ( X ` ( m + 1 ) ) -> ( ( ( ph /\ ( t e. T |-> E ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) e. A ) <-> ( ( ph /\ ( t e. T |-> E ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( ( X ` ( m + 1 ) ) ` t ) ) ) e. A ) ) )
105 83 eleq1i 
 |-  ( ( r e. T |-> E ) e. A <-> ( t e. T |-> E ) e. A )
106 fveq1 
 |-  ( f = ( r e. T |-> E ) -> ( f ` t ) = ( ( r e. T |-> E ) ` t ) )
107 83 fveq1i 
 |-  ( ( r e. T |-> E ) ` t ) = ( ( t e. T |-> E ) ` t )
108 106 107 eqtrdi 
 |-  ( f = ( r e. T |-> E ) -> ( f ` t ) = ( ( t e. T |-> E ) ` t ) )
109 108 oveq1d 
 |-  ( f = ( r e. T |-> E ) -> ( ( f ` t ) x. ( g ` t ) ) = ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) )
110 109 mpteq2dv 
 |-  ( f = ( r e. T |-> E ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) )
111 110 eleq1d 
 |-  ( f = ( r e. T |-> E ) -> ( ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A <-> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) e. A ) )
112 111 imbi2d 
 |-  ( f = ( r e. T |-> E ) -> ( ( ( ph /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A ) <-> ( ( ph /\ g e. A ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) e. A ) ) )
113 5 3com12 
 |-  ( ( f e. A /\ ph /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
114 113 3expib 
 |-  ( f e. A -> ( ( ph /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A ) )
115 112 114 vtoclga 
 |-  ( ( r e. T |-> E ) e. A -> ( ( ph /\ g e. A ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) e. A ) )
116 105 115 sylbir 
 |-  ( ( t e. T |-> E ) e. A -> ( ( ph /\ g e. A ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) e. A ) )
117 116 3impib 
 |-  ( ( ( t e. T |-> E ) e. A /\ ph /\ g e. A ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) e. A )
118 117 3com13 
 |-  ( ( g e. A /\ ph /\ ( t e. T |-> E ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) e. A )
119 118 3expib 
 |-  ( g e. A -> ( ( ph /\ ( t e. T |-> E ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( g ` t ) ) ) e. A ) )
120 104 119 vtoclga 
 |-  ( ( X ` ( m + 1 ) ) e. A -> ( ( ph /\ ( t e. T |-> E ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( ( X ` ( m + 1 ) ) ` t ) ) ) e. A ) )
121 120 3impib 
 |-  ( ( ( X ` ( m + 1 ) ) e. A /\ ph /\ ( t e. T |-> E ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( ( X ` ( m + 1 ) ) ` t ) ) ) e. A )
122 90 91 99 121 syl3anc 
 |-  ( ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( t e. T |-> ( ( ( t e. T |-> E ) ` t ) x. ( ( X ` ( m + 1 ) ) ` t ) ) ) e. A )
123 89 122 eqeltrrd 
 |-  ( ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) e. A )
124 123 ad2antll 
 |-  ( ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) /\ ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) ) -> ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) e. A )
125 simprrl 
 |-  ( ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) /\ ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) ) -> ph )
126 simpl 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> m e. NN0 )
127 simprl 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> ph )
128 2 ad2antrl 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> N e. NN )
129 128 nnnn0d 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> N e. NN0 )
130 nn0re 
 |-  ( m e. NN0 -> m e. RR )
131 130 adantr 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> m e. RR )
132 peano2nn0 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN0 )
133 132 nn0red 
 |-  ( m e. NN0 -> ( m + 1 ) e. RR )
134 133 adantr 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> ( m + 1 ) e. RR )
135 2 nnred 
 |-  ( ph -> N e. RR )
136 135 ad2antrl 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> N e. RR )
137 lep1 
 |-  ( m e. RR -> m <_ ( m + 1 ) )
138 126 130 137 3syl 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> m <_ ( m + 1 ) )
139 elfzle2 
 |-  ( ( m + 1 ) e. ( 0 ... N ) -> ( m + 1 ) <_ N )
140 139 ad2antll 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> ( m + 1 ) <_ N )
141 131 134 136 138 140 letrd 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> m <_ N )
142 elfz2nn0 
 |-  ( m e. ( 0 ... N ) <-> ( m e. NN0 /\ N e. NN0 /\ m <_ N ) )
143 126 129 141 142 syl3anbrc 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> m e. ( 0 ... N ) )
144 126 127 143 jca32 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> ( m e. NN0 /\ ( ph /\ m e. ( 0 ... N ) ) ) )
145 144 adantl 
 |-  ( ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) /\ ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) ) -> ( m e. NN0 /\ ( ph /\ m e. ( 0 ... N ) ) ) )
146 pm3.31 
 |-  ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) -> ( ( m e. NN0 /\ ( ph /\ m e. ( 0 ... N ) ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) )
147 146 adantr 
 |-  ( ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) /\ ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) ) -> ( ( m e. NN0 /\ ( ph /\ m e. ( 0 ... N ) ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) )
148 145 147 mpd 
 |-  ( ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) /\ ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A )
149 fveq2 
 |-  ( r = t -> ( ( X ` ( m + 1 ) ) ` r ) = ( ( X ` ( m + 1 ) ) ` t ) )
150 149 oveq2d 
 |-  ( r = t -> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) = ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) )
151 150 cbvmptv 
 |-  ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) = ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) )
152 151 eleq1i 
 |-  ( ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) e. A <-> ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) e. A )
153 fveq1 
 |-  ( g = ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) -> ( g ` t ) = ( ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) ` t ) )
154 151 fveq1i 
 |-  ( ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) ` t ) = ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t )
155 153 154 eqtrdi 
 |-  ( g = ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) -> ( g ` t ) = ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) )
156 155 oveq2d 
 |-  ( g = ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) -> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) = ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) )
157 156 mpteq2dv 
 |-  ( g = ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) = ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) ) )
158 157 eleq1d 
 |-  ( g = ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) -> ( ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) e. A <-> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) ) e. A ) )
159 158 imbi2d 
 |-  ( g = ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) -> ( ( ( ph /\ ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) e. A ) <-> ( ( ph /\ ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) ) e. A ) ) )
160 fveq2 
 |-  ( r = t -> ( ( X ` i ) ` r ) = ( ( X ` i ) ` t ) )
161 160 oveq2d 
 |-  ( r = t -> ( E x. ( ( X ` i ) ` r ) ) = ( E x. ( ( X ` i ) ` t ) ) )
162 161 sumeq2sdv 
 |-  ( r = t -> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) = sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) )
163 162 cbvmptv 
 |-  ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) = ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) )
164 163 eleq1i 
 |-  ( ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) e. A <-> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A )
165 fveq1 
 |-  ( f = ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) -> ( f ` t ) = ( ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) ` t ) )
166 163 fveq1i 
 |-  ( ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) ` t ) = ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t )
167 165 166 eqtrdi 
 |-  ( f = ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) -> ( f ` t ) = ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) )
168 167 oveq1d 
 |-  ( f = ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) -> ( ( f ` t ) + ( g ` t ) ) = ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) )
169 168 mpteq2dv 
 |-  ( f = ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) = ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) )
170 169 eleq1d 
 |-  ( f = ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) -> ( ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A <-> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) e. A ) )
171 170 imbi2d 
 |-  ( f = ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) -> ( ( ( ph /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A ) <-> ( ( ph /\ g e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) e. A ) ) )
172 4 3com12 
 |-  ( ( f e. A /\ ph /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
173 172 3expib 
 |-  ( f e. A -> ( ( ph /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A ) )
174 171 173 vtoclga 
 |-  ( ( r e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` r ) ) ) e. A -> ( ( ph /\ g e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) e. A ) )
175 164 174 sylbir 
 |-  ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A -> ( ( ph /\ g e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) e. A ) )
176 175 3impib 
 |-  ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A /\ ph /\ g e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) e. A )
177 176 3com13 
 |-  ( ( g e. A /\ ph /\ ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) e. A )
178 177 3expib 
 |-  ( g e. A -> ( ( ph /\ ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( g ` t ) ) ) e. A ) )
179 159 178 vtoclga 
 |-  ( ( r e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` r ) ) ) e. A -> ( ( ph /\ ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) ) e. A ) )
180 152 179 sylbir 
 |-  ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) e. A -> ( ( ph /\ ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) ) e. A ) )
181 180 3impib 
 |-  ( ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) e. A /\ ph /\ ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) ) e. A )
182 124 125 148 181 syl3anc 
 |-  ( ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) /\ ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) ) -> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) ) e. A )
183 3anass 
 |-  ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) <-> ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) )
184 183 biimpri 
 |-  ( ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) -> ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) )
185 184 adantl 
 |-  ( ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) /\ ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) ) -> ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) )
186 nfv 
 |-  F/ t m e. NN0
187 nfv 
 |-  F/ t ( m + 1 ) e. ( 0 ... N )
188 186 1 187 nf3an 
 |-  F/ t ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) )
189 simpr 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> t e. T )
190 fzfid 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( 0 ... m ) e. Fin )
191 7 3ad2ant2 
 |-  ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> E e. RR )
192 191 adantr 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> E e. RR )
193 192 adantr 
 |-  ( ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) /\ i e. ( 0 ... m ) ) -> E e. RR )
194 fzelp1 
 |-  ( i e. ( 0 ... m ) -> i e. ( 0 ... ( m + 1 ) ) )
195 194 anim2i 
 |-  ( ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) /\ i e. ( 0 ... m ) ) -> ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) /\ i e. ( 0 ... ( m + 1 ) ) ) )
196 an32 
 |-  ( ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) /\ i e. ( 0 ... ( m + 1 ) ) ) <-> ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ i e. ( 0 ... ( m + 1 ) ) ) /\ t e. T ) )
197 195 196 sylib 
 |-  ( ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) /\ i e. ( 0 ... m ) ) -> ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ i e. ( 0 ... ( m + 1 ) ) ) /\ t e. T ) )
198 3 3ad2ant2 
 |-  ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> X : ( 0 ... N ) --> A )
199 198 adantr 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ i e. ( 0 ... ( m + 1 ) ) ) -> X : ( 0 ... N ) --> A )
200 elfzuz3 
 |-  ( ( m + 1 ) e. ( 0 ... N ) -> N e. ( ZZ>= ` ( m + 1 ) ) )
201 fzss2 
 |-  ( N e. ( ZZ>= ` ( m + 1 ) ) -> ( 0 ... ( m + 1 ) ) C_ ( 0 ... N ) )
202 200 201 syl 
 |-  ( ( m + 1 ) e. ( 0 ... N ) -> ( 0 ... ( m + 1 ) ) C_ ( 0 ... N ) )
203 202 sselda 
 |-  ( ( ( m + 1 ) e. ( 0 ... N ) /\ i e. ( 0 ... ( m + 1 ) ) ) -> i e. ( 0 ... N ) )
204 203 3ad2antl3 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ i e. ( 0 ... ( m + 1 ) ) ) -> i e. ( 0 ... N ) )
205 199 204 ffvelrnd 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ i e. ( 0 ... ( m + 1 ) ) ) -> ( X ` i ) e. A )
206 simpl2 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ i e. ( 0 ... ( m + 1 ) ) ) -> ph )
207 feq1 
 |-  ( f = ( X ` i ) -> ( f : T --> RR <-> ( X ` i ) : T --> RR ) )
208 207 imbi2d 
 |-  ( f = ( X ` i ) -> ( ( ph -> f : T --> RR ) <-> ( ph -> ( X ` i ) : T --> RR ) ) )
209 208 66 vtoclga 
 |-  ( ( X ` i ) e. A -> ( ph -> ( X ` i ) : T --> RR ) )
210 205 206 209 sylc 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ i e. ( 0 ... ( m + 1 ) ) ) -> ( X ` i ) : T --> RR )
211 210 ffvelrnda 
 |-  ( ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ i e. ( 0 ... ( m + 1 ) ) ) /\ t e. T ) -> ( ( X ` i ) ` t ) e. RR )
212 197 211 syl 
 |-  ( ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) /\ i e. ( 0 ... m ) ) -> ( ( X ` i ) ` t ) e. RR )
213 193 212 remulcld 
 |-  ( ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) /\ i e. ( 0 ... m ) ) -> ( E x. ( ( X ` i ) ` t ) ) e. RR )
214 190 213 fsumrecl 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) e. RR )
215 eqid 
 |-  ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) )
216 215 fvmpt2 
 |-  ( ( t e. T /\ sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) e. RR ) -> ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) = sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) )
217 189 214 216 syl2anc 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) = sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) )
218 217 oveq1d 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) = ( sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) + ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) )
219 3simpc 
 |-  ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) )
220 219 adantr 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) )
221 feq1 
 |-  ( f = ( X ` ( m + 1 ) ) -> ( f : T --> RR <-> ( X ` ( m + 1 ) ) : T --> RR ) )
222 221 imbi2d 
 |-  ( f = ( X ` ( m + 1 ) ) -> ( ( ph -> f : T --> RR ) <-> ( ph -> ( X ` ( m + 1 ) ) : T --> RR ) ) )
223 222 66 vtoclga 
 |-  ( ( X ` ( m + 1 ) ) e. A -> ( ph -> ( X ` ( m + 1 ) ) : T --> RR ) )
224 90 91 223 sylc 
 |-  ( ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( X ` ( m + 1 ) ) : T --> RR )
225 220 224 syl 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( X ` ( m + 1 ) ) : T --> RR )
226 225 189 ffvelrnd 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( ( X ` ( m + 1 ) ) ` t ) e. RR )
227 192 226 remulcld 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) e. RR )
228 eqid 
 |-  ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) = ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) )
229 228 fvmpt2 
 |-  ( ( t e. T /\ ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) e. RR ) -> ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) = ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) )
230 189 227 229 syl2anc 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) = ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) )
231 230 oveq2d 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) = ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) )
232 elfzuz 
 |-  ( ( m + 1 ) e. ( 0 ... N ) -> ( m + 1 ) e. ( ZZ>= ` 0 ) )
233 232 3ad2ant3 
 |-  ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( m + 1 ) e. ( ZZ>= ` 0 ) )
234 233 adantr 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( m + 1 ) e. ( ZZ>= ` 0 ) )
235 192 adantr 
 |-  ( ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) /\ i e. ( 0 ... ( m + 1 ) ) ) -> E e. RR )
236 211 an32s 
 |-  ( ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) /\ i e. ( 0 ... ( m + 1 ) ) ) -> ( ( X ` i ) ` t ) e. RR )
237 remulcl 
 |-  ( ( E e. RR /\ ( ( X ` i ) ` t ) e. RR ) -> ( E x. ( ( X ` i ) ` t ) ) e. RR )
238 237 recnd 
 |-  ( ( E e. RR /\ ( ( X ` i ) ` t ) e. RR ) -> ( E x. ( ( X ` i ) ` t ) ) e. CC )
239 235 236 238 syl2anc 
 |-  ( ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) /\ i e. ( 0 ... ( m + 1 ) ) ) -> ( E x. ( ( X ` i ) ` t ) ) e. CC )
240 fveq2 
 |-  ( i = ( m + 1 ) -> ( X ` i ) = ( X ` ( m + 1 ) ) )
241 240 fveq1d 
 |-  ( i = ( m + 1 ) -> ( ( X ` i ) ` t ) = ( ( X ` ( m + 1 ) ) ` t ) )
242 241 oveq2d 
 |-  ( i = ( m + 1 ) -> ( E x. ( ( X ` i ) ` t ) ) = ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) )
243 234 239 242 fsumm1 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) = ( sum_ i e. ( 0 ... ( ( m + 1 ) - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) + ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) )
244 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
245 244 3ad2ant1 
 |-  ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> m e. CC )
246 245 adantr 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> m e. CC )
247 1cnd 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> 1 e. CC )
248 246 247 pncand 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( ( m + 1 ) - 1 ) = m )
249 248 oveq2d 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( 0 ... ( ( m + 1 ) - 1 ) ) = ( 0 ... m ) )
250 249 sumeq1d 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> sum_ i e. ( 0 ... ( ( m + 1 ) - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) = sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) )
251 250 oveq1d 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> ( sum_ i e. ( 0 ... ( ( m + 1 ) - 1 ) ) ( E x. ( ( X ` i ) ` t ) ) + ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) = ( sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) + ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) )
252 243 251 eqtrd 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) = ( sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) + ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) )
253 218 231 252 3eqtr4rd 
 |-  ( ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) /\ t e. T ) -> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) = ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) )
254 188 253 mpteq2da 
 |-  ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) ) )
255 254 eleq1d 
 |-  ( ( m e. NN0 /\ ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( ( t e. T |-> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) ) e. A <-> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) ) e. A ) )
256 185 255 syl 
 |-  ( ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) /\ ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) ) -> ( ( t e. T |-> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) ) e. A <-> ( t e. T |-> ( ( ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) + ( ( t e. T |-> ( E x. ( ( X ` ( m + 1 ) ) ` t ) ) ) ` t ) ) ) e. A ) )
257 182 256 mpbird 
 |-  ( ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) /\ ( m e. NN0 /\ ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) ) ) -> ( t e. T |-> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) ) e. A )
258 257 exp32 
 |-  ( ( m e. NN0 -> ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) -> ( m e. NN0 -> ( ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) )
259 258 pm2.86i 
 |-  ( m e. NN0 -> ( ( ( ph /\ m e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... m ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) -> ( ( ph /\ ( m + 1 ) e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... ( m + 1 ) ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) ) )
260 21 28 35 42 81 259 nn0ind 
 |-  ( N e. NN0 -> ( ( ph /\ N e. ( 0 ... N ) ) -> ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) e. A ) )
261 9 14 260 sylc 
 |-  ( ph -> ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) e. A )