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 sseldi
 |-  ( 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 mulid2d
 |-  ( ( 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 ffvelrnd
 |-  ( ( ( 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 ffvelrnd
 |-  ( ( ( 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 ffvelrnda
 |-  ( ( ( ( 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 ffvelrnda
 |-  ( ( ( ( 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 addid2d
 |-  ( ( ( ( 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 ( 0 ... i )
452 nfcv
 |-  F/_ k ( 0 ... i )
453 nfcv
 |-  F/_ h ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) )
454 nfcv
 |-  F/_ k ( i _C h )
455 nfcv
 |-  F/_ k x.
456 nfcv
 |-  F/_ k ( h + 1 )
457 345 456 nffv
 |-  F/_ k ( C ` ( h + 1 ) )
458 nfcv
 |-  F/_ k x
459 457 458 nffv
 |-  F/_ k ( ( C ` ( h + 1 ) ) ` x )
460 nfmpt1
 |-  F/_ k ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) )
461 11 460 nfcxfr
 |-  F/_ k D
462 nfcv
 |-  F/_ k ( i - h )
463 461 462 nffv
 |-  F/_ k ( D ` ( i - h ) )
464 463 458 nffv
 |-  F/_ k ( ( D ` ( i - h ) ) ` x )
465 459 455 464 nfov
 |-  F/_ k ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) )
466 454 455 465 nfov
 |-  F/_ k ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) )
467 450 451 452 453 466 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 ) ) )
468 467 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 ) ) ) )
469 1zzd
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 1 e. ZZ )
470 96 a1i
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 0 e. ZZ )
471 234 ad2antlr
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> i e. ZZ )
472 nfv
 |-  F/ k ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X )
473 nfcv
 |-  F/_ k h
474 473 452 nfel
 |-  F/ k h e. ( 0 ... i )
475 472 474 nfan
 |-  F/ k ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) )
476 466 349 nfel
 |-  F/ k ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC
477 475 476 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 )
478 eleq1
 |-  ( k = h -> ( k e. ( 0 ... i ) <-> h e. ( 0 ... i ) ) )
479 478 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 ) ) ) )
480 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 ) )
481 479 480 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 ) ) )
482 477 481 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 )
483 oveq2
 |-  ( h = ( j - 1 ) -> ( i _C h ) = ( i _C ( j - 1 ) ) )
484 fvoveq1
 |-  ( h = ( j - 1 ) -> ( C ` ( h + 1 ) ) = ( C ` ( ( j - 1 ) + 1 ) ) )
485 484 fveq1d
 |-  ( h = ( j - 1 ) -> ( ( C ` ( h + 1 ) ) ` x ) = ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) )
486 oveq2
 |-  ( h = ( j - 1 ) -> ( i - h ) = ( i - ( j - 1 ) ) )
487 486 fveq2d
 |-  ( h = ( j - 1 ) -> ( D ` ( i - h ) ) = ( D ` ( i - ( j - 1 ) ) ) )
488 487 fveq1d
 |-  ( h = ( j - 1 ) -> ( ( D ` ( i - h ) ) ` x ) = ( ( D ` ( i - ( j - 1 ) ) ) ` x ) )
489 485 488 oveq12d
 |-  ( h = ( j - 1 ) -> ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) = ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) )
490 483 489 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 ) ) ) )
491 469 470 471 482 490 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 ) ) ) )
492 468 491 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 ) ) ) )
493 0p1e1
 |-  ( 0 + 1 ) = 1
494 493 oveq1i
 |-  ( ( 0 + 1 ) ... ( i + 1 ) ) = ( 1 ... ( i + 1 ) )
495 494 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 ) ) )
496 495 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 ) ) ) )
497 elfzelz
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> j e. ZZ )
498 497 zcnd
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> j e. CC )
499 1cnd
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 1 e. CC )
500 498 499 npcand
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> ( ( j - 1 ) + 1 ) = j )
501 500 fveq2d
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> ( C ` ( ( j - 1 ) + 1 ) ) = ( C ` j ) )
502 501 fveq1d
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) = ( ( C ` j ) ` x ) )
503 502 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) = ( ( C ` j ) ` x ) )
504 215 recnd
 |-  ( i e. ( 0 ..^ N ) -> i e. CC )
505 504 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. CC )
506 498 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. CC )
507 499 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. CC )
508 505 506 507 subsub3d
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i - ( j - 1 ) ) = ( ( i + 1 ) - j ) )
509 508 fveq2d
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( i - ( j - 1 ) ) ) = ( D ` ( ( i + 1 ) - j ) ) )
510 509 fveq1d
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( D ` ( i - ( j - 1 ) ) ) ` x ) = ( ( D ` ( ( i + 1 ) - j ) ) ` x ) )
511 503 510 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 ) ) )
512 511 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 ) ) ) )
513 512 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 ) ) ) )
514 513 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 ) ) ) )
515 nfv
 |-  F/ j ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X )
516 nfcv
 |-  F/_ j ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
517 fzfid
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... ( i + 1 ) ) e. Fin )
518 187 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. NN0 )
519 497 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ZZ )
520 1zzd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. ZZ )
521 519 520 zsubcld
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( j - 1 ) e. ZZ )
522 518 521 bccld
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. NN0 )
523 522 nn0cnd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
524 523 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
525 524 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
526 12 ad2antrr
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ph )
527 0zd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 e. ZZ )
528 208 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> N e. ZZ )
529 173 a1i
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 0 e. RR )
530 497 zred
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> j e. RR )
531 1red
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 1 e. RR )
532 0lt1
 |-  0 < 1
533 532 a1i
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 0 < 1 )
534 elfzle1
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 1 <_ j )
535 529 531 530 533 534 ltletrd
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 0 < j )
536 529 530 535 ltled
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> 0 <_ j )
537 536 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 <_ j )
538 530 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. RR )
539 215 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. RR )
540 1red
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. RR )
541 539 540 readdcld
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) e. RR )
542 213 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> N e. RR )
543 elfzle2
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> j <_ ( i + 1 ) )
544 543 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j <_ ( i + 1 ) )
545 301 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) <_ N )
546 538 541 542 544 545 letrd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j <_ N )
547 527 528 519 537 546 elfzd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ( 0 ... N ) )
548 547 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ( 0 ... N ) )
549 526 548 355 syl2anc
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( C ` j ) : X --> CC )
550 549 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( C ` j ) : X --> CC )
551 simplr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> x e. X )
552 550 551 ffvelrnd
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( C ` j ) ` x ) e. CC )
553 234 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. ZZ )
554 553 peano2zd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) e. ZZ )
555 554 519 zsubcld
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ZZ )
556 541 538 subge0d
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( 0 <_ ( ( i + 1 ) - j ) <-> j <_ ( i + 1 ) ) )
557 544 556 mpbird
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 <_ ( ( i + 1 ) - j ) )
558 541 538 resubcld
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. RR )
559 558 leidd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) <_ ( ( i + 1 ) - j ) )
560 530 535 elrpd
 |-  ( j e. ( 1 ... ( i + 1 ) ) -> j e. RR+ )
561 560 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. RR+ )
562 541 561 ltsubrpd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < ( i + 1 ) )
563 558 541 542 562 545 ltletrd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < N )
564 558 558 542 559 563 lelttrd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < N )
565 558 542 564 ltled
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) <_ N )
566 527 528 555 557 565 elfzd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ( 0 ... N ) )
567 566 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ( 0 ... N ) )
568 nfv
 |-  F/ k ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) )
569 nfcv
 |-  F/_ k ( ( i + 1 ) - j )
570 461 569 nffv
 |-  F/_ k ( D ` ( ( i + 1 ) - j ) )
571 570 348 349 nff
 |-  F/ k ( D ` ( ( i + 1 ) - j ) ) : X --> CC
572 568 571 nfim
 |-  F/ k ( ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
573 ovex
 |-  ( ( i + 1 ) - j ) e. _V
574 eleq1
 |-  ( k = ( ( i + 1 ) - j ) -> ( k e. ( 0 ... N ) <-> ( ( i + 1 ) - j ) e. ( 0 ... N ) ) )
575 574 anbi2d
 |-  ( k = ( ( i + 1 ) - j ) -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) ) )
576 fveq2
 |-  ( k = ( ( i + 1 ) - j ) -> ( D ` k ) = ( D ` ( ( i + 1 ) - j ) ) )
577 576 feq1d
 |-  ( k = ( ( i + 1 ) - j ) -> ( ( D ` k ) : X --> CC <-> ( D ` ( ( i + 1 ) - j ) ) : X --> CC ) )
578 575 577 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 ) ) )
579 11 a1i
 |-  ( ph -> D = ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) ) )
580 fvexd
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) e. _V )
581 579 580 fvmpt2d
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) = ( ( S Dn G ) ` k ) )
582 581 feq1d
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( D ` k ) : X --> CC <-> ( ( S Dn G ) ` k ) : X --> CC ) )
583 9 582 mpbird
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC )
584 572 573 578 583 vtoclf
 |-  ( ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
585 526 567 584 syl2anc
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
586 585 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
587 586 551 ffvelrnd
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) e. CC )
588 552 587 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 )
589 525 588 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 )
590 1zzd
 |-  ( i e. ( 0 ..^ N ) -> 1 e. ZZ )
591 234 peano2zd
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ZZ )
592 493 eqcomi
 |-  1 = ( 0 + 1 )
593 592 a1i
 |-  ( i e. ( 0 ..^ N ) -> 1 = ( 0 + 1 ) )
594 173 a1i
 |-  ( i e. ( 0 ..^ N ) -> 0 e. RR )
595 1red
 |-  ( i e. ( 0 ..^ N ) -> 1 e. RR )
596 187 nn0ge0d
 |-  ( i e. ( 0 ..^ N ) -> 0 <_ i )
597 594 215 595 596 leadd1dd
 |-  ( i e. ( 0 ..^ N ) -> ( 0 + 1 ) <_ ( i + 1 ) )
598 593 597 eqbrtrd
 |-  ( i e. ( 0 ..^ N ) -> 1 <_ ( i + 1 ) )
599 590 591 598 3jca
 |-  ( i e. ( 0 ..^ N ) -> ( 1 e. ZZ /\ ( i + 1 ) e. ZZ /\ 1 <_ ( i + 1 ) ) )
600 eluz2
 |-  ( ( i + 1 ) e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ ( i + 1 ) e. ZZ /\ 1 <_ ( i + 1 ) ) )
601 599 600 sylibr
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( ZZ>= ` 1 ) )
602 eluzfz2
 |-  ( ( i + 1 ) e. ( ZZ>= ` 1 ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
603 601 602 syl
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
604 603 ad2antlr
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
605 oveq1
 |-  ( j = ( i + 1 ) -> ( j - 1 ) = ( ( i + 1 ) - 1 ) )
606 605 oveq2d
 |-  ( j = ( i + 1 ) -> ( i _C ( j - 1 ) ) = ( i _C ( ( i + 1 ) - 1 ) ) )
607 fveq2
 |-  ( j = ( i + 1 ) -> ( C ` j ) = ( C ` ( i + 1 ) ) )
608 607 fveq1d
 |-  ( j = ( i + 1 ) -> ( ( C ` j ) ` x ) = ( ( C ` ( i + 1 ) ) ` x ) )
609 oveq2
 |-  ( j = ( i + 1 ) -> ( ( i + 1 ) - j ) = ( ( i + 1 ) - ( i + 1 ) ) )
610 609 fveq2d
 |-  ( j = ( i + 1 ) -> ( D ` ( ( i + 1 ) - j ) ) = ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) )
611 610 fveq1d
 |-  ( j = ( i + 1 ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) = ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
612 608 611 oveq12d
 |-  ( j = ( i + 1 ) -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
613 606 612 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 ) ) ) )
614 515 516 517 589 604 613 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 ) ) ) ) )
615 1cnd
 |-  ( i e. ( 0 ..^ N ) -> 1 e. CC )
616 504 615 pncand
 |-  ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - 1 ) = i )
617 616 oveq2d
 |-  ( i e. ( 0 ..^ N ) -> ( i _C ( ( i + 1 ) - 1 ) ) = ( i _C i ) )
618 bcnn
 |-  ( i e. NN0 -> ( i _C i ) = 1 )
619 187 618 syl
 |-  ( i e. ( 0 ..^ N ) -> ( i _C i ) = 1 )
620 617 619 eqtrd
 |-  ( i e. ( 0 ..^ N ) -> ( i _C ( ( i + 1 ) - 1 ) ) = 1 )
621 504 615 addcld
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. CC )
622 621 subidd
 |-  ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - ( i + 1 ) ) = 0 )
623 622 fveq2d
 |-  ( i e. ( 0 ..^ N ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) = ( D ` 0 ) )
624 623 fveq1d
 |-  ( i e. ( 0 ..^ N ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) = ( ( D ` 0 ) ` x ) )
625 624 oveq2d
 |-  ( i e. ( 0 ..^ N ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) )
626 620 625 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 ) ) ) )
627 626 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 ) ) ) )
628 simpl
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ph )
629 fzofzp1
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ... N ) )
630 629 adantl
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ... N ) )
631 nfv
 |-  F/ k ( ph /\ ( i + 1 ) e. ( 0 ... N ) )
632 nfcv
 |-  F/_ k ( i + 1 )
633 345 632 nffv
 |-  F/_ k ( C ` ( i + 1 ) )
634 633 348 349 nff
 |-  F/ k ( C ` ( i + 1 ) ) : X --> CC
635 631 634 nfim
 |-  F/ k ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
636 ovex
 |-  ( i + 1 ) e. _V
637 eleq1
 |-  ( k = ( i + 1 ) -> ( k e. ( 0 ... N ) <-> ( i + 1 ) e. ( 0 ... N ) ) )
638 637 anbi2d
 |-  ( k = ( i + 1 ) -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) ) )
639 fveq2
 |-  ( k = ( i + 1 ) -> ( C ` k ) = ( C ` ( i + 1 ) ) )
640 639 feq1d
 |-  ( k = ( i + 1 ) -> ( ( C ` k ) : X --> CC <-> ( C ` ( i + 1 ) ) : X --> CC ) )
641 638 640 imbi12d
 |-  ( k = ( i + 1 ) -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC ) ) )
642 635 636 641 229 vtoclf
 |-  ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
643 628 630 642 syl2anc
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
644 643 ffvelrnda
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( C ` ( i + 1 ) ) ` x ) e. CC )
645 nfv
 |-  F/ k ( ph /\ 0 e. ( 0 ... N ) )
646 nfcv
 |-  F/_ k 0
647 461 646 nffv
 |-  F/_ k ( D ` 0 )
648 647 348 349 nff
 |-  F/ k ( D ` 0 ) : X --> CC
649 645 648 nfim
 |-  F/ k ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC )
650 c0ex
 |-  0 e. _V
651 eleq1
 |-  ( k = 0 -> ( k e. ( 0 ... N ) <-> 0 e. ( 0 ... N ) ) )
652 651 anbi2d
 |-  ( k = 0 -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ 0 e. ( 0 ... N ) ) ) )
653 fveq2
 |-  ( k = 0 -> ( D ` k ) = ( D ` 0 ) )
654 653 feq1d
 |-  ( k = 0 -> ( ( D ` k ) : X --> CC <-> ( D ` 0 ) : X --> CC ) )
655 652 654 imbi12d
 |-  ( k = 0 -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC ) ) )
656 649 650 655 583 vtoclf
 |-  ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC )
657 12 117 656 syl2anc
 |-  ( ph -> ( D ` 0 ) : X --> CC )
658 657 adantr
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` 0 ) : X --> CC )
659 658 ffvelrnda
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` 0 ) ` x ) e. CC )
660 644 659 mulcld
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) e. CC )
661 660 mulid2d
 |-  ( ( ( 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 ) ) )
662 627 661 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 ) ) )
663 1m1e0
 |-  ( 1 - 1 ) = 0
664 663 fveq2i
 |-  ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
665 13 eqcomi
 |-  ( ZZ>= ` 0 ) = NN0
666 664 665 eqtr2i
 |-  NN0 = ( ZZ>= ` ( 1 - 1 ) )
667 666 a1i
 |-  ( i e. ( 0 ..^ N ) -> NN0 = ( ZZ>= ` ( 1 - 1 ) ) )
668 187 667 eleqtrd
 |-  ( i e. ( 0 ..^ N ) -> i e. ( ZZ>= ` ( 1 - 1 ) ) )
669 fzdifsuc2
 |-  ( i e. ( ZZ>= ` ( 1 - 1 ) ) -> ( 1 ... i ) = ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
670 668 669 syl
 |-  ( i e. ( 0 ..^ N ) -> ( 1 ... i ) = ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
671 670 eqcomd
 |-  ( i e. ( 0 ..^ N ) -> ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) = ( 1 ... i ) )
672 671 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 ) ) ) )
673 672 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 ) ) ) )
674 662 673 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 ) ) ) ) )
675 514 614 674 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 ) ) ) ) )
676 492 496 675 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 ) ) ) ) )
677 nfcv
 |-  F/_ k ( i _C 0 )
678 345 646 nffv
 |-  F/_ k ( C ` 0 )
679 678 458 nffv
 |-  F/_ k ( ( C ` 0 ) ` x )
680 nfcv
 |-  F/_ k ( ( i + 1 ) - 0 )
681 461 680 nffv
 |-  F/_ k ( D ` ( ( i + 1 ) - 0 ) )
682 681 458 nffv
 |-  F/_ k ( ( D ` ( ( i + 1 ) - 0 ) ) ` x )
683 679 455 682 nfov
 |-  F/_ k ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) )
684 677 455 683 nfov
 |-  F/_ k ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
685 665 a1i
 |-  ( i e. ( 0 ..^ N ) -> ( ZZ>= ` 0 ) = NN0 )
686 187 685 eleqtrrd
 |-  ( i e. ( 0 ..^ N ) -> i e. ( ZZ>= ` 0 ) )
687 eluzfz1
 |-  ( i e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... i ) )
688 686 687 syl
 |-  ( i e. ( 0 ..^ N ) -> 0 e. ( 0 ... i ) )
689 688 ad2antlr
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 0 e. ( 0 ... i ) )
690 oveq2
 |-  ( k = 0 -> ( i _C k ) = ( i _C 0 ) )
691 110 fveq1d
 |-  ( k = 0 -> ( ( C ` k ) ` x ) = ( ( C ` 0 ) ` x ) )
692 oveq2
 |-  ( k = 0 -> ( ( i + 1 ) - k ) = ( ( i + 1 ) - 0 ) )
693 692 fveq2d
 |-  ( k = 0 -> ( D ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - 0 ) ) )
694 693 fveq1d
 |-  ( k = 0 -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) )
695 691 694 oveq12d
 |-  ( k = 0 -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
696 690 695 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 ) ) ) )
697 472 684 439 441 689 696 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 ) ) ) ) )
698 621 subid1d
 |-  ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - 0 ) = ( i + 1 ) )
699 698 fveq2d
 |-  ( i e. ( 0 ..^ N ) -> ( D ` ( ( i + 1 ) - 0 ) ) = ( D ` ( i + 1 ) ) )
700 699 fveq1d
 |-  ( i e. ( 0 ..^ N ) -> ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) = ( ( D ` ( i + 1 ) ) ` x ) )
701 700 oveq2d
 |-  ( i e. ( 0 ..^ N ) -> ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) )
702 701 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 ) ) ) )
703 702 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 ) ) ) ) )
704 703 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 ) ) ) ) )
705 bcn0
 |-  ( i e. NN0 -> ( i _C 0 ) = 1 )
706 187 705 syl
 |-  ( i e. ( 0 ..^ N ) -> ( i _C 0 ) = 1 )
707 706 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 ) ) ) )
708 707 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 ) ) ) )
709 678 348 349 nff
 |-  F/ k ( C ` 0 ) : X --> CC
710 645 709 nfim
 |-  F/ k ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC )
711 110 feq1d
 |-  ( k = 0 -> ( ( C ` k ) : X --> CC <-> ( C ` 0 ) : X --> CC ) )
712 652 711 imbi12d
 |-  ( k = 0 -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC ) ) )
713 710 650 712 229 vtoclf
 |-  ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC )
714 12 117 713 syl2anc
 |-  ( ph -> ( C ` 0 ) : X --> CC )
715 714 adantr
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( C ` 0 ) : X --> CC )
716 715 ffvelrnda
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( C ` 0 ) ` x ) e. CC )
717 461 632 nffv
 |-  F/_ k ( D ` ( i + 1 ) )
718 717 348 349 nff
 |-  F/ k ( D ` ( i + 1 ) ) : X --> CC
719 631 718 nfim
 |-  F/ k ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
720 fveq2
 |-  ( k = ( i + 1 ) -> ( D ` k ) = ( D ` ( i + 1 ) ) )
721 720 feq1d
 |-  ( k = ( i + 1 ) -> ( ( D ` k ) : X --> CC <-> ( D ` ( i + 1 ) ) : X --> CC ) )
722 638 721 imbi12d
 |-  ( k = ( i + 1 ) -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC ) ) )
723 719 636 722 583 vtoclf
 |-  ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
724 628 630 723 syl2anc
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
725 724 ffvelrnda
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` ( i + 1 ) ) ` x ) e. CC )
726 716 725 mulcld
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) e. CC )
727 726 mulid2d
 |-  ( ( ( 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 ) ) )
728 708 727 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 ) ) )
729 nfv
 |-  F/ j i e. ( 0 ..^ N )
730 1zzd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> 1 e. ZZ )
731 234 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> i e. ZZ )
732 eldifi
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ( 0 ... i ) )
733 elfzelz
 |-  ( j e. ( 0 ... i ) -> j e. ZZ )
734 732 733 syl
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ZZ )
735 734 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j e. ZZ )
736 elfznn0
 |-  ( j e. ( 0 ... i ) -> j e. NN0 )
737 732 736 syl
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. NN0 )
738 eldifsni
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j =/= 0 )
739 737 738 jca
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> ( j e. NN0 /\ j =/= 0 ) )
740 elnnne0
 |-  ( j e. NN <-> ( j e. NN0 /\ j =/= 0 ) )
741 739 740 sylibr
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. NN )
742 nnge1
 |-  ( j e. NN -> 1 <_ j )
743 741 742 syl
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> 1 <_ j )
744 743 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> 1 <_ j )
745 elfzle2
 |-  ( j e. ( 0 ... i ) -> j <_ i )
746 732 745 syl
 |-  ( j e. ( ( 0 ... i ) \ { 0 } ) -> j <_ i )
747 746 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j <_ i )
748 730 731 735 744 747 elfzd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j e. ( 1 ... i ) )
749 748 ex
 |-  ( i e. ( 0 ..^ N ) -> ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ( 1 ... i ) ) )
750 0zd
 |-  ( j e. ( 1 ... i ) -> 0 e. ZZ )
751 elfzel2
 |-  ( j e. ( 1 ... i ) -> i e. ZZ )
752 elfzelz
 |-  ( j e. ( 1 ... i ) -> j e. ZZ )
753 173 a1i
 |-  ( j e. ( 1 ... i ) -> 0 e. RR )
754 752 zred
 |-  ( j e. ( 1 ... i ) -> j e. RR )
755 1red
 |-  ( j e. ( 1 ... i ) -> 1 e. RR )
756 532 a1i
 |-  ( j e. ( 1 ... i ) -> 0 < 1 )
757 elfzle1
 |-  ( j e. ( 1 ... i ) -> 1 <_ j )
758 753 755 754 756 757 ltletrd
 |-  ( j e. ( 1 ... i ) -> 0 < j )
759 753 754 758 ltled
 |-  ( j e. ( 1 ... i ) -> 0 <_ j )
760 elfzle2
 |-  ( j e. ( 1 ... i ) -> j <_ i )
761 750 751 752 759 760 elfzd
 |-  ( j e. ( 1 ... i ) -> j e. ( 0 ... i ) )
762 753 758 gtned
 |-  ( j e. ( 1 ... i ) -> j =/= 0 )
763 nelsn
 |-  ( j =/= 0 -> -. j e. { 0 } )
764 762 763 syl
 |-  ( j e. ( 1 ... i ) -> -. j e. { 0 } )
765 761 764 eldifd
 |-  ( j e. ( 1 ... i ) -> j e. ( ( 0 ... i ) \ { 0 } ) )
766 765 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> j e. ( ( 0 ... i ) \ { 0 } ) )
767 766 ex
 |-  ( i e. ( 0 ..^ N ) -> ( j e. ( 1 ... i ) -> j e. ( ( 0 ... i ) \ { 0 } ) ) )
768 749 767 impbid
 |-  ( i e. ( 0 ..^ N ) -> ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
769 729 768 alrimi
 |-  ( i e. ( 0 ..^ N ) -> A. j ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
770 dfcleq
 |-  ( ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) <-> A. j ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
771 769 770 sylibr
 |-  ( i e. ( 0 ..^ N ) -> ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) )
772 771 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 ) ) ) )
773 772 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 ) ) ) )
774 728 773 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 ) ) ) ) )
775 697 704 774 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 ) ) ) ) )
776 676 775 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 ) ) ) ) ) )
777 fzfid
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... i ) e. Fin )
778 187 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> i e. NN0 )
779 766 734 syl
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> j e. ZZ )
780 1zzd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> 1 e. ZZ )
781 779 780 zsubcld
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( j - 1 ) e. ZZ )
782 778 781 bccld
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. NN0 )
783 782 nn0cnd
 |-  ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
784 783 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
785 784 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
786 simpl
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) )
787 fzelp1
 |-  ( j e. ( 1 ... i ) -> j e. ( 1 ... ( i + 1 ) ) )
788 787 adantl
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> j e. ( 1 ... ( i + 1 ) ) )
789 786 788 552 syl2anc
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( C ` j ) ` x ) e. CC )
790 788 587 syldan
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) e. CC )
791 789 790 mulcld
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) e. CC )
792 785 791 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 )
793 777 792 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 )
794 187 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> i e. NN0 )
795 elfzelz
 |-  ( k e. ( 1 ... i ) -> k e. ZZ )
796 795 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> k e. ZZ )
797 794 796 bccld
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. NN0 )
798 797 nn0cnd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
799 798 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
800 799 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
801 simpll
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ph /\ i e. ( 0 ..^ N ) ) )
802 simplr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> x e. X )
803 761 ssriv
 |-  ( 1 ... i ) C_ ( 0 ... i )
804 id
 |-  ( k e. ( 1 ... i ) -> k e. ( 1 ... i ) )
805 803 804 sseldi
 |-  ( k e. ( 1 ... i ) -> k e. ( 0 ... i ) )
806 805 adantl
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> k e. ( 0 ... i ) )
807 801 802 806 433 syl21anc
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( C ` k ) ` x ) e. CC )
808 806 435 syldan
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
809 807 808 mulcld
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) e. CC )
810 800 809 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 )
811 777 810 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 )
812 660 793 726 811 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 ) ) ) ) ) )
813 oveq1
 |-  ( j = k -> ( j - 1 ) = ( k - 1 ) )
814 813 oveq2d
 |-  ( j = k -> ( i _C ( j - 1 ) ) = ( i _C ( k - 1 ) ) )
815 fveq2
 |-  ( j = k -> ( C ` j ) = ( C ` k ) )
816 815 fveq1d
 |-  ( j = k -> ( ( C ` j ) ` x ) = ( ( C ` k ) ` x ) )
817 oveq2
 |-  ( j = k -> ( ( i + 1 ) - j ) = ( ( i + 1 ) - k ) )
818 817 fveq2d
 |-  ( j = k -> ( D ` ( ( i + 1 ) - j ) ) = ( D ` ( ( i + 1 ) - k ) ) )
819 818 fveq1d
 |-  ( j = k -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) = ( ( D ` ( ( i + 1 ) - k ) ) ` x ) )
820 816 819 oveq12d
 |-  ( j = k -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
821 814 820 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 ) ) ) )
822 nfcv
 |-  F/_ k ( 1 ... i )
823 nfcv
 |-  F/_ j ( 1 ... i )
824 nfcv
 |-  F/_ k ( i _C ( j - 1 ) )
825 347 458 nffv
 |-  F/_ k ( ( C ` j ) ` x )
826 570 458 nffv
 |-  F/_ k ( ( D ` ( ( i + 1 ) - j ) ) ` x )
827 825 455 826 nfov
 |-  F/_ k ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) )
828 824 455 827 nfov
 |-  F/_ k ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) )
829 nfcv
 |-  F/_ j ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
830 821 822 823 828 829 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 ) ) )
831 830 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 ) ) ) )
832 831 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 ) ) ) ) )
833 peano2zm
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
834 796 833 syl
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( k - 1 ) e. ZZ )
835 794 834 bccld
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. NN0 )
836 835 nn0cnd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
837 836 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
838 837 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
839 838 809 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 )
840 777 839 810 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 ) ) ) ) )
841 840 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 ) ) ) ) )
842 836 798 addcomd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i _C ( k - 1 ) ) + ( i _C k ) ) = ( ( i _C k ) + ( i _C ( k - 1 ) ) ) )
843 bcpasc
 |-  ( ( i e. NN0 /\ k e. ZZ ) -> ( ( i _C k ) + ( i _C ( k - 1 ) ) ) = ( ( i + 1 ) _C k ) )
844 794 796 843 syl2anc
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i _C k ) + ( i _C ( k - 1 ) ) ) = ( ( i + 1 ) _C k ) )
845 842 844 eqtr2d
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) = ( ( i _C ( k - 1 ) ) + ( i _C k ) ) )
846 845 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 ) ) ) )
847 846 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 ) ) ) )
848 847 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 ) ) ) )
849 838 800 809 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 ) ) ) ) )
850 848 849 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 ) ) ) )
851 850 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 ) ) ) )
852 832 841 851 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 ) ) ) )
853 852 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 ) ) ) ) )
854 peano2nn0
 |-  ( i e. NN0 -> ( i + 1 ) e. NN0 )
855 794 854 syl
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i + 1 ) e. NN0 )
856 855 796 bccld
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
857 856 nn0cnd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
858 857 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
859 858 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
860 859 809 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 )
861 777 860 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 )
862 660 726 861 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 ) ) ) ) ) )
863 187 854 syl
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. NN0 )
864 bcn0
 |-  ( ( i + 1 ) e. NN0 -> ( ( i + 1 ) _C 0 ) = 1 )
865 863 864 syl
 |-  ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) _C 0 ) = 1 )
866 865 701 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 ) ) ) )
867 866 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 ) ) ) )
868 867 727 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 ) ) ) )
869 771 ad2antlr
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) )
870 869 eqcomd
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... i ) = ( ( 0 ... i ) \ { 0 } ) )
871 870 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 ) ) ) )
872 868 871 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 ) ) ) ) )
873 nfcv
 |-  F/_ k ( ( i + 1 ) _C 0 )
874 873 455 683 nfov
 |-  F/_ k ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
875 199 854 syl
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. NN0 )
876 875 201 bccld
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
877 876 nn0cnd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
878 877 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
879 878 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
880 879 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 )
881 oveq2
 |-  ( k = 0 -> ( ( i + 1 ) _C k ) = ( ( i + 1 ) _C 0 ) )
882 881 695 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 ) ) ) )
883 472 874 439 880 689 882 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 ) ) ) ) )
884 883 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 ) ) ) )
885 872 884 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 ) ) ) )
886 885 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 ) ) ) ) )
887 bcnn
 |-  ( ( i + 1 ) e. NN0 -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
888 863 887 syl
 |-  ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
889 888 ad2antlr
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
890 889 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 ) ) ) )
891 623 adantl
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) = ( D ` 0 ) )
892 891 feq1d
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC <-> ( D ` 0 ) : X --> CC ) )
893 658 892 mpbird
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC )
894 893 adantr
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC )
895 simpr
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> x e. X )
896 894 895 ffvelrnd
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) e. CC )
897 644 896 mulcld
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) e. CC )
898 897 mulid2d
 |-  ( ( ( 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 ) ) )
899 625 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 ) ) )
900 890 898 899 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 ) ) ) )
901 fzdifsuc
 |-  ( i e. ( ZZ>= ` 0 ) -> ( 0 ... i ) = ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
902 686 901 syl
 |-  ( i e. ( 0 ..^ N ) -> ( 0 ... i ) = ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
903 902 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 ) ) ) )
904 903 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 ) ) ) )
905 900 904 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 ) ) ) ) )
906 nfcv
 |-  F/_ k ( ( i + 1 ) _C ( i + 1 ) )
907 633 458 nffv
 |-  F/_ k ( ( C ` ( i + 1 ) ) ` x )
908 nfcv
 |-  F/_ k ( ( i + 1 ) - ( i + 1 ) )
909 461 908 nffv
 |-  F/_ k ( D ` ( ( i + 1 ) - ( i + 1 ) ) )
910 909 458 nffv
 |-  F/_ k ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x )
911 907 455 910 nfov
 |-  F/_ k ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
912 906 455 911 nfov
 |-  F/_ k ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
913 fzfid
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 0 ... ( i + 1 ) ) e. Fin )
914 863 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. NN0 )
915 elfzelz
 |-  ( k e. ( 0 ... ( i + 1 ) ) -> k e. ZZ )
916 915 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ZZ )
917 914 916 bccld
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
918 917 nn0cnd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
919 918 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
920 919 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
921 628 adantr
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ph )
922 96 a1i
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 e. ZZ )
923 208 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> N e. ZZ )
924 elfzle1
 |-  ( k e. ( 0 ... ( i + 1 ) ) -> 0 <_ k )
925 924 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 <_ k )
926 916 zred
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. RR )
927 914 nn0red
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. RR )
928 213 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> N e. RR )
929 elfzle2
 |-  ( k e. ( 0 ... ( i + 1 ) ) -> k <_ ( i + 1 ) )
930 929 adantl
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k <_ ( i + 1 ) )
931 301 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) <_ N )
932 926 927 928 930 931 letrd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k <_ N )
933 922 923 916 925 932 elfzd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ( 0 ... N ) )
934 933 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ( 0 ... N ) )
935 921 934 229 syl2anc
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( C ` k ) : X --> CC )
936 935 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( C ` k ) : X --> CC )
937 simplr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> x e. X )
938 936 937 ffvelrnd
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( C ` k ) ` x ) e. CC )
939 921 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ph )
940 591 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. ZZ )
941 940 916 zsubcld
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ZZ )
942 927 926 subge0d
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( 0 <_ ( ( i + 1 ) - k ) <-> k <_ ( i + 1 ) ) )
943 930 942 mpbird
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 <_ ( ( i + 1 ) - k ) )
944 927 926 resubcld
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. RR )
945 928 926 resubcld
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - k ) e. RR )
946 928 173 247 sylancl
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - 0 ) e. RR )
947 927 928 926 931 lesub1dd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ ( N - k ) )
948 173 a1i
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 e. RR )
949 948 926 928 925 lesub2dd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - k ) <_ ( N - 0 ) )
950 944 945 946 947 949 letrd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ ( N - 0 ) )
951 253 adantr
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - 0 ) = N )
952 950 951 breqtrd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ N )
953 922 923 941 943 952 elfzd
 |-  ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
954 953 adantll
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
955 954 adantlr
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
956 fveq2
 |-  ( j = ( ( i + 1 ) - k ) -> ( D ` j ) = ( D ` ( ( i + 1 ) - k ) ) )
957 956 feq1d
 |-  ( j = ( ( i + 1 ) - k ) -> ( ( D ` j ) : X --> CC <-> ( D ` ( ( i + 1 ) - k ) ) : X --> CC ) )
958 310 957 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 ) ) )
959 461 346 nffv
 |-  F/_ k ( D ` j )
960 959 348 349 nff
 |-  F/ k ( D ` j ) : X --> CC
961 343 960 nfim
 |-  F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC )
962 fveq2
 |-  ( k = j -> ( D ` k ) = ( D ` j ) )
963 962 feq1d
 |-  ( k = j -> ( ( D ` k ) : X --> CC <-> ( D ` j ) : X --> CC ) )
964 267 963 imbi12d
 |-  ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC ) ) )
965 961 964 583 chvarfv
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC )
966 308 958 965 vtocl
 |-  ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
967 939 955 966 syl2anc
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
968 967 937 ffvelrnd
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
969 938 968 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 )
970 920 969 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 )
971 863 685 eleqtrrd
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( ZZ>= ` 0 ) )
972 eluzfz2
 |-  ( ( i + 1 ) e. ( ZZ>= ` 0 ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
973 971 972 syl
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
974 973 ad2antlr
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
975 oveq2
 |-  ( k = ( i + 1 ) -> ( ( i + 1 ) _C k ) = ( ( i + 1 ) _C ( i + 1 ) ) )
976 639 fveq1d
 |-  ( k = ( i + 1 ) -> ( ( C ` k ) ` x ) = ( ( C ` ( i + 1 ) ) ` x ) )
977 oveq2
 |-  ( k = ( i + 1 ) -> ( ( i + 1 ) - k ) = ( ( i + 1 ) - ( i + 1 ) ) )
978 977 fveq2d
 |-  ( k = ( i + 1 ) -> ( D ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) )
979 978 fveq1d
 |-  ( k = ( i + 1 ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
980 976 979 oveq12d
 |-  ( k = ( i + 1 ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
981 975 980 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 ) ) ) )
982 472 912 913 970 974 981 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 ) ) ) ) )
983 982 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 ) ) ) )
984 886 905 983 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 ) ) ) )
985 853 862 984 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 ) ) ) )
986 776 812 985 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 ) ) ) )
987 438 442 986 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 ) ) ) )
988 987 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 ) ) ) ) )
989 422 988 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 ) ) ) ) )
990 989 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 ) ) ) ) )
991 191 193 990 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 ) ) ) ) )
992 180 181 184 991 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 ) ) ) ) )
993 992 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 ) ) ) ) ) ) )
994 44 57 70 83 179 993 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 ) ) ) ) ) )
995 31 994 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 ) ) ) ) ) ) )
996 5 16 995 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 ) ) ) ) ) )
997 12 996 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 ) ) ) ) )