Metamath Proof Explorer

Theorem dvnmul

Description: Function-builder for the N -th derivative, product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvnmul.s 
|- ( ph -> S e. { RR , CC } )
dvnmul.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
dvnmul.a 
|- ( ( ph /\ x e. X ) -> A e. CC )
dvnmul.cc 
|- ( ( ph /\ x e. X ) -> B e. CC )
dvnmul.n 
|- ( ph -> N e. NN0 )
dvnmulf 
|- F = ( x e. X |-> A )
dvnmul.f 
|- G = ( x e. X |-> B )
dvnmul.dvnf 
|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) : X --> CC )
dvnmul.dvng 
|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) : X --> CC )
dvnmul.c 
|- C = ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) )
dvnmul.d 
|- D = ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) )
Assertion dvnmul 
|- ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dvnmul.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvnmul.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 dvnmul.a 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
4 dvnmul.cc 
 |-  ( ( ph /\ x e. X ) -> B e. CC )
5 dvnmul.n 
 |-  ( ph -> N e. NN0 )
6 dvnmulf 
 |-  F = ( x e. X |-> A )
7 dvnmul.f 
 |-  G = ( x e. X |-> B )
8 dvnmul.dvnf 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) : X --> CC )
9 dvnmul.dvng 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) : X --> CC )
10 dvnmul.c 
 |-  C = ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) )
11 dvnmul.d 
 |-  D = ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) )
12 id 
 |-  ( ph -> ph )
13 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
14 5 13 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
15 eluzfz2 
 |-  ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) )
16 14 15 syl 
 |-  ( ph -> N e. ( 0 ... N ) )
17 eleq1 
 |-  ( n = N -> ( n e. ( 0 ... N ) <-> N e. ( 0 ... N ) ) )
18 fveq2 
 |-  ( n = N -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) )
19 oveq2 
 |-  ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
20 19 sumeq1d 
 |-  ( n = N -> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... N ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) )
21 oveq1 
 |-  ( n = N -> ( n _C k ) = ( N _C k ) )
22 fvoveq1 
 |-  ( n = N -> ( D ` ( n - k ) ) = ( D ` ( N - k ) ) )
23 22 fveq1d 
 |-  ( n = N -> ( ( D ` ( n - k ) ) ` x ) = ( ( D ` ( N - k ) ) ` x ) )
24 23 oveq2d 
 |-  ( n = N -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) )
25 21 24 oveq12d 
 |-  ( n = N -> ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) = ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) )
26 25 sumeq2sdv 
 |-  ( n = N -> sum_ k e. ( 0 ... N ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) )
27 20 26 eqtrd 
 |-  ( n = N -> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) )
28 27 mpteq2dv 
 |-  ( n = N -> ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) )
29 18 28 eqeq12d 
 |-  ( n = N -> ( ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) <-> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) ) )
30 29 imbi2d 
 |-  ( n = N -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) ) ) )
31 17 30 imbi12d 
 |-  ( n = N -> ( ( n e. ( 0 ... N ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) ) ) <-> ( N e. ( 0 ... N ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) ) ) ) )
32 fveq2 
 |-  ( m = 0 -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) )
33 simpl 
 |-  ( ( m = 0 /\ x e. X ) -> m = 0 )
34 33 oveq2d 
 |-  ( ( m = 0 /\ x e. X ) -> ( 0 ... m ) = ( 0 ... 0 ) )
35 simpll 
 |-  ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> m = 0 )
36 35 oveq1d 
 |-  ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( m _C k ) = ( 0 _C k ) )
37 35 fvoveq1d 
 |-  ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( D ` ( m - k ) ) = ( D ` ( 0 - k ) ) )
38 37 fveq1d 
 |-  ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( 0 - k ) ) ` x ) )
39 38 oveq2d 
 |-  ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) )
40 36 39 oveq12d 
 |-  ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) )
41 34 40 sumeq12rdv 
 |-  ( ( m = 0 /\ x e. X ) -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) )
42 41 mpteq2dva 
 |-  ( m = 0 -> ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) )
43 32 42 eqeq12d 
 |-  ( m = 0 -> ( ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) <-> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) ) )
44 43 imbi2d 
 |-  ( m = 0 -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) ) ) )
45 fveq2 
 |-  ( m = i -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) )
46 simpl 
 |-  ( ( m = i /\ x e. X ) -> m = i )
47 46 oveq2d 
 |-  ( ( m = i /\ x e. X ) -> ( 0 ... m ) = ( 0 ... i ) )
48 simpll 
 |-  ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> m = i )
49 48 oveq1d 
 |-  ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( m _C k ) = ( i _C k ) )
50 48 fvoveq1d 
 |-  ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( D ` ( m - k ) ) = ( D ` ( i - k ) ) )
51 50 fveq1d 
 |-  ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( i - k ) ) ` x ) )
52 51 oveq2d 
 |-  ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) )
53 49 52 oveq12d 
 |-  ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) )
54 47 53 sumeq12rdv 
 |-  ( ( m = i /\ x e. X ) -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) )
55 54 mpteq2dva 
 |-  ( m = i -> ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) )
56 45 55 eqeq12d 
 |-  ( m = i -> ( ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) <-> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) )
57 56 imbi2d 
 |-  ( m = i -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) ) )
58 fveq2 
 |-  ( m = ( i + 1 ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) )
59 simpl 
 |-  ( ( m = ( i + 1 ) /\ x e. X ) -> m = ( i + 1 ) )
60 59 oveq2d 
 |-  ( ( m = ( i + 1 ) /\ x e. X ) -> ( 0 ... m ) = ( 0 ... ( i + 1 ) ) )
61 simpll 
 |-  ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> m = ( i + 1 ) )
62 61 oveq1d 
 |-  ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( m _C k ) = ( ( i + 1 ) _C k ) )
63 61 fvoveq1d 
 |-  ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( D ` ( m - k ) ) = ( D ` ( ( i + 1 ) - k ) ) )
64 63 fveq1d 
 |-  ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - k ) ) ` x ) )
65 64 oveq2d 
 |-  ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
66 62 65 oveq12d 
 |-  ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
67 60 66 sumeq12rdv 
 |-  ( ( m = ( i + 1 ) /\ x e. X ) -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
68 67 mpteq2dva 
 |-  ( m = ( i + 1 ) -> ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
69 58 68 eqeq12d 
 |-  ( m = ( i + 1 ) -> ( ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) <-> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
70 69 imbi2d 
 |-  ( m = ( i + 1 ) -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) ) )
71 fveq2 
 |-  ( m = n -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) )
72 simpl 
 |-  ( ( m = n /\ x e. X ) -> m = n )
73 72 oveq2d 
 |-  ( ( m = n /\ x e. X ) -> ( 0 ... m ) = ( 0 ... n ) )
74 simpll 
 |-  ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> m = n )
75 74 oveq1d 
 |-  ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( m _C k ) = ( n _C k ) )
76 74 fvoveq1d 
 |-  ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( D ` ( m - k ) ) = ( D ` ( n - k ) ) )
77 76 fveq1d 
 |-  ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( n - k ) ) ` x ) )
78 77 oveq2d 
 |-  ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) )
79 75 78 oveq12d 
 |-  ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) )
80 73 79 sumeq12rdv 
 |-  ( ( m = n /\ x e. X ) -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) )
81 80 mpteq2dva 
 |-  ( m = n -> ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) )
82 71 81 eqeq12d 
 |-  ( m = n -> ( ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) <-> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) ) )
83 82 imbi2d 
 |-  ( m = n -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) ) ) )
84 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
85 1 84 syl 
 |-  ( ph -> S C_ CC )
86 3 4 mulcld 
 |-  ( ( ph /\ x e. X ) -> ( A x. B ) e. CC )
87 restsspw 
 |-  ( ( TopOpen ` CCfld ) |`t S ) C_ ~P S
88 87 2 sselid 
 |-  ( ph -> X e. ~P S )
89 elpwi 
 |-  ( X e. ~P S -> X C_ S )
90 88 89 syl 
 |-  ( ph -> X C_ S )
91 cnex 
 |-  CC e. _V
92 91 a1i 
 |-  ( ph -> CC e. _V )
93 86 90 92 1 mptelpm 
 |-  ( ph -> ( x e. X |-> ( A x. B ) ) e. ( CC ^pm S ) )
94 dvn0 
 |-  ( ( S C_ CC /\ ( x e. X |-> ( A x. B ) ) e. ( CC ^pm S ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> ( A x. B ) ) )
95 85 93 94 syl2anc 
 |-  ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> ( A x. B ) ) )
96 0z 
 |-  0 e. ZZ
97 fzsn 
 |-  ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
98 96 97 ax-mp 
 |-  ( 0 ... 0 ) = { 0 }
99 98 sumeq1i 
 |-  sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) )
100 99 a1i 
 |-  ( ( ph /\ x e. X ) -> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) )
101 nfcvd 
 |-  ( ( ph /\ x e. X ) -> F/_ k ( A x. B ) )
102 nfv 
 |-  F/ k ( ph /\ x e. X )
103 oveq2 
 |-  ( k = 0 -> ( 0 _C k ) = ( 0 _C 0 ) )
104 0nn0 
 |-  0 e. NN0
105 bcn0 
 |-  ( 0 e. NN0 -> ( 0 _C 0 ) = 1 )
106 104 105 ax-mp 
 |-  ( 0 _C 0 ) = 1
107 106 a1i 
 |-  ( k = 0 -> ( 0 _C 0 ) = 1 )
108 103 107 eqtrd 
 |-  ( k = 0 -> ( 0 _C k ) = 1 )
109 108 adantl 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( 0 _C k ) = 1 )
110 fveq2 
 |-  ( k = 0 -> ( C ` k ) = ( C ` 0 ) )
111 110 adantl 
 |-  ( ( ph /\ k = 0 ) -> ( C ` k ) = ( C ` 0 ) )
112 fveq2 
 |-  ( k = n -> ( ( S Dn F ) ` k ) = ( ( S Dn F ) ` n ) )
113 112 cbvmptv 
 |-  ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) ) = ( n e. ( 0 ... N ) |-> ( ( S Dn F ) ` n ) )
114 10 113 eqtri 
 |-  C = ( n e. ( 0 ... N ) |-> ( ( S Dn F ) ` n ) )
115 fveq2 
 |-  ( n = 0 -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` 0 ) )
116 eluzfz1 
 |-  ( N e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... N ) )
117 14 116 syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
118 fvexd 
 |-  ( ph -> ( ( S Dn F ) ` 0 ) e. _V )
119 114 115 117 118 fvmptd3 
 |-  ( ph -> ( C ` 0 ) = ( ( S Dn F ) ` 0 ) )
120 119 adantr 
 |-  ( ( ph /\ k = 0 ) -> ( C ` 0 ) = ( ( S Dn F ) ` 0 ) )
121 111 120 eqtrd 
 |-  ( ( ph /\ k = 0 ) -> ( C ` k ) = ( ( S Dn F ) ` 0 ) )
122 3 90 92 1 mptelpm 
 |-  ( ph -> ( x e. X |-> A ) e. ( CC ^pm S ) )
123 6 122 eqeltrid 
 |-  ( ph -> F e. ( CC ^pm S ) )
124 dvn0 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
125 85 123 124 syl2anc 
 |-  ( ph -> ( ( S Dn F ) ` 0 ) = F )
126 125 adantr 
 |-  ( ( ph /\ k = 0 ) -> ( ( S Dn F ) ` 0 ) = F )
127 121 126 eqtrd 
 |-  ( ( ph /\ k = 0 ) -> ( C ` k ) = F )
128 127 fveq1d 
 |-  ( ( ph /\ k = 0 ) -> ( ( C ` k ) ` x ) = ( F ` x ) )
129 128 adantlr 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( C ` k ) ` x ) = ( F ` x ) )
130 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
131 6 fvmpt2 
 |-  ( ( x e. X /\ A e. CC ) -> ( F ` x ) = A )
132 130 3 131 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) = A )
133 132 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( F ` x ) = A )
134 129 133 eqtrd 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( C ` k ) ` x ) = A )
135 oveq2 
 |-  ( k = 0 -> ( 0 - k ) = ( 0 - 0 ) )
136 0m0e0 
 |-  ( 0 - 0 ) = 0
137 136 a1i 
 |-  ( k = 0 -> ( 0 - 0 ) = 0 )
138 135 137 eqtrd 
 |-  ( k = 0 -> ( 0 - k ) = 0 )
139 138 fveq2d 
 |-  ( k = 0 -> ( D ` ( 0 - k ) ) = ( D ` 0 ) )
140 139 fveq1d 
 |-  ( k = 0 -> ( ( D ` ( 0 - k ) ) ` x ) = ( ( D ` 0 ) ` x ) )
141 140 adantl 
 |-  ( ( ph /\ k = 0 ) -> ( ( D ` ( 0 - k ) ) ` x ) = ( ( D ` 0 ) ` x ) )
142 141 adantlr 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( D ` ( 0 - k ) ) ` x ) = ( ( D ` 0 ) ` x ) )
143 fveq2 
 |-  ( k = n -> ( ( S Dn G ) ` k ) = ( ( S Dn G ) ` n ) )
144 143 cbvmptv 
 |-  ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) ) = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) )
145 11 144 eqtri 
 |-  D = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) )
146 145 fveq1i 
 |-  ( D ` 0 ) = ( ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) ` 0 )
147 146 a1i 
 |-  ( ph -> ( D ` 0 ) = ( ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) ` 0 ) )
148 eqidd 
 |-  ( ph -> ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) )
149 fveq2 
 |-  ( n = 0 -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` 0 ) )
150 149 adantl 
 |-  ( ( ph /\ n = 0 ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` 0 ) )
151 4 90 92 1 mptelpm 
 |-  ( ph -> ( x e. X |-> B ) e. ( CC ^pm S ) )
152 7 151 eqeltrid 
 |-  ( ph -> G e. ( CC ^pm S ) )
153 dvn0 
 |-  ( ( S C_ CC /\ G e. ( CC ^pm S ) ) -> ( ( S Dn G ) ` 0 ) = G )
154 85 152 153 syl2anc 
 |-  ( ph -> ( ( S Dn G ) ` 0 ) = G )
155 154 adantr 
 |-  ( ( ph /\ n = 0 ) -> ( ( S Dn G ) ` 0 ) = G )
156 150 155 eqtrd 
 |-  ( ( ph /\ n = 0 ) -> ( ( S Dn G ) ` n ) = G )
157 7 a1i 
 |-  ( ph -> G = ( x e. X |-> B ) )
158 mptexg 
 |-  ( X e. ~P S -> ( x e. X |-> B ) e. _V )
159 88 158 syl 
 |-  ( ph -> ( x e. X |-> B ) e. _V )
160 157 159 eqeltrd 
 |-  ( ph -> G e. _V )
161 148 156 117 160 fvmptd 
 |-  ( ph -> ( ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) ` 0 ) = G )
162 147 161 eqtrd 
 |-  ( ph -> ( D ` 0 ) = G )
163 162 fveq1d 
 |-  ( ph -> ( ( D ` 0 ) ` x ) = ( G ` x ) )
164 163 ad2antrr 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( D ` 0 ) ` x ) = ( G ` x ) )
165 157 4 fvmpt2d 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) = B )
166 165 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( G ` x ) = B )
167 142 164 166 3eqtrd 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( D ` ( 0 - k ) ) ` x ) = B )
168 134 167 oveq12d 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) = ( A x. B ) )
169 109 168 oveq12d 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = ( 1 x. ( A x. B ) ) )
170 86 mullidd 
 |-  ( ( ph /\ x e. X ) -> ( 1 x. ( A x. B ) ) = ( A x. B ) )
171 170 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( 1 x. ( A x. B ) ) = ( A x. B ) )
172 169 171 eqtrd 
 |-  ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = ( A x. B ) )
173 0re 
 |-  0 e. RR
174 173 a1i 
 |-  ( ( ph /\ x e. X ) -> 0 e. RR )
175 101 102 172 174 86 sumsnd 
 |-  ( ( ph /\ x e. X ) -> sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = ( A x. B ) )
176 100 175 eqtr2d 
 |-  ( ( ph /\ x e. X ) -> ( A x. B ) = sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) )
177 176 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( A x. B ) ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) )
178 95 177 eqtrd 
 |-  ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) )
179 178 a1i 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) ) )
180 simp3 
 |-  ( ( i e. ( 0 ..^ N ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) /\ ph ) -> ph )
181 simp1 
 |-  ( ( i e. ( 0 ..^ N ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) /\ ph ) -> i e. ( 0 ..^ N ) )
182 simp2 
 |-  ( ( i e. ( 0 ..^ N ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) /\ ph ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) )
183 pm3.35 
 |-  ( ( ph /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) )
184 180 182 183 syl2anc 
 |-  ( ( i e. ( 0 ..^ N ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) /\ ph ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) )
185 85 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> S C_ CC )
186 93 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( x e. X |-> ( A x. B ) ) e. ( CC ^pm S ) )
187 elfzonn0 
 |-  ( i e. ( 0 ..^ N ) -> i e. NN0 )
188 187 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> i e. NN0 )
189 dvnp1 
 |-  ( ( S C_ CC /\ ( x e. X |-> ( A x. B ) ) e. ( CC ^pm S ) /\ i e. NN0 ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) ) )
190 185 186 188 189 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) ) )
191 190 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) ) )
192 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) )
193 192 oveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( S _D ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) ) = ( S _D ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) )
194 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
195 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
196 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> S e. { RR , CC } )
197 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
198 fzfid 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( 0 ... i ) e. Fin )
199 187 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. NN0 )
200 elfzelz 
 |-  ( k e. ( 0 ... i ) -> k e. ZZ )
201 200 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. ZZ )
202 199 201 bccld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. NN0 )
203 202 nn0cnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. CC )
204 203 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. CC )
205 204 3adant3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( i _C k ) e. CC )
206 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ph )
207 0zd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 e. ZZ )
208 elfzoel2 
 |-  ( i e. ( 0 ..^ N ) -> N e. ZZ )
209 208 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> N e. ZZ )
210 elfzle1 
 |-  ( k e. ( 0 ... i ) -> 0 <_ k )
211 210 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ k )
212 201 zred 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. RR )
213 208 zred 
 |-  ( i e. ( 0 ..^ N ) -> N e. RR )
214 213 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> N e. RR )
215 187 nn0red 
 |-  ( i e. ( 0 ..^ N ) -> i e. RR )
216 215 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. RR )
217 elfzle2 
 |-  ( k e. ( 0 ... i ) -> k <_ i )
218 217 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ i )
219 elfzolt2 
 |-  ( i e. ( 0 ..^ N ) -> i < N )
220 219 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i < N )
221 212 216 214 218 220 lelttrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k < N )
222 212 214 221 ltled 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ N )
223 207 209 201 211 222 elfzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. ( 0 ... N ) )
224 223 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> k e. ( 0 ... N ) )
225 10 a1i 
 |-  ( ph -> C = ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) ) )
226 fvexd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) e. _V )
227 225 226 fvmpt2d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) = ( ( S Dn F ) ` k ) )
228 227 feq1d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( C ` k ) : X --> CC <-> ( ( S Dn F ) ` k ) : X --> CC ) )
229 8 228 mpbird 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC )
230 206 224 229 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` k ) : X --> CC )
231 230 3adant3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( C ` k ) : X --> CC )
232 simp3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> x e. X )
233 231 232 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( C ` k ) ` x ) e. CC )
234 187 nn0zd 
 |-  ( i e. ( 0 ..^ N ) -> i e. ZZ )
235 234 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. ZZ )
236 235 201 zsubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ZZ )
237 elfzel2 
 |-  ( k e. ( 0 ... i ) -> i e. ZZ )
238 237 zred 
 |-  ( k e. ( 0 ... i ) -> i e. RR )
239 200 zred 
 |-  ( k e. ( 0 ... i ) -> k e. RR )
240 238 239 subge0d 
 |-  ( k e. ( 0 ... i ) -> ( 0 <_ ( i - k ) <-> k <_ i ) )
241 217 240 mpbird 
 |-  ( k e. ( 0 ... i ) -> 0 <_ ( i - k ) )
242 241 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( i - k ) )
243 216 212 resubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. RR )
244 214 212 resubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) e. RR )
245 173 a1i 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 e. RR )
246 214 245 jca 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N e. RR /\ 0 e. RR ) )
247 resubcl 
 |-  ( ( N e. RR /\ 0 e. RR ) -> ( N - 0 ) e. RR )
248 246 247 syl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - 0 ) e. RR )
249 216 214 212 220 ltsub1dd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < ( N - k ) )
250 245 212 214 211 lesub2dd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) <_ ( N - 0 ) )
251 243 244 248 249 250 ltletrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < ( N - 0 ) )
252 213 recnd 
 |-  ( i e. ( 0 ..^ N ) -> N e. CC )
253 252 subid1d 
 |-  ( i e. ( 0 ..^ N ) -> ( N - 0 ) = N )
254 253 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - 0 ) = N )
255 251 254 breqtrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < N )
256 243 214 255 ltled 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) <_ N )
257 207 209 236 242 256 elfzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ( 0 ... N ) )
258 257 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ( 0 ... N ) )
259 ovex 
 |-  ( i - k ) e. _V
260 eleq1 
 |-  ( j = ( i - k ) -> ( j e. ( 0 ... N ) <-> ( i - k ) e. ( 0 ... N ) ) )
261 260 anbi2d 
 |-  ( j = ( i - k ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( i - k ) e. ( 0 ... N ) ) ) )
262 fveq2 
 |-  ( j = ( i - k ) -> ( ( S Dn G ) ` j ) = ( ( S Dn G ) ` ( i - k ) ) )
263 262 feq1d 
 |-  ( j = ( i - k ) -> ( ( ( S Dn G ) ` j ) : X --> CC <-> ( ( S Dn G ) ` ( i - k ) ) : X --> CC ) )
264 261 263 imbi12d 
 |-  ( j = ( i - k ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC ) <-> ( ( ph /\ ( i - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( i - k ) ) : X --> CC ) ) )
265 nfv 
 |-  F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC )
266 eleq1 
 |-  ( k = j -> ( k e. ( 0 ... N ) <-> j e. ( 0 ... N ) ) )
267 266 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ j e. ( 0 ... N ) ) ) )
268 fveq2 
 |-  ( k = j -> ( ( S Dn G ) ` k ) = ( ( S Dn G ) ` j ) )
269 268 feq1d 
 |-  ( k = j -> ( ( ( S Dn G ) ` k ) : X --> CC <-> ( ( S Dn G ) ` j ) : X --> CC ) )
270 267 269 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC ) ) )
271 265 270 9 chvarfv 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC )
272 259 264 271 vtocl 
 |-  ( ( ph /\ ( i - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( i - k ) ) : X --> CC )
273 206 258 272 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) : X --> CC )
274 fveq2 
 |-  ( n = ( i - k ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` ( i - k ) ) )
275 fvexd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) e. _V )
276 145 274 257 275 fvmptd3 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( ( S Dn G ) ` ( i - k ) ) )
277 276 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( ( S Dn G ) ` ( i - k ) ) )
278 277 feq1d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( i - k ) ) : X --> CC <-> ( ( S Dn G ) ` ( i - k ) ) : X --> CC ) )
279 273 278 mpbird 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) : X --> CC )
280 279 3adant3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( D ` ( i - k ) ) : X --> CC )
281 280 232 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( D ` ( i - k ) ) ` x ) e. CC )
282 233 281 mulcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
283 205 282 mulcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) e. CC )
284 205 3expa 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( i _C k ) e. CC )
285 235 peano2zd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. ZZ )
286 285 201 zsubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ZZ )
287 peano2re 
 |-  ( i e. RR -> ( i + 1 ) e. RR )
288 238 287 syl 
 |-  ( k e. ( 0 ... i ) -> ( i + 1 ) e. RR )
289 peano2re 
 |-  ( k e. RR -> ( k + 1 ) e. RR )
290 239 289 syl 
 |-  ( k e. ( 0 ... i ) -> ( k + 1 ) e. RR )
291 239 ltp1d 
 |-  ( k e. ( 0 ... i ) -> k < ( k + 1 ) )
292 1red 
 |-  ( k e. ( 0 ... i ) -> 1 e. RR )
293 239 238 292 217 leadd1dd 
 |-  ( k e. ( 0 ... i ) -> ( k + 1 ) <_ ( i + 1 ) )
294 239 290 288 291 293 ltletrd 
 |-  ( k e. ( 0 ... i ) -> k < ( i + 1 ) )
295 239 288 294 ltled 
 |-  ( k e. ( 0 ... i ) -> k <_ ( i + 1 ) )
296 295 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ ( i + 1 ) )
297 216 287 syl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. RR )
298 297 212 subge0d 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 <_ ( ( i + 1 ) - k ) <-> k <_ ( i + 1 ) ) )
299 296 298 mpbird 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( ( i + 1 ) - k ) )
300 297 212 resubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. RR )
301 elfzop1le2 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) <_ N )
302 301 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) <_ N )
303 297 214 212 302 lesub1dd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) <_ ( N - k ) )
304 250 254 breqtrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) <_ N )
305 300 244 214 303 304 letrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) <_ N )
306 207 209 286 299 305 elfzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
307 306 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
308 ovex 
 |-  ( ( i + 1 ) - k ) e. _V
309 eleq1 
 |-  ( j = ( ( i + 1 ) - k ) -> ( j e. ( 0 ... N ) <-> ( ( i + 1 ) - k ) e. ( 0 ... N ) ) )
310 309 anbi2d 
 |-  ( j = ( ( i + 1 ) - k ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) ) )
311 fveq2 
 |-  ( j = ( ( i + 1 ) - k ) -> ( ( S Dn G ) ` j ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
312 311 feq1d 
 |-  ( j = ( ( i + 1 ) - k ) -> ( ( ( S Dn G ) ` j ) : X --> CC <-> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC ) )
313 310 312 imbi12d 
 |-  ( j = ( ( i + 1 ) - k ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC ) <-> ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC ) ) )
314 308 313 271 vtocl 
 |-  ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC )
315 206 307 314 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC )
316 145 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> D = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) )
317 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ n = ( ( i + 1 ) - k ) ) -> n = ( ( i + 1 ) - k ) )
318 317 fveq2d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ n = ( ( i + 1 ) - k ) ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
319 fvexd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) e. _V )
320 316 318 307 319 fvmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
321 320 feq1d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) : X --> CC <-> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC ) )
322 315 321 mpbird 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
323 322 ffvelcdmda 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
324 233 3expa 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( C ` k ) ` x ) e. CC )
325 323 324 mulcomd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
326 325 oveq2d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) = ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
327 201 peano2zd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ZZ )
328 173 a1i 
 |-  ( k e. ( 0 ... i ) -> 0 e. RR )
329 328 239 290 210 291 lelttrd 
 |-  ( k e. ( 0 ... i ) -> 0 < ( k + 1 ) )
330 328 290 329 ltled 
 |-  ( k e. ( 0 ... i ) -> 0 <_ ( k + 1 ) )
331 330 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( k + 1 ) )
332 212 289 syl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. RR )
333 293 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) <_ ( i + 1 ) )
334 332 297 214 333 302 letrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) <_ N )
335 207 209 327 331 334 elfzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ( 0 ... N ) )
336 335 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ( 0 ... N ) )
337 ovex 
 |-  ( k + 1 ) e. _V
338 eleq1 
 |-  ( j = ( k + 1 ) -> ( j e. ( 0 ... N ) <-> ( k + 1 ) e. ( 0 ... N ) ) )
339 338 anbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) ) )
340 fveq2 
 |-  ( j = ( k + 1 ) -> ( C ` j ) = ( C ` ( k + 1 ) ) )
341 340 feq1d 
 |-  ( j = ( k + 1 ) -> ( ( C ` j ) : X --> CC <-> ( C ` ( k + 1 ) ) : X --> CC ) )
342 339 341 imbi12d 
 |-  ( j = ( k + 1 ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC ) <-> ( ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) -> ( C ` ( k + 1 ) ) : X --> CC ) ) )
343 nfv 
 |-  F/ k ( ph /\ j e. ( 0 ... N ) )
344 nfmpt1 
 |-  F/_ k ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) )
345 10 344 nfcxfr 
 |-  F/_ k C
346 nfcv 
 |-  F/_ k j
347 345 346 nffv 
 |-  F/_ k ( C ` j )
348 nfcv 
 |-  F/_ k X
349 nfcv 
 |-  F/_ k CC
350 347 348 349 nff 
 |-  F/ k ( C ` j ) : X --> CC
351 343 350 nfim 
 |-  F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC )
352 fveq2 
 |-  ( k = j -> ( C ` k ) = ( C ` j ) )
353 352 feq1d 
 |-  ( k = j -> ( ( C ` k ) : X --> CC <-> ( C ` j ) : X --> CC ) )
354 267 353 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC ) ) )
355 351 354 229 chvarfv 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC )
356 337 342 355 vtocl 
 |-  ( ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) -> ( C ` ( k + 1 ) ) : X --> CC )
357 206 336 356 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` ( k + 1 ) ) : X --> CC )
358 357 ffvelcdmda 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( C ` ( k + 1 ) ) ` x ) e. CC )
359 281 3expa 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( D ` ( i - k ) ) ` x ) e. CC )
360 358 359 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
361 323 324 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) e. CC )
362 360 361 addcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) e. CC )
363 326 362 eqeltrrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
364 284 363 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) e. CC )
365 364 3impa 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) e. CC )
366 206 1 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> S e. { RR , CC } )
367 173 a1i 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> 0 e. RR )
368 206 2 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
369 366 368 204 dvmptconst 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( i _C k ) ) ) = ( x e. X |-> 0 ) )
370 282 3expa 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
371 206 224 227 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` k ) = ( ( S Dn F ) ` k ) )
372 371 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` k ) = ( C ` k ) )
373 230 feqmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` k ) = ( x e. X |-> ( ( C ` k ) ` x ) ) )
374 372 373 eqtr2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( x e. X |-> ( ( C ` k ) ` x ) ) = ( ( S Dn F ) ` k ) )
375 374 oveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( C ` k ) ` x ) ) ) = ( S _D ( ( S Dn F ) ` k ) ) )
376 366 84 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> S C_ CC )
377 206 123 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> F e. ( CC ^pm S ) )
378 elfznn0 
 |-  ( k e. ( 0 ... i ) -> k e. NN0 )
379 378 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> k e. NN0 )
380 dvnp1 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( S _D ( ( S Dn F ) ` k ) ) )
381 376 377 379 380 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( S _D ( ( S Dn F ) ` k ) ) )
382 381 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( ( S Dn F ) ` k ) ) = ( ( S Dn F ) ` ( k + 1 ) ) )
383 fveq2 
 |-  ( n = ( k + 1 ) -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` ( k + 1 ) ) )
384 fvexd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) e. _V )
385 114 383 336 384 fvmptd3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` ( k + 1 ) ) = ( ( S Dn F ) ` ( k + 1 ) ) )
386 385 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( C ` ( k + 1 ) ) )
387 357 feqmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` ( k + 1 ) ) = ( x e. X |-> ( ( C ` ( k + 1 ) ) ` x ) ) )
388 386 387 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( x e. X |-> ( ( C ` ( k + 1 ) ) ` x ) ) )
389 375 382 388 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( C ` k ) ` x ) ) ) = ( x e. X |-> ( ( C ` ( k + 1 ) ) ` x ) ) )
390 277 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) = ( D ` ( i - k ) ) )
391 279 feqmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( x e. X |-> ( ( D ` ( i - k ) ) ` x ) ) )
392 390 391 eqtr2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( x e. X |-> ( ( D ` ( i - k ) ) ` x ) ) = ( ( S Dn G ) ` ( i - k ) ) )
393 392 oveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( D ` ( i - k ) ) ` x ) ) ) = ( S _D ( ( S Dn G ) ` ( i - k ) ) ) )
394 206 152 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> G e. ( CC ^pm S ) )
395 fznn0sub 
 |-  ( k e. ( 0 ... i ) -> ( i - k ) e. NN0 )
396 395 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. NN0 )
397 dvnp1 
 |-  ( ( S C_ CC /\ G e. ( CC ^pm S ) /\ ( i - k ) e. NN0 ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( S _D ( ( S Dn G ) ` ( i - k ) ) ) )
398 376 394 396 397 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( S _D ( ( S Dn G ) ` ( i - k ) ) ) )
399 398 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( ( S Dn G ) ` ( i - k ) ) ) = ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) )
400 216 recnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. CC )
401 1cnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 1 e. CC )
402 212 recnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. CC )
403 400 401 402 addsubd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) = ( ( i - k ) + 1 ) )
404 403 eqcomd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i - k ) + 1 ) = ( ( i + 1 ) - k ) )
405 404 fveq2d 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
406 405 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
407 320 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - k ) ) )
408 322 feqmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) = ( x e. X |-> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
409 406 407 408 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( x e. X |-> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
410 393 399 409 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( D ` ( i - k ) ) ` x ) ) ) = ( x e. X |-> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
411 366 324 358 389 359 323 410 dvmptmul 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) = ( x e. X |-> ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) ) )
412 366 284 367 369 370 362 411 dvmptmul 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) = ( x e. X |-> ( ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) ) ) )
413 370 mul02d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = 0 )
414 326 oveq1d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) = ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) x. ( i _C k ) ) )
415 363 284 mulcomd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) x. ( i _C k ) ) = ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
416 414 415 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) = ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
417 413 416 oveq12d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) ) = ( 0 + ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
418 364 addlidd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( 0 + ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
419 417 418 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) ) = ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
420 419 mpteq2dva 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( x e. X |-> ( ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) ) ) = ( x e. X |-> ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
421 412 420 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) = ( x e. X |-> ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
422 194 195 196 197 198 283 365 421 dvmptfsum 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( S _D ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
423 204 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. CC )
424 360 an32s 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
425 anass 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) <-> ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( k e. ( 0 ... i ) /\ x e. X ) ) )
426 ancom 
 |-  ( ( k e. ( 0 ... i ) /\ x e. X ) <-> ( x e. X /\ k e. ( 0 ... i ) ) )
427 426 anbi2i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( k e. ( 0 ... i ) /\ x e. X ) ) <-> ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( x e. X /\ k e. ( 0 ... i ) ) ) )
428 anass 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) <-> ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( x e. X /\ k e. ( 0 ... i ) ) ) )
429 428 bicomi 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( x e. X /\ k e. ( 0 ... i ) ) ) <-> ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) )
430 427 429 bitri 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( k e. ( 0 ... i ) /\ x e. X ) ) <-> ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) )
431 425 430 bitri 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) <-> ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) )
432 431 imbi1i 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( C ` k ) ` x ) e. CC ) <-> ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( C ` k ) ` x ) e. CC ) )
433 324 432 mpbi 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( C ` k ) ` x ) e. CC )
434 431 imbi1i 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC ) <-> ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC ) )
435 323 434 mpbi 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
436 433 435 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) e. CC )
437 423 424 436 adddid 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
438 437 sumeq2dv 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... i ) ( ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
439 198 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 0 ... i ) e. Fin )
440 423 424 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) e. CC )
441 423 436 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
442 439 440 441 fsumadd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
443 oveq2 
 |-  ( k = h -> ( i _C k ) = ( i _C h ) )
444 fvoveq1 
 |-  ( k = h -> ( C ` ( k + 1 ) ) = ( C ` ( h + 1 ) ) )
445 444 fveq1d 
 |-  ( k = h -> ( ( C ` ( k + 1 ) ) ` x ) = ( ( C ` ( h + 1 ) ) ` x ) )
446 oveq2 
 |-  ( k = h -> ( i - k ) = ( i - h ) )
447 446 fveq2d 
 |-  ( k = h -> ( D ` ( i - k ) ) = ( D ` ( i - h ) ) )
448 447 fveq1d 
 |-  ( k = h -> ( ( D ` ( i - k ) ) ` x ) = ( ( D ` ( i - h ) ) ` x ) )
449 445 448 oveq12d 
 |-  ( k = h -> ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) = ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) )
450 443 449 oveq12d 
 |-  ( k = h -> ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) )
451 nfcv 
 |-  F/_ h ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) )
452 nfcv 
 |-  F/_ k ( i _C h )
453 nfcv 
 |-  F/_ k x.
454 nfcv 
 |-  F/_ k ( h + 1 )
455 345 454 nffv 
 |-  F/_ k ( C ` ( h + 1 ) )
456 nfcv 
 |-  F/_ k x
457 455 456 nffv 
 |-  F/_ k ( ( C ` ( h + 1 ) ) ` x )
458 nfmpt1 
 |-  F/_ k ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) )
459 11 458 nfcxfr 
 |-  F/_ k D
460 nfcv 
 |-  F/_ k ( i - h )
461 459 460 nffv 
 |-  F/_ k ( D ` ( i - h ) )
462 461 456 nffv 
 |-  F/_ k ( ( D ` ( i - h ) ) ` x )
463 457 453 462 nfov 
 |-  F/_ k ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) )
464 452 453 463 nfov 
 |-  F/_ k ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) )
465 450 451 464 cbvsum 
 |-  sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = sum_ h e. ( 0 ... i ) ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) )
466 465 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = sum_ h e. ( 0 ... i ) ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) )
467 1zzd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 1 e. ZZ )
468 96 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 0 e. ZZ )
469 234 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> i e. ZZ )
470 nfv 
 |-  F/ k ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X )
471 nfcv 
 |-  F/_ k h
472 nfcv 
 |-  F/_ k ( 0 ... i )
473 471 472 nfel 
 |-  F/ k h e. ( 0 ... i )
474 470 473 nfan 
 |-  F/ k ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) )
475 464 349 nfel 
 |-  F/ k ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC
476 474 475 nfim 
 |-  F/ k ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) ) -> ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC )
477 eleq1 
 |-  ( k = h -> ( k e. ( 0 ... i ) <-> h e. ( 0 ... i ) ) )
478 477 anbi2d 
 |-  ( k = h -> ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) <-> ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) ) ) )
479 450 eleq1d 
 |-  ( k = h -> ( ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) e. CC <-> ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC ) )
480 478 479 imbi12d 
 |-  ( k = h -> ( ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) e. CC ) <-> ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) ) -> ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC ) ) )
481 476 480 440 chvarfv 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) ) -> ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC )
482 oveq2 
 |-  ( h = ( j - 1 ) -> ( i _C h ) = ( i _C ( j - 1 ) ) )
483 fvoveq1 
 |-  ( h = ( j - 1 ) -> ( C ` ( h + 1 ) ) = ( C ` ( ( j - 1 ) + 1 ) ) )
484 483 fveq1d 
 |-  ( h = ( j - 1 ) -> ( ( C ` ( h + 1 ) ) ` x ) = ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) )
485 oveq2 
 |-  ( h = ( j - 1 ) -> ( i - h ) = ( i - ( j - 1 ) ) )
486 485 fveq2d 
 |-  ( h = ( j - 1 ) -> ( D ` ( i - h ) ) = ( D ` ( i - ( j - 1 ) ) ) )
487 486 fveq1d 
 |-  ( h = ( j - 1 ) -> ( ( D ` ( i - h ) ) ` x ) = ( ( D ` ( i - ( j - 1 ) ) ) ` x ) )
488 484 487 oveq12d 
 |-  ( h = ( j - 1 ) -> ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) = ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) )
489 482 488 oveq12d 
 |-  ( h = ( j - 1 ) -> ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) = ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) )
490 467 468 469 481 489 fsumshft 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ h e. ( 0 ... i ) ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) = sum_ j e. ( ( 0 + 1 ) ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) )
491 466 490 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = sum_ j e. ( ( 0 + 1 ) ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) )
492 0p1e1 
 |-  ( 0 + 1 ) = 1
493 492 oveq1i 
 |-  ( ( 0 + 1 ) ... ( i + 1 ) ) = ( 1 ... ( i + 1 ) )
494 493 sumeq1i 
 |-  sum_ j e. ( ( 0 + 1 ) ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) )
495 494 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( ( 0 + 1 ) ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) )
496 elfzelz 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> j e. ZZ )
497 496 zcnd 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> j e. CC )
498 1cnd 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 1 e. CC )
499 497 498 npcand 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> ( ( j - 1 ) + 1 ) = j )
500 499 fveq2d 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> ( C ` ( ( j - 1 ) + 1 ) ) = ( C ` j ) )
501 500 fveq1d 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) = ( ( C ` j ) ` x ) )
502 501 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) = ( ( C ` j ) ` x ) )
503 215 recnd 
 |-  ( i e. ( 0 ..^ N ) -> i e. CC )
504 503 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. CC )
505 497 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. CC )
506 498 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. CC )
507 504 505 506 subsub3d 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i - ( j - 1 ) ) = ( ( i + 1 ) - j ) )
508 507 fveq2d 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( i - ( j - 1 ) ) ) = ( D ` ( ( i + 1 ) - j ) ) )
509 508 fveq1d 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( D ` ( i - ( j - 1 ) ) ) ` x ) = ( ( D ` ( ( i + 1 ) - j ) ) ` x ) )
510 502 509 oveq12d 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) = ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) )
511 510 oveq2d 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) )
512 511 sumeq2dv 
 |-  ( i e. ( 0 ..^ N ) -> sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) )
513 512 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) )
514 nfv 
 |-  F/ j ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X )
515 nfcv 
 |-  F/_ j ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
516 fzfid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... ( i + 1 ) ) e. Fin )
517 187 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. NN0 )
518 496 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ZZ )
519 1zzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. ZZ )
520 518 519 zsubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( j - 1 ) e. ZZ )
521 517 520 bccld 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. NN0 )
522 521 nn0cnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
523 522 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
524 523 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
525 12 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ph )
526 0zd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 e. ZZ )
527 208 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> N e. ZZ )
528 173 a1i 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 0 e. RR )
529 496 zred 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> j e. RR )
530 1red 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 1 e. RR )
531 0lt1 
 |-  0 < 1
532 531 a1i 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 0 < 1 )
533 elfzle1 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 1 <_ j )
534 528 530 529 532 533 ltletrd 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 0 < j )
535 528 529 534 ltled 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 0 <_ j )
536 535 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 <_ j )
537 529 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. RR )
538 215 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. RR )
539 1red 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. RR )
540 538 539 readdcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) e. RR )
541 213 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> N e. RR )
542 elfzle2 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> j <_ ( i + 1 ) )
543 542 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j <_ ( i + 1 ) )
544 301 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) <_ N )
545 537 540 541 543 544 letrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j <_ N )
546 526 527 518 536 545 elfzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ( 0 ... N ) )
547 546 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ( 0 ... N ) )
548 525 547 355 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( C ` j ) : X --> CC )
549 548 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( C ` j ) : X --> CC )
550 simplr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> x e. X )
551 549 550 ffvelcdmd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( C ` j ) ` x ) e. CC )
552 234 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. ZZ )
553 552 peano2zd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) e. ZZ )
554 553 518 zsubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ZZ )
555 540 537 subge0d 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( 0 <_ ( ( i + 1 ) - j ) <-> j <_ ( i + 1 ) ) )
556 543 555 mpbird 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 <_ ( ( i + 1 ) - j ) )
557 540 537 resubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. RR )
558 557 leidd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) <_ ( ( i + 1 ) - j ) )
559 529 534 elrpd 
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> j e. RR+ )
560 559 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. RR+ )
561 540 560 ltsubrpd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < ( i + 1 ) )
562 557 540 541 561 544 ltletrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < N )
563 557 557 541 558 562 lelttrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < N )
564 557 541 563 ltled 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) <_ N )
565 526 527 554 556 564 elfzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ( 0 ... N ) )
566 565 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ( 0 ... N ) )
567 nfv 
 |-  F/ k ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) )
568 nfcv 
 |-  F/_ k ( ( i + 1 ) - j )
569 459 568 nffv 
 |-  F/_ k ( D ` ( ( i + 1 ) - j ) )
570 569 348 349 nff 
 |-  F/ k ( D ` ( ( i + 1 ) - j ) ) : X --> CC
571 567 570 nfim 
 |-  F/ k ( ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
572 ovex 
 |-  ( ( i + 1 ) - j ) e. _V
573 eleq1 
 |-  ( k = ( ( i + 1 ) - j ) -> ( k e. ( 0 ... N ) <-> ( ( i + 1 ) - j ) e. ( 0 ... N ) ) )
574 573 anbi2d 
 |-  ( k = ( ( i + 1 ) - j ) -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) ) )
575 fveq2 
 |-  ( k = ( ( i + 1 ) - j ) -> ( D ` k ) = ( D ` ( ( i + 1 ) - j ) ) )
576 575 feq1d 
 |-  ( k = ( ( i + 1 ) - j ) -> ( ( D ` k ) : X --> CC <-> ( D ` ( ( i + 1 ) - j ) ) : X --> CC ) )
577 574 576 imbi12d 
 |-  ( k = ( ( i + 1 ) - j ) -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC ) ) )
578 11 a1i 
 |-  ( ph -> D = ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) ) )
579 fvexd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) e. _V )
580 578 579 fvmpt2d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) = ( ( S Dn G ) ` k ) )
581 580 feq1d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( D ` k ) : X --> CC <-> ( ( S Dn G ) ` k ) : X --> CC ) )
582 9 581 mpbird 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC )
583 571 572 577 582 vtoclf 
 |-  ( ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
584 525 566 583 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
585 584 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
586 585 550 ffvelcdmd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) e. CC )
587 551 586 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) e. CC )
588 524 587 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) e. CC )
589 1zzd 
 |-  ( i e. ( 0 ..^ N ) -> 1 e. ZZ )
590 234 peano2zd 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ZZ )
591 492 eqcomi 
 |-  1 = ( 0 + 1 )
592 591 a1i 
 |-  ( i e. ( 0 ..^ N ) -> 1 = ( 0 + 1 ) )
593 173 a1i 
 |-  ( i e. ( 0 ..^ N ) -> 0 e. RR )
594 1red 
 |-  ( i e. ( 0 ..^ N ) -> 1 e. RR )
595 187 nn0ge0d 
 |-  ( i e. ( 0 ..^ N ) -> 0 <_ i )
596 593 215 594 595 leadd1dd 
 |-  ( i e. ( 0 ..^ N ) -> ( 0 + 1 ) <_ ( i + 1 ) )
597 592 596 eqbrtrd 
 |-  ( i e. ( 0 ..^ N ) -> 1 <_ ( i + 1 ) )
598 589 590 597 3jca 
 |-  ( i e. ( 0 ..^ N ) -> ( 1 e. ZZ /\ ( i + 1 ) e. ZZ /\ 1 <_ ( i + 1 ) ) )
599 eluz2 
 |-  ( ( i + 1 ) e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ ( i + 1 ) e. ZZ /\ 1 <_ ( i + 1 ) ) )
600 598 599 sylibr 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( ZZ>= ` 1 ) )
601 eluzfz2 
 |-  ( ( i + 1 ) e. ( ZZ>= ` 1 ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
602 600 601 syl 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
603 602 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
604 oveq1 
 |-  ( j = ( i + 1 ) -> ( j - 1 ) = ( ( i + 1 ) - 1 ) )
605 604 oveq2d 
 |-  ( j = ( i + 1 ) -> ( i _C ( j - 1 ) ) = ( i _C ( ( i + 1 ) - 1 ) ) )
606 fveq2 
 |-  ( j = ( i + 1 ) -> ( C ` j ) = ( C ` ( i + 1 ) ) )
607 606 fveq1d 
 |-  ( j = ( i + 1 ) -> ( ( C ` j ) ` x ) = ( ( C ` ( i + 1 ) ) ` x ) )
608 oveq2 
 |-  ( j = ( i + 1 ) -> ( ( i + 1 ) - j ) = ( ( i + 1 ) - ( i + 1 ) ) )
609 608 fveq2d 
 |-  ( j = ( i + 1 ) -> ( D ` ( ( i + 1 ) - j ) ) = ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) )
610 609 fveq1d 
 |-  ( j = ( i + 1 ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) = ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
611 607 610 oveq12d 
 |-  ( j = ( i + 1 ) -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
612 605 611 oveq12d 
 |-  ( j = ( i + 1 ) -> ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) )
613 514 515 516 588 603 612 fsumsplit1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = ( ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) + sum_ j e. ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) )
614 1cnd 
 |-  ( i e. ( 0 ..^ N ) -> 1 e. CC )
615 503 614 pncand 
 |-  ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - 1 ) = i )
616 615 oveq2d 
 |-  ( i e. ( 0 ..^ N ) -> ( i _C ( ( i + 1 ) - 1 ) ) = ( i _C i ) )
617 bcnn 
 |-  ( i e. NN0 -> ( i _C i ) = 1 )
618 187 617 syl 
 |-  ( i e. ( 0 ..^ N ) -> ( i _C i ) = 1 )
619 616 618 eqtrd 
 |-  ( i e. ( 0 ..^ N ) -> ( i _C ( ( i + 1 ) - 1 ) ) = 1 )
620 503 614 addcld 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. CC )
621 620 subidd 
 |-  ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - ( i + 1 ) ) = 0 )
622 621 fveq2d 
 |-  ( i e. ( 0 ..^ N ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) = ( D ` 0 ) )
623 622 fveq1d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) = ( ( D ` 0 ) ` x ) )
624 623 oveq2d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) )
625 619 624 oveq12d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) ) )
626 625 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) ) )
627 simpl 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ph )
628 fzofzp1 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ... N ) )
629 628 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ... N ) )
630 nfv 
 |-  F/ k ( ph /\ ( i + 1 ) e. ( 0 ... N ) )
631 nfcv 
 |-  F/_ k ( i + 1 )
632 345 631 nffv 
 |-  F/_ k ( C ` ( i + 1 ) )
633 632 348 349 nff 
 |-  F/ k ( C ` ( i + 1 ) ) : X --> CC
634 630 633 nfim 
 |-  F/ k ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
635 ovex 
 |-  ( i + 1 ) e. _V
636 eleq1 
 |-  ( k = ( i + 1 ) -> ( k e. ( 0 ... N ) <-> ( i + 1 ) e. ( 0 ... N ) ) )
637 636 anbi2d 
 |-  ( k = ( i + 1 ) -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) ) )
638 fveq2 
 |-  ( k = ( i + 1 ) -> ( C ` k ) = ( C ` ( i + 1 ) ) )
639 638 feq1d 
 |-  ( k = ( i + 1 ) -> ( ( C ` k ) : X --> CC <-> ( C ` ( i + 1 ) ) : X --> CC ) )
640 637 639 imbi12d 
 |-  ( k = ( i + 1 ) -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC ) ) )
641 634 635 640 229 vtoclf 
 |-  ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
642 627 629 641 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
643 642 ffvelcdmda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( C ` ( i + 1 ) ) ` x ) e. CC )
644 nfv 
 |-  F/ k ( ph /\ 0 e. ( 0 ... N ) )
645 nfcv 
 |-  F/_ k 0
646 459 645 nffv 
 |-  F/_ k ( D ` 0 )
647 646 348 349 nff 
 |-  F/ k ( D ` 0 ) : X --> CC
648 644 647 nfim 
 |-  F/ k ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC )
649 c0ex 
 |-  0 e. _V
650 eleq1 
 |-  ( k = 0 -> ( k e. ( 0 ... N ) <-> 0 e. ( 0 ... N ) ) )
651 650 anbi2d 
 |-  ( k = 0 -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ 0 e. ( 0 ... N ) ) ) )
652 fveq2 
 |-  ( k = 0 -> ( D ` k ) = ( D ` 0 ) )
653 652 feq1d 
 |-  ( k = 0 -> ( ( D ` k ) : X --> CC <-> ( D ` 0 ) : X --> CC ) )
654 651 653 imbi12d 
 |-  ( k = 0 -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC ) ) )
655 648 649 654 582 vtoclf 
 |-  ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC )
656 12 117 655 syl2anc 
 |-  ( ph -> ( D ` 0 ) : X --> CC )
657 656 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` 0 ) : X --> CC )
658 657 ffvelcdmda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` 0 ) ` x ) e. CC )
659 643 658 mulcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) e. CC )
660 659 mullidd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) )
661 626 660 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) )
662 1m1e0 
 |-  ( 1 - 1 ) = 0
663 662 fveq2i 
 |-  ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
664 13 eqcomi 
 |-  ( ZZ>= ` 0 ) = NN0
665 663 664 eqtr2i 
 |-  NN0 = ( ZZ>= ` ( 1 - 1 ) )
666 665 a1i 
 |-  ( i e. ( 0 ..^ N ) -> NN0 = ( ZZ>= ` ( 1 - 1 ) ) )
667 187 666 eleqtrd 
 |-  ( i e. ( 0 ..^ N ) -> i e. ( ZZ>= ` ( 1 - 1 ) ) )
668 fzdifsuc2 
 |-  ( i e. ( ZZ>= ` ( 1 - 1 ) ) -> ( 1 ... i ) = ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
669 667 668 syl 
 |-  ( i e. ( 0 ..^ N ) -> ( 1 ... i ) = ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
670 669 eqcomd 
 |-  ( i e. ( 0 ..^ N ) -> ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) = ( 1 ... i ) )
671 670 sumeq1d 
 |-  ( i e. ( 0 ..^ N ) -> sum_ j e. ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) )
672 671 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) )
673 661 672 oveq12d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) + sum_ j e. ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) = ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) )
674 513 613 673 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) )
675 491 495 674 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) )
676 nfcv 
 |-  F/_ k ( i _C 0 )
677 345 645 nffv 
 |-  F/_ k ( C ` 0 )
678 677 456 nffv 
 |-  F/_ k ( ( C ` 0 ) ` x )
679 nfcv 
 |-  F/_ k ( ( i + 1 ) - 0 )
680 459 679 nffv 
 |-  F/_ k ( D ` ( ( i + 1 ) - 0 ) )
681 680 456 nffv 
 |-  F/_ k ( ( D ` ( ( i + 1 ) - 0 ) ) ` x )
682 678 453 681 nfov 
 |-  F/_ k ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) )
683 676 453 682 nfov 
 |-  F/_ k ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
684 664 a1i 
 |-  ( i e. ( 0 ..^ N ) -> ( ZZ>= ` 0 ) = NN0 )
685 187 684 eleqtrrd 
 |-  ( i e. ( 0 ..^ N ) -> i e. ( ZZ>= ` 0 ) )
686 eluzfz1 
 |-  ( i e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... i ) )
687 685 686 syl 
 |-  ( i e. ( 0 ..^ N ) -> 0 e. ( 0 ... i ) )
688 687 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 0 e. ( 0 ... i ) )
689 oveq2 
 |-  ( k = 0 -> ( i _C k ) = ( i _C 0 ) )
690 110 fveq1d 
 |-  ( k = 0 -> ( ( C ` k ) ` x ) = ( ( C ` 0 ) ` x ) )
691 oveq2 
 |-  ( k = 0 -> ( ( i + 1 ) - k ) = ( ( i + 1 ) - 0 ) )
692 691 fveq2d 
 |-  ( k = 0 -> ( D ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - 0 ) ) )
693 692 fveq1d 
 |-  ( k = 0 -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) )
694 690 693 oveq12d 
 |-  ( k = 0 -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
695 689 694 oveq12d 
 |-  ( k = 0 -> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) )
696 470 683 439 441 688 695 fsumsplit1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
697 620 subid1d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - 0 ) = ( i + 1 ) )
698 697 fveq2d 
 |-  ( i e. ( 0 ..^ N ) -> ( D ` ( ( i + 1 ) - 0 ) ) = ( D ` ( i + 1 ) ) )
699 698 fveq1d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) = ( ( D ` ( i + 1 ) ) ` x ) )
700 699 oveq2d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) )
701 700 oveq2d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) = ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) )
702 701 oveq1d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
703 702 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
704 bcn0 
 |-  ( i e. NN0 -> ( i _C 0 ) = 1 )
705 187 704 syl 
 |-  ( i e. ( 0 ..^ N ) -> ( i _C 0 ) = 1 )
706 705 oveq1d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) )
707 706 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) )
708 677 348 349 nff 
 |-  F/ k ( C ` 0 ) : X --> CC
709 644 708 nfim 
 |-  F/ k ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC )
710 110 feq1d 
 |-  ( k = 0 -> ( ( C ` k ) : X --> CC <-> ( C ` 0 ) : X --> CC ) )
711 651 710 imbi12d 
 |-  ( k = 0 -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC ) ) )
712 709 649 711 229 vtoclf 
 |-  ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC )
713 12 117 712 syl2anc 
 |-  ( ph -> ( C ` 0 ) : X --> CC )
714 713 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( C ` 0 ) : X --> CC )
715 714 ffvelcdmda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( C ` 0 ) ` x ) e. CC )
716 459 631 nffv 
 |-  F/_ k ( D ` ( i + 1 ) )
717 716 348 349 nff 
 |-  F/ k ( D ` ( i + 1 ) ) : X --> CC
718 630 717 nfim 
 |-  F/ k ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
719 fveq2 
 |-  ( k = ( i + 1 ) -> ( D ` k ) = ( D ` ( i + 1 ) ) )
720 719 feq1d 
 |-  ( k = ( i + 1 ) -> ( ( D ` k ) : X --> CC <-> ( D ` ( i + 1 ) ) : X --> CC ) )
721 637 720 imbi12d 
 |-  ( k = ( i + 1 ) -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC ) ) )
722 718 635 721 582 vtoclf 
 |-  ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
723 627 629 722 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
724 723 ffvelcdmda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` ( i + 1 ) ) ` x ) e. CC )
725 715 724 mulcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) e. CC )
726 725 mullidd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) )
727 707 726 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) )
728 nfv 
 |-  F/ j i e. ( 0 ..^ N )
729 1zzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> 1 e. ZZ )
730 234 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> i e. ZZ )
731 eldifi 
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ( 0 ... i ) )
732 elfzelz 
 |-  ( j e. ( 0 ... i ) -> j e. ZZ )
733 731 732 syl 
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ZZ )
734 733 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j e. ZZ )
735 elfznn0 
 |-  ( j e. ( 0 ... i ) -> j e. NN0 )
736 731 735 syl 
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. NN0 )
737 eldifsni 
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j =/= 0 )
738 736 737 jca 
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> ( j e. NN0 /\ j =/= 0 ) )
739 elnnne0 
 |-  ( j e. NN <-> ( j e. NN0 /\ j =/= 0 ) )
740 738 739 sylibr 
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. NN )
741 nnge1 
 |-  ( j e. NN -> 1 <_ j )
742 740 741 syl 
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> 1 <_ j )
743 742 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> 1 <_ j )
744 elfzle2 
 |-  ( j e. ( 0 ... i ) -> j <_ i )
745 731 744 syl 
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j <_ i )
746 745 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j <_ i )
747 729 730 734 743 746 elfzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j e. ( 1 ... i ) )
748 747 ex 
 |-  ( i e. ( 0 ..^ N ) -> ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ( 1 ... i ) ) )
749 0zd 
 |-  ( j e. ( 1 ... i ) -> 0 e. ZZ )
750 elfzel2 
 |-  ( j e. ( 1 ... i ) -> i e. ZZ )
751 elfzelz 
 |-  ( j e. ( 1 ... i ) -> j e. ZZ )
752 173 a1i 
 |-  ( j e. ( 1 ... i ) -> 0 e. RR )
753 751 zred 
 |-  ( j e. ( 1 ... i ) -> j e. RR )
754 1red 
 |-  ( j e. ( 1 ... i ) -> 1 e. RR )
755 531 a1i 
 |-  ( j e. ( 1 ... i ) -> 0 < 1 )
756 elfzle1 
 |-  ( j e. ( 1 ... i ) -> 1 <_ j )
757 752 754 753 755 756 ltletrd 
 |-  ( j e. ( 1 ... i ) -> 0 < j )
758 752 753 757 ltled 
 |-  ( j e. ( 1 ... i ) -> 0 <_ j )
759 elfzle2 
 |-  ( j e. ( 1 ... i ) -> j <_ i )
760 749 750 751 758 759 elfzd 
 |-  ( j e. ( 1 ... i ) -> j e. ( 0 ... i ) )
761 752 757 gtned 
 |-  ( j e. ( 1 ... i ) -> j =/= 0 )
762 nelsn 
 |-  ( j =/= 0 -> -. j e. { 0 } )
763 761 762 syl 
 |-  ( j e. ( 1 ... i ) -> -. j e. { 0 } )
764 760 763 eldifd 
 |-  ( j e. ( 1 ... i ) -> j e. ( ( 0 ... i ) \ { 0 } ) )
765 764 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> j e. ( ( 0 ... i ) \ { 0 } ) )
766 765 ex 
 |-  ( i e. ( 0 ..^ N ) -> ( j e. ( 1 ... i ) -> j e. ( ( 0 ... i ) \ { 0 } ) ) )
767 748 766 impbid 
 |-  ( i e. ( 0 ..^ N ) -> ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
768 728 767 alrimi 
 |-  ( i e. ( 0 ..^ N ) -> A. j ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
769 dfcleq 
 |-  ( ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) <-> A. j ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
770 768 769 sylibr 
 |-  ( i e. ( 0 ..^ N ) -> ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) )
771 770 sumeq1d 
 |-  ( i e. ( 0 ..^ N ) -> sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
772 771 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
773 727 772 oveq12d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
774 696 703 773 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
775 675 774 oveq12d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) + ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
776 fzfid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... i ) e. Fin )
777 187 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> i e. NN0 )
778 765 733 syl 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> j e. ZZ )
779 1zzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> 1 e. ZZ )
780 778 779 zsubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( j - 1 ) e. ZZ )
781 777 780 bccld 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. NN0 )
782 781 nn0cnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
783 782 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
784 783 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
785 simpl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) )
786 fzelp1 
 |-  ( j e. ( 1 ... i ) -> j e. ( 1 ... ( i + 1 ) ) )
787 786 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> j e. ( 1 ... ( i + 1 ) ) )
788 785 787 551 syl2anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( C ` j ) ` x ) e. CC )
789 787 586 syldan 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) e. CC )
790 788 789 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) e. CC )
791 784 790 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) e. CC )
792 776 791 fsumcl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) e. CC )
793 187 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> i e. NN0 )
794 elfzelz 
 |-  ( k e. ( 1 ... i ) -> k e. ZZ )
795 794 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> k e. ZZ )
796 793 795 bccld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. NN0 )
797 796 nn0cnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
798 797 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
799 798 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
800 simpll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ph /\ i e. ( 0 ..^ N ) ) )
801 simplr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> x e. X )
802 760 ssriv 
 |-  ( 1 ... i ) C_ ( 0 ... i )
803 id 
 |-  ( k e. ( 1 ... i ) -> k e. ( 1 ... i ) )
804 802 803 sselid 
 |-  ( k e. ( 1 ... i ) -> k e. ( 0 ... i ) )
805 804 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> k e. ( 0 ... i ) )
806 800 801 805 433 syl21anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( C ` k ) ` x ) e. CC )
807 805 435 syldan 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
808 806 807 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) e. CC )
809 799 808 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
810 776 809 fsumcl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
811 659 792 725 810 add4d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) + ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + ( sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
812 oveq1 
 |-  ( j = k -> ( j - 1 ) = ( k - 1 ) )
813 812 oveq2d 
 |-  ( j = k -> ( i _C ( j - 1 ) ) = ( i _C ( k - 1 ) ) )
814 fveq2 
 |-  ( j = k -> ( C ` j ) = ( C ` k ) )
815 814 fveq1d 
 |-  ( j = k -> ( ( C ` j ) ` x ) = ( ( C ` k ) ` x ) )
816 oveq2 
 |-  ( j = k -> ( ( i + 1 ) - j ) = ( ( i + 1 ) - k ) )
817 816 fveq2d 
 |-  ( j = k -> ( D ` ( ( i + 1 ) - j ) ) = ( D ` ( ( i + 1 ) - k ) ) )
818 817 fveq1d 
 |-  ( j = k -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) = ( ( D ` ( ( i + 1 ) - k ) ) ` x ) )
819 815 818 oveq12d 
 |-  ( j = k -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
820 813 819 oveq12d 
 |-  ( j = k -> ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
821 nfcv 
 |-  F/_ k ( i _C ( j - 1 ) )
822 347 456 nffv 
 |-  F/_ k ( ( C ` j ) ` x )
823 569 456 nffv 
 |-  F/_ k ( ( D ` ( ( i + 1 ) - j ) ) ` x )
824 822 453 823 nfov 
 |-  F/_ k ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) )
825 821 453 824 nfov 
 |-  F/_ k ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) )
826 nfcv 
 |-  F/_ j ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
827 820 825 826 cbvsum 
 |-  sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = sum_ k e. ( 1 ... i ) ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
828 827 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = sum_ k e. ( 1 ... i ) ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
829 828 oveq1d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( sum_ k e. ( 1 ... i ) ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
830 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
831 795 830 syl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( k - 1 ) e. ZZ )
832 793 831 bccld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. NN0 )
833 832 nn0cnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
834 833 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
835 834 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
836 835 808 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
837 776 836 809 fsumadd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 1 ... i ) ( ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( sum_ k e. ( 1 ... i ) ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
838 837 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( sum_ k e. ( 1 ... i ) ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 1 ... i ) ( ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
839 833 797 addcomd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i _C ( k - 1 ) ) + ( i _C k ) ) = ( ( i _C k ) + ( i _C ( k - 1 ) ) ) )
840 bcpasc 
 |-  ( ( i e. NN0 /\ k e. ZZ ) -> ( ( i _C k ) + ( i _C ( k - 1 ) ) ) = ( ( i + 1 ) _C k ) )
841 793 795 840 syl2anc 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i _C k ) + ( i _C ( k - 1 ) ) ) = ( ( i + 1 ) _C k ) )
842 839 841 eqtr2d 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) = ( ( i _C ( k - 1 ) ) + ( i _C k ) ) )
843 842 oveq1d 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i _C ( k - 1 ) ) + ( i _C k ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
844 843 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i _C ( k - 1 ) ) + ( i _C k ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
845 844 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i _C ( k - 1 ) ) + ( i _C k ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
846 835 799 808 adddird 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( i _C ( k - 1 ) ) + ( i _C k ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
847 845 846 eqtr2d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
848 847 sumeq2dv 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 1 ... i ) ( ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
849 829 838 848 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
850 849 oveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + ( sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
851 peano2nn0 
 |-  ( i e. NN0 -> ( i + 1 ) e. NN0 )
852 793 851 syl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i + 1 ) e. NN0 )
853 852 795 bccld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
854 853 nn0cnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
855 854 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
856 855 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
857 856 808 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
858 776 857 fsumcl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
859 659 725 858 addassd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
860 187 851 syl 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. NN0 )
861 bcn0 
 |-  ( ( i + 1 ) e. NN0 -> ( ( i + 1 ) _C 0 ) = 1 )
862 860 861 syl 
 |-  ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) _C 0 ) = 1 )
863 862 700 oveq12d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) )
864 863 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) )
865 864 726 eqtr2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) = ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) )
866 770 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) )
867 866 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... i ) = ( ( 0 ... i ) \ { 0 } ) )
868 867 sumeq1d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
869 865 868 oveq12d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
870 nfcv 
 |-  F/_ k ( ( i + 1 ) _C 0 )
871 870 453 682 nfov 
 |-  F/_ k ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
872 199 851 syl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. NN0 )
873 872 201 bccld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
874 873 nn0cnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
875 874 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
876 875 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
877 876 436 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
878 oveq2 
 |-  ( k = 0 -> ( ( i + 1 ) _C k ) = ( ( i + 1 ) _C 0 ) )
879 878 694 oveq12d 
 |-  ( k = 0 -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) )
880 470 871 439 877 688 879 fsumsplit1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
881 880 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
882 869 881 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
883 882 oveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
884 bcnn 
 |-  ( ( i + 1 ) e. NN0 -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
885 860 884 syl 
 |-  ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
886 885 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
887 886 oveq1d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) )
888 622 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) = ( D ` 0 ) )
889 888 feq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC <-> ( D ` 0 ) : X --> CC ) )
890 657 889 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC )
891 890 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC )
892 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> x e. X )
893 891 892 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) e. CC )
894 643 893 mulcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) e. CC )
895 894 mullidd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
896 624 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) )
897 887 895 896 3eqtrrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) = ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) )
898 fzdifsuc 
 |-  ( i e. ( ZZ>= ` 0 ) -> ( 0 ... i ) = ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
899 685 898 syl 
 |-  ( i e. ( 0 ..^ N ) -> ( 0 ... i ) = ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
900 899 sumeq1d 
 |-  ( i e. ( 0 ..^ N ) -> sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = sum_ k e. ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
901 900 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = sum_ k e. ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
902 897 901 oveq12d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
903 nfcv 
 |-  F/_ k ( ( i + 1 ) _C ( i + 1 ) )
904 632 456 nffv 
 |-  F/_ k ( ( C ` ( i + 1 ) ) ` x )
905 nfcv 
 |-  F/_ k ( ( i + 1 ) - ( i + 1 ) )
906 459 905 nffv 
 |-  F/_ k ( D ` ( ( i + 1 ) - ( i + 1 ) ) )
907 906 456 nffv 
 |-  F/_ k ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x )
908 904 453 907 nfov 
 |-  F/_ k ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
909 903 453 908 nfov 
 |-  F/_ k ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
910 fzfid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 0 ... ( i + 1 ) ) e. Fin )
911 860 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. NN0 )
912 elfzelz 
 |-  ( k e. ( 0 ... ( i + 1 ) ) -> k e. ZZ )
913 912 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ZZ )
914 911 913 bccld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
915 914 nn0cnd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
916 915 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
917 916 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
918 627 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ph )
919 96 a1i 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 e. ZZ )
920 208 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> N e. ZZ )
921 elfzle1 
 |-  ( k e. ( 0 ... ( i + 1 ) ) -> 0 <_ k )
922 921 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 <_ k )
923 913 zred 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. RR )
924 911 nn0red 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. RR )
925 213 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> N e. RR )
926 elfzle2 
 |-  ( k e. ( 0 ... ( i + 1 ) ) -> k <_ ( i + 1 ) )
927 926 adantl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k <_ ( i + 1 ) )
928 301 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) <_ N )
929 923 924 925 927 928 letrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k <_ N )
930 919 920 913 922 929 elfzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ( 0 ... N ) )
931 930 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ( 0 ... N ) )
932 918 931 229 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( C ` k ) : X --> CC )
933 932 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( C ` k ) : X --> CC )
934 simplr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> x e. X )
935 933 934 ffvelcdmd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( C ` k ) ` x ) e. CC )
936 918 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ph )
937 590 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. ZZ )
938 937 913 zsubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ZZ )
939 924 923 subge0d 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( 0 <_ ( ( i + 1 ) - k ) <-> k <_ ( i + 1 ) ) )
940 927 939 mpbird 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 <_ ( ( i + 1 ) - k ) )
941 924 923 resubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. RR )
942 925 923 resubcld 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - k ) e. RR )
943 925 173 247 sylancl 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - 0 ) e. RR )
944 924 925 923 928 lesub1dd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ ( N - k ) )
945 173 a1i 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 e. RR )
946 945 923 925 922 lesub2dd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - k ) <_ ( N - 0 ) )
947 941 942 943 944 946 letrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ ( N - 0 ) )
948 253 adantr 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - 0 ) = N )
949 947 948 breqtrd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ N )
950 919 920 938 940 949 elfzd 
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
951 950 adantll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
952 951 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
953 fveq2 
 |-  ( j = ( ( i + 1 ) - k ) -> ( D ` j ) = ( D ` ( ( i + 1 ) - k ) ) )
954 953 feq1d 
 |-  ( j = ( ( i + 1 ) - k ) -> ( ( D ` j ) : X --> CC <-> ( D ` ( ( i + 1 ) - k ) ) : X --> CC ) )
955 310 954 imbi12d 
 |-  ( j = ( ( i + 1 ) - k ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC ) <-> ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC ) ) )
956 459 346 nffv 
 |-  F/_ k ( D ` j )
957 956 348 349 nff 
 |-  F/ k ( D ` j ) : X --> CC
958 343 957 nfim 
 |-  F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC )
959 fveq2 
 |-  ( k = j -> ( D ` k ) = ( D ` j ) )
960 959 feq1d 
 |-  ( k = j -> ( ( D ` k ) : X --> CC <-> ( D ` j ) : X --> CC ) )
961 267 960 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC ) ) )
962 958 961 582 chvarfv 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC )
963 308 955 962 vtocl 
 |-  ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
964 936 952 963 syl2anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
965 964 934 ffvelcdmd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
966 935 965 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) e. CC )
967 917 966 mulcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
968 860 684 eleqtrrd 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( ZZ>= ` 0 ) )
969 eluzfz2 
 |-  ( ( i + 1 ) e. ( ZZ>= ` 0 ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
970 968 969 syl 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
971 970 ad2antlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
972 oveq2 
 |-  ( k = ( i + 1 ) -> ( ( i + 1 ) _C k ) = ( ( i + 1 ) _C ( i + 1 ) ) )
973 638 fveq1d 
 |-  ( k = ( i + 1 ) -> ( ( C ` k ) ` x ) = ( ( C ` ( i + 1 ) ) ` x ) )
974 oveq2 
 |-  ( k = ( i + 1 ) -> ( ( i + 1 ) - k ) = ( ( i + 1 ) - ( i + 1 ) ) )
975 974 fveq2d 
 |-  ( k = ( i + 1 ) -> ( D ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) )
976 975 fveq1d 
 |-  ( k = ( i + 1 ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
977 973 976 oveq12d 
 |-  ( k = ( i + 1 ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
978 972 977 oveq12d 
 |-  ( k = ( i + 1 ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) )
979 470 909 910 967 971 978 fsumsplit1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
980 979 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
981 883 902 980 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
982 850 859 981 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + ( sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
983 775 811 982 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
984 438 442 983 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
985 984 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
986 422 985 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( S _D ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
987 986 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( S _D ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
988 191 193 987 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
989 180 181 184 988 syl21anc 
 |-  ( ( i e. ( 0 ..^ N ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) /\ ph ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
990 989 3exp 
 |-  ( i e. ( 0 ..^ N ) -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) ) )
991 44 57 70 83 179 990 fzind2 
 |-  ( n e. ( 0 ... N ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) ) )
992 31 991 vtoclg 
 |-  ( N e. NN0 -> ( N e. ( 0 ... N ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) ) ) )
993 5 16 992 sylc 
 |-  ( ph -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) ) )
994 12 993 mpd 
 |-  ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) )