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 ) ) ) ) ) |