Metamath Proof Explorer

Theorem breprexplemc

Description: Lemma for breprexp (induction step). (Contributed by Thierry Arnoux, 6-Dec-2021)

Ref Expression
Hypotheses breprexp.n 
|- ( ph -> N e. NN0 )
breprexp.s 
|- ( ph -> S e. NN0 )
breprexp.z 
|- ( ph -> Z e. CC )
breprexp.h 
|- ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
breprexplemc.t 
|- ( ph -> T e. NN0 )
breprexplemc.s 
|- ( ph -> ( T + 1 ) <_ S )
breprexplemc.1 
|- ( ph -> prod_ a e. ( 0 ..^ T ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( T x. N ) ) sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) )
Assertion breprexplemc 
|- ( ph -> prod_ a e. ( 0 ..^ ( T + 1 ) ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) )

Proof

Step Hyp Ref Expression
1 breprexp.n 
 |-  ( ph -> N e. NN0 )
2 breprexp.s 
 |-  ( ph -> S e. NN0 )
3 breprexp.z 
 |-  ( ph -> Z e. CC )
4 breprexp.h 
 |-  ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
5 breprexplemc.t 
 |-  ( ph -> T e. NN0 )
6 breprexplemc.s 
 |-  ( ph -> ( T + 1 ) <_ S )
7 breprexplemc.1 
 |-  ( ph -> prod_ a e. ( 0 ..^ T ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( T x. N ) ) sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) )
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 5 8 eleqtrdi 
 |-  ( ph -> T e. ( ZZ>= ` 0 ) )
10 fzosplitsn 
 |-  ( T e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( T + 1 ) ) = ( ( 0 ..^ T ) u. { T } ) )
11 9 10 syl 
 |-  ( ph -> ( 0 ..^ ( T + 1 ) ) = ( ( 0 ..^ T ) u. { T } ) )
12 11 prodeq1d 
 |-  ( ph -> prod_ a e. ( 0 ..^ ( T + 1 ) ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = prod_ a e. ( ( 0 ..^ T ) u. { T } ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) )
13 nfv 
 |-  F/ a ph
14 nfcv 
 |-  F/_ a sum_ b e. ( 1 ... N ) ( ( ( L ` T ) ` b ) x. ( Z ^ b ) )
15 fzofi 
 |-  ( 0 ..^ T ) e. Fin
16 15 a1i 
 |-  ( ph -> ( 0 ..^ T ) e. Fin )
17 fzonel 
 |-  -. T e. ( 0 ..^ T )
18 17 a1i 
 |-  ( ph -> -. T e. ( 0 ..^ T ) )
19 fzfid 
 |-  ( ( ph /\ a e. ( 0 ..^ T ) ) -> ( 1 ... N ) e. Fin )
20 1 ad2antrr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ T ) ) /\ b e. ( 1 ... N ) ) -> N e. NN0 )
21 2 ad2antrr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ T ) ) /\ b e. ( 1 ... N ) ) -> S e. NN0 )
22 3 ad2antrr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ T ) ) /\ b e. ( 1 ... N ) ) -> Z e. CC )
23 4 adantr 
 |-  ( ( ph /\ a e. ( 0 ..^ T ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
24 23 adantr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ T ) ) /\ b e. ( 1 ... N ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
25 5 nn0zd 
 |-  ( ph -> T e. ZZ )
26 2 nn0zd 
 |-  ( ph -> S e. ZZ )
27 5 nn0red 
 |-  ( ph -> T e. RR )
28 1red 
 |-  ( ph -> 1 e. RR )
29 27 28 readdcld 
 |-  ( ph -> ( T + 1 ) e. RR )
30 2 nn0red 
 |-  ( ph -> S e. RR )
31 27 lep1d 
 |-  ( ph -> T <_ ( T + 1 ) )
32 27 29 30 31 6 letrd 
 |-  ( ph -> T <_ S )
33 eluz1 
 |-  ( T e. ZZ -> ( S e. ( ZZ>= ` T ) <-> ( S e. ZZ /\ T <_ S ) ) )
34 33 biimpar 
 |-  ( ( T e. ZZ /\ ( S e. ZZ /\ T <_ S ) ) -> S e. ( ZZ>= ` T ) )
35 25 26 32 34 syl12anc 
 |-  ( ph -> S e. ( ZZ>= ` T ) )
36 fzoss2 
 |-  ( S e. ( ZZ>= ` T ) -> ( 0 ..^ T ) C_ ( 0 ..^ S ) )
37 35 36 syl 
 |-  ( ph -> ( 0 ..^ T ) C_ ( 0 ..^ S ) )
38 37 sselda 
 |-  ( ( ph /\ a e. ( 0 ..^ T ) ) -> a e. ( 0 ..^ S ) )
39 38 adantr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ T ) ) /\ b e. ( 1 ... N ) ) -> a e. ( 0 ..^ S ) )
40 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
41 40 a1i 
 |-  ( ( ph /\ a e. ( 0 ..^ T ) ) -> ( 1 ... N ) C_ NN )
42 41 sselda 
 |-  ( ( ( ph /\ a e. ( 0 ..^ T ) ) /\ b e. ( 1 ... N ) ) -> b e. NN )
43 20 21 22 24 39 42 breprexplemb 
 |-  ( ( ( ph /\ a e. ( 0 ..^ T ) ) /\ b e. ( 1 ... N ) ) -> ( ( L ` a ) ` b ) e. CC )
44 nnssnn0 
 |-  NN C_ NN0
45 40 44 sstri 
 |-  ( 1 ... N ) C_ NN0
46 45 a1i 
 |-  ( ph -> ( 1 ... N ) C_ NN0 )
47 46 ralrimivw 
 |-  ( ph -> A. a e. ( 0 ..^ T ) ( 1 ... N ) C_ NN0 )
48 47 r19.21bi 
 |-  ( ( ph /\ a e. ( 0 ..^ T ) ) -> ( 1 ... N ) C_ NN0 )
49 48 sselda 
 |-  ( ( ( ph /\ a e. ( 0 ..^ T ) ) /\ b e. ( 1 ... N ) ) -> b e. NN0 )
50 22 49 expcld 
 |-  ( ( ( ph /\ a e. ( 0 ..^ T ) ) /\ b e. ( 1 ... N ) ) -> ( Z ^ b ) e. CC )
51 43 50 mulcld 
 |-  ( ( ( ph /\ a e. ( 0 ..^ T ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) e. CC )
52 19 51 fsumcl 
 |-  ( ( ph /\ a e. ( 0 ..^ T ) ) -> sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) e. CC )
53 simpl 
 |-  ( ( a = T /\ b e. ( 1 ... N ) ) -> a = T )
54 53 fveq2d 
 |-  ( ( a = T /\ b e. ( 1 ... N ) ) -> ( L ` a ) = ( L ` T ) )
55 54 fveq1d 
 |-  ( ( a = T /\ b e. ( 1 ... N ) ) -> ( ( L ` a ) ` b ) = ( ( L ` T ) ` b ) )
56 55 oveq1d 
 |-  ( ( a = T /\ b e. ( 1 ... N ) ) -> ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) )
57 56 sumeq2dv 
 |-  ( a = T -> sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ b e. ( 1 ... N ) ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) )
58 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
59 1 adantr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> N e. NN0 )
60 2 adantr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> S e. NN0 )
61 3 adantr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> Z e. CC )
62 4 adantr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
63 5 nn0ge0d 
 |-  ( ph -> 0 <_ T )
64 zltp1le 
 |-  ( ( T e. ZZ /\ S e. ZZ ) -> ( T < S <-> ( T + 1 ) <_ S ) )
65 25 26 64 syl2anc 
 |-  ( ph -> ( T < S <-> ( T + 1 ) <_ S ) )
66 6 65 mpbird 
 |-  ( ph -> T < S )
67 0zd 
 |-  ( ph -> 0 e. ZZ )
68 elfzo 
 |-  ( ( T e. ZZ /\ 0 e. ZZ /\ S e. ZZ ) -> ( T e. ( 0 ..^ S ) <-> ( 0 <_ T /\ T < S ) ) )
69 25 67 26 68 syl3anc 
 |-  ( ph -> ( T e. ( 0 ..^ S ) <-> ( 0 <_ T /\ T < S ) ) )
70 63 66 69 mpbir2and 
 |-  ( ph -> T e. ( 0 ..^ S ) )
71 70 adantr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> T e. ( 0 ..^ S ) )
72 40 a1i 
 |-  ( ph -> ( 1 ... N ) C_ NN )
73 72 sselda 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> b e. NN )
74 59 60 61 62 71 73 breprexplemb 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( L ` T ) ` b ) e. CC )
75 46 sselda 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> b e. NN0 )
76 61 75 expcld 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( Z ^ b ) e. CC )
77 74 76 mulcld 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) e. CC )
78 58 77 fsumcl 
 |-  ( ph -> sum_ b e. ( 1 ... N ) ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) e. CC )
79 13 14 16 5 18 52 57 78 fprodsplitsn 
 |-  ( ph -> prod_ a e. ( ( 0 ..^ T ) u. { T } ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = ( prod_ a e. ( 0 ..^ T ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) x. sum_ b e. ( 1 ... N ) ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) )
80 7 oveq1d 
 |-  ( ph -> ( prod_ a e. ( 0 ..^ T ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) x. sum_ b e. ( 1 ... N ) ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) = ( sum_ m e. ( 0 ... ( T x. N ) ) sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. sum_ b e. ( 1 ... N ) ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) )
81 fzfid 
 |-  ( ph -> ( 0 ... ( T x. N ) ) e. Fin )
82 40 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> ( 1 ... N ) C_ NN )
83 fz0ssnn0 
 |-  ( 0 ... ( T x. N ) ) C_ NN0
84 simpr 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> m e. ( 0 ... ( T x. N ) ) )
85 83 84 sseldi 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> m e. NN0 )
86 85 nn0zd 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> m e. ZZ )
87 5 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> T e. NN0 )
88 58 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> ( 1 ... N ) e. Fin )
89 82 86 87 88 reprfi 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> ( ( 1 ... N ) ( repr ` T ) m ) e. Fin )
90 15 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( 0 ..^ T ) e. Fin )
91 1 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> N e. NN0 )
92 91 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> N e. NN0 )
93 2 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> S e. NN0 )
94 3 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> Z e. CC )
95 4 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
96 37 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( 0 ..^ T ) C_ ( 0 ..^ S ) )
97 96 sselda 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> a e. ( 0 ..^ S ) )
98 40 a1i 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> ( 1 ... N ) C_ NN )
99 86 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> m e. ZZ )
100 87 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> T e. NN0 )
101 simplr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> d e. ( ( 1 ... N ) ( repr ` T ) m ) )
102 98 99 100 101 reprf 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> d : ( 0 ..^ T ) --> ( 1 ... N ) )
103 simpr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> a e. ( 0 ..^ T ) )
104 102 103 ffvelrnd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> ( d ` a ) e. ( 1 ... N ) )
105 40 104 sseldi 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> ( d ` a ) e. NN )
106 92 93 94 95 97 105 breprexplemb 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> ( ( L ` a ) ` ( d ` a ) ) e. CC )
107 90 106 fprodcl 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) e. CC )
108 3 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> Z e. CC )
109 85 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> m e. NN0 )
110 108 109 expcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( Z ^ m ) e. CC )
111 107 110 mulcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) e. CC )
112 89 111 fsumcl 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) e. CC )
113 81 58 112 77 fsum2mul 
 |-  ( ph -> sum_ m e. ( 0 ... ( T x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) = ( sum_ m e. ( 0 ... ( T x. N ) ) sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. sum_ b e. ( 1 ... N ) ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) )
114 40 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( 1 ... N ) C_ NN )
115 fzssz 
 |-  ( 0 ... ( ( T + 1 ) x. N ) ) C_ ZZ
116 simpr 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> m e. ( 0 ... ( ( T + 1 ) x. N ) ) )
117 115 116 sseldi 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> m e. ZZ )
118 117 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> m e. ZZ )
119 fzssz 
 |-  ( 1 ... N ) C_ ZZ
120 simpr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> b e. ( 1 ... N ) )
121 119 120 sseldi 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> b e. ZZ )
122 118 121 zsubcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( m - b ) e. ZZ )
123 5 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> T e. NN0 )
124 123 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> T e. NN0 )
125 58 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( 1 ... N ) e. Fin )
126 125 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( 1 ... N ) e. Fin )
127 114 122 124 126 reprfi 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) e. Fin )
128 74 adantlr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( L ` T ) ` b ) e. CC )
129 3 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> Z e. CC )
130 fz0ssnn0 
 |-  ( 0 ... ( ( T + 1 ) x. N ) ) C_ NN0
131 130 116 sseldi 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> m e. NN0 )
132 129 131 expcld 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( Z ^ m ) e. CC )
133 132 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( Z ^ m ) e. CC )
134 128 133 mulcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) e. CC )
135 15 a1i 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) -> ( 0 ..^ T ) e. Fin )
136 1 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> N e. NN0 )
137 136 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> N e. NN0 )
138 137 ad2antrr 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> N e. NN0 )
139 2 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> S e. NN0 )
140 129 ad3antrrr 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> Z e. CC )
141 4 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
142 38 ad5ant15 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> a e. ( 0 ..^ S ) )
143 40 a1i 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> ( 1 ... N ) C_ NN )
144 122 ad2antrr 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> ( m - b ) e. ZZ )
145 124 ad2antrr 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> T e. NN0 )
146 simplr 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) )
147 143 144 145 146 reprf 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> d : ( 0 ..^ T ) --> ( 1 ... N ) )
148 simpr 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> a e. ( 0 ..^ T ) )
149 147 148 ffvelrnd 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> ( d ` a ) e. ( 1 ... N ) )
150 40 149 sseldi 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> ( d ` a ) e. NN )
151 138 139 140 141 142 150 breprexplemb 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) /\ a e. ( 0 ..^ T ) ) -> ( ( L ` a ) ` ( d ` a ) ) e. CC )
152 135 151 fprodcl 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) -> prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) e. CC )
153 127 134 152 fsummulc1 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
154 153 sumeq2dv 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) = sum_ b e. ( 1 ... N ) sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
155 elfzle2 
 |-  ( m e. ( 0 ... ( ( T + 1 ) x. N ) ) -> m <_ ( ( T + 1 ) x. N ) )
156 155 adantl 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> m <_ ( ( T + 1 ) x. N ) )
157 136 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> N e. NN0 )
158 2 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> S e. NN0 )
159 129 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> Z e. CC )
160 4 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
161 25 peano2zd 
 |-  ( ph -> ( T + 1 ) e. ZZ )
162 eluz 
 |-  ( ( ( T + 1 ) e. ZZ /\ S e. ZZ ) -> ( S e. ( ZZ>= ` ( T + 1 ) ) <-> ( T + 1 ) <_ S ) )
163 162 biimpar 
 |-  ( ( ( ( T + 1 ) e. ZZ /\ S e. ZZ ) /\ ( T + 1 ) <_ S ) -> S e. ( ZZ>= ` ( T + 1 ) ) )
164 161 26 6 163 syl21anc 
 |-  ( ph -> S e. ( ZZ>= ` ( T + 1 ) ) )
165 fzoss2 
 |-  ( S e. ( ZZ>= ` ( T + 1 ) ) -> ( 0 ..^ ( T + 1 ) ) C_ ( 0 ..^ S ) )
166 164 165 syl 
 |-  ( ph -> ( 0 ..^ ( T + 1 ) ) C_ ( 0 ..^ S ) )
167 166 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> ( 0 ..^ ( T + 1 ) ) C_ ( 0 ..^ S ) )
168 simplr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> x e. ( 0 ..^ ( T + 1 ) ) )
169 167 168 sseldd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> x e. ( 0 ..^ S ) )
170 simpr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> y e. NN )
171 157 158 159 160 169 170 breprexplemb 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> ( ( L ` x ) ` y ) e. CC )
172 136 123 131 156 171 breprexplema 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) = sum_ b e. ( 1 ... N ) sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) )
173 172 oveq1d 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) = ( sum_ b e. ( 1 ... N ) sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ m ) ) )
174 128 adantr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) -> ( ( L ` T ) ` b ) e. CC )
175 152 174 mulcld 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) -> ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) e. CC )
176 127 175 fsumcl 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) e. CC )
177 125 132 176 fsummulc1 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( sum_ b e. ( 1 ... N ) sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ m ) ) = sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ m ) ) )
178 127 133 175 fsummulc1 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ m ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ m ) ) )
179 133 adantr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) -> ( Z ^ m ) e. CC )
180 152 174 179 mulassd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ) -> ( ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
181 180 sumeq2dv 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ m ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
182 178 181 eqtrd 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ m ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
183 182 sumeq2dv 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ m ) ) = sum_ b e. ( 1 ... N ) sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
184 173 177 183 3eqtrd 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) = sum_ b e. ( 1 ... N ) sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
185 40 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( 1 ... N ) C_ NN )
186 1nn0 
 |-  1 e. NN0
187 186 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> 1 e. NN0 )
188 123 187 nn0addcld 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( T + 1 ) e. NN0 )
189 185 117 188 125 reprfi 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) e. Fin )
190 fzofi 
 |-  ( 0 ..^ ( T + 1 ) ) e. Fin
191 190 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) -> ( 0 ..^ ( T + 1 ) ) e. Fin )
192 136 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> N e. NN0 )
193 2 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> S e. NN0 )
194 129 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> Z e. CC )
195 4 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
196 166 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) -> ( 0 ..^ ( T + 1 ) ) C_ ( 0 ..^ S ) )
197 196 sselda 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> a e. ( 0 ..^ S ) )
198 40 a1i 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> ( 1 ... N ) C_ NN )
199 117 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> m e. ZZ )
200 188 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> ( T + 1 ) e. NN0 )
201 simplr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) )
202 198 199 200 201 reprf 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> d : ( 0 ..^ ( T + 1 ) ) --> ( 1 ... N ) )
203 simpr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> a e. ( 0 ..^ ( T + 1 ) ) )
204 202 203 ffvelrnd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> ( d ` a ) e. ( 1 ... N ) )
205 40 204 sseldi 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> ( d ` a ) e. NN )
206 192 193 194 195 197 205 breprexplemb 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) /\ a e. ( 0 ..^ ( T + 1 ) ) ) -> ( ( L ` a ) ` ( d ` a ) ) e. CC )
207 191 206 fprodcl 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) -> prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) e. CC )
208 189 132 207 fsummulc1 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) )
209 154 184 208 3eqtr2rd 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) = sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
210 209 sumeq2dv 
 |-  ( ph -> sum_ m e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) = sum_ m e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
211 oveq1 
 |-  ( n = m -> ( n - b ) = ( m - b ) )
212 211 oveq2d 
 |-  ( n = m -> ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) = ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) )
213 212 sumeq1d 
 |-  ( n = m -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) )
214 oveq2 
 |-  ( n = m -> ( Z ^ n ) = ( Z ^ m ) )
215 214 oveq2d 
 |-  ( n = m -> ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) = ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) )
216 213 215 oveq12d 
 |-  ( n = m -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) ) = ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
217 216 adantr 
 |-  ( ( n = m /\ b e. ( 1 ... N ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) ) = ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
218 217 sumeq2dv 
 |-  ( n = m -> sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) ) = sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) ) )
219 218 cbvsumv 
 |-  sum_ n e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) ) = sum_ m e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) )
220 210 219 eqtr4di 
 |-  ( ph -> sum_ m e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) = sum_ n e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) ) )
221 5 1 nn0mulcld 
 |-  ( ph -> ( T x. N ) e. NN0 )
222 oveq2 
 |-  ( m = ( n - b ) -> ( ( 1 ... N ) ( repr ` T ) m ) = ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) )
223 222 sumeq1d 
 |-  ( m = ( n - b ) -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) )
224 oveq1 
 |-  ( m = ( n - b ) -> ( m + b ) = ( ( n - b ) + b ) )
225 224 oveq2d 
 |-  ( m = ( n - b ) -> ( Z ^ ( m + b ) ) = ( Z ^ ( ( n - b ) + b ) ) )
226 225 oveq2d 
 |-  ( m = ( n - b ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) = ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) )
227 223 226 oveq12d 
 |-  ( m = ( n - b ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) = ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) )
228 40 a1i 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( 1 ... N ) C_ NN )
229 uzssz 
 |-  ( ZZ>= ` -u b ) C_ ZZ
230 simp2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> m e. ( ZZ>= ` -u b ) )
231 229 230 sseldi 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> m e. ZZ )
232 5 3ad2ant1 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> T e. NN0 )
233 58 3ad2ant1 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( 1 ... N ) e. Fin )
234 228 231 232 233 reprfi 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( ( 1 ... N ) ( repr ` T ) m ) e. Fin )
235 15 a1i 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( 0 ..^ T ) e. Fin )
236 59 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> N e. NN0 )
237 236 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> N e. NN0 )
238 60 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> S e. NN0 )
239 238 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> S e. NN0 )
240 61 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> Z e. CC )
241 240 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> Z e. CC )
242 62 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
243 242 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
244 37 3ad2ant1 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( 0 ..^ T ) C_ ( 0 ..^ S ) )
245 244 adantr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( 0 ..^ T ) C_ ( 0 ..^ S ) )
246 245 sselda 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> a e. ( 0 ..^ S ) )
247 40 a1i 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( 1 ... N ) C_ NN )
248 231 adantr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> m e. ZZ )
249 232 adantr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> T e. NN0 )
250 simpr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> d e. ( ( 1 ... N ) ( repr ` T ) m ) )
251 247 248 249 250 reprf 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> d : ( 0 ..^ T ) --> ( 1 ... N ) )
252 251 adantr 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> d : ( 0 ..^ T ) --> ( 1 ... N ) )
253 simpr 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> a e. ( 0 ..^ T ) )
254 252 253 ffvelrnd 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> ( d ` a ) e. ( 1 ... N ) )
255 40 254 sseldi 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> ( d ` a ) e. NN )
256 237 239 241 243 246 255 breprexplemb 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> ( ( L ` a ) ` ( d ` a ) ) e. CC )
257 235 256 fprodcl 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) e. CC )
258 234 257 fsumcl 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) e. CC )
259 71 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> T e. ( 0 ..^ S ) )
260 73 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> b e. NN )
261 236 238 240 242 259 260 breprexplemb 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( ( L ` T ) ` b ) e. CC )
262 231 zcnd 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> m e. CC )
263 simp3 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> b e. ( 1 ... N ) )
264 119 263 sseldi 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> b e. ZZ )
265 264 zcnd 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> b e. CC )
266 262 265 subnegd 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( m - -u b ) = ( m + b ) )
267 264 znegcld 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> -u b e. ZZ )
268 eluzle 
 |-  ( m e. ( ZZ>= ` -u b ) -> -u b <_ m )
269 230 268 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> -u b <_ m )
270 znn0sub 
 |-  ( ( -u b e. ZZ /\ m e. ZZ ) -> ( -u b <_ m <-> ( m - -u b ) e. NN0 ) )
271 270 biimpa 
 |-  ( ( ( -u b e. ZZ /\ m e. ZZ ) /\ -u b <_ m ) -> ( m - -u b ) e. NN0 )
272 267 231 269 271 syl21anc 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( m - -u b ) e. NN0 )
273 266 272 eqeltrrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( m + b ) e. NN0 )
274 240 273 expcld 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( Z ^ ( m + b ) ) e. CC )
275 261 274 mulcld 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) e. CC )
276 258 275 mulcld 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) e. CC )
277 59 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> N e. NN0 )
278 ssidd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( 1 ... N ) C_ ( 1 ... N ) )
279 fzssz 
 |-  ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) C_ ZZ
280 simpr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) )
281 279 280 sseldi 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> n e. ZZ )
282 simplr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> b e. ( 1 ... N ) )
283 119 282 sseldi 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> b e. ZZ )
284 281 283 zsubcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( n - b ) e. ZZ )
285 5 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> T e. NN0 )
286 27 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> T e. RR )
287 277 nn0red 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> N e. RR )
288 286 287 remulcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( T x. N ) e. RR )
289 283 zred 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> b e. RR )
290 221 adantr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( T x. N ) e. NN0 )
291 290 75 nn0addcld 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( T x. N ) + b ) e. NN0 )
292 186 a1i 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> 1 e. NN0 )
293 291 292 nn0addcld 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( ( T x. N ) + b ) + 1 ) e. NN0 )
294 fz2ssnn0 
 |-  ( ( ( ( T x. N ) + b ) + 1 ) e. NN0 -> ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) C_ NN0 )
295 293 294 syl 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) C_ NN0 )
296 295 sselda 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> n e. NN0 )
297 296 nn0red 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> n e. RR )
298 25 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> T e. ZZ )
299 277 nn0zd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> N e. ZZ )
300 298 299 zmulcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( T x. N ) e. ZZ )
301 300 283 zaddcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( T x. N ) + b ) e. ZZ )
302 elfzle1 
 |-  ( n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) -> ( ( ( T x. N ) + b ) + 1 ) <_ n )
303 280 302 syl 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( ( T x. N ) + b ) + 1 ) <_ n )
304 zltp1le 
 |-  ( ( ( ( T x. N ) + b ) e. ZZ /\ n e. ZZ ) -> ( ( ( T x. N ) + b ) < n <-> ( ( ( T x. N ) + b ) + 1 ) <_ n ) )
305 304 biimpar 
 |-  ( ( ( ( ( T x. N ) + b ) e. ZZ /\ n e. ZZ ) /\ ( ( ( T x. N ) + b ) + 1 ) <_ n ) -> ( ( T x. N ) + b ) < n )
306 301 281 303 305 syl21anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( T x. N ) + b ) < n )
307 ltaddsub 
 |-  ( ( ( T x. N ) e. RR /\ b e. RR /\ n e. RR ) -> ( ( ( T x. N ) + b ) < n <-> ( T x. N ) < ( n - b ) ) )
308 307 biimpa 
 |-  ( ( ( ( T x. N ) e. RR /\ b e. RR /\ n e. RR ) /\ ( ( T x. N ) + b ) < n ) -> ( T x. N ) < ( n - b ) )
309 288 289 297 306 308 syl31anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( T x. N ) < ( n - b ) )
310 277 278 284 285 309 reprgt 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) = (/) )
311 310 sumeq1d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) = sum_ d e. (/) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) )
312 sum0 
 |-  sum_ d e. (/) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) = 0
313 311 312 eqtrdi 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) = 0 )
314 313 oveq1d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) = ( 0 x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) )
315 74 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( L ` T ) ` b ) e. CC )
316 61 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> Z e. CC )
317 281 zcnd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> n e. CC )
318 283 zcnd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> b e. CC )
319 317 318 npcand 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( n - b ) + b ) = n )
320 319 296 eqeltrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( n - b ) + b ) e. NN0 )
321 316 320 expcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( Z ^ ( ( n - b ) + b ) ) e. CC )
322 315 321 mulcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) e. CC )
323 322 mul02d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( 0 x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) = 0 )
324 314 323 eqtrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) = 0 )
325 40 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( 1 ... N ) C_ NN )
326 fzossfz 
 |-  ( 0 ..^ b ) C_ ( 0 ... b )
327 fzssz 
 |-  ( 0 ... b ) C_ ZZ
328 326 327 sstri 
 |-  ( 0 ..^ b ) C_ ZZ
329 simpr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n e. ( 0 ..^ b ) )
330 328 329 sseldi 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n e. ZZ )
331 simplr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> b e. ( 1 ... N ) )
332 119 331 sseldi 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> b e. ZZ )
333 330 332 zsubcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( n - b ) e. ZZ )
334 5 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> T e. NN0 )
335 333 zred 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( n - b ) e. RR )
336 0red 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> 0 e. RR )
337 27 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> T e. RR )
338 elfzolt2 
 |-  ( n e. ( 0 ..^ b ) -> n < b )
339 338 adantl 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n < b )
340 330 zred 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n e. RR )
341 332 zred 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> b e. RR )
342 340 341 sublt0d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( n - b ) < 0 <-> n < b ) )
343 339 342 mpbird 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( n - b ) < 0 )
344 63 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> 0 <_ T )
345 335 336 337 343 344 ltletrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( n - b ) < T )
346 325 333 334 345 reprlt 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) = (/) )
347 346 sumeq1d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) = sum_ d e. (/) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) )
348 347 312 eqtrdi 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) = 0 )
349 348 oveq1d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) = ( 0 x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) )
350 74 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( L ` T ) ` b ) e. CC )
351 61 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> Z e. CC )
352 340 recnd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n e. CC )
353 341 recnd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> b e. CC )
354 352 353 npcand 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( n - b ) + b ) = n )
355 fzo0ssnn0 
 |-  ( 0 ..^ b ) C_ NN0
356 355 329 sseldi 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n e. NN0 )
357 354 356 eqeltrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( n - b ) + b ) e. NN0 )
358 351 357 expcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( Z ^ ( ( n - b ) + b ) ) e. CC )
359 350 358 mulcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) e. CC )
360 359 mul02d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( 0 x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) = 0 )
361 349 360 eqtrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) = 0 )
362 221 1 227 276 324 361 fsum2dsub 
 |-  ( ph -> sum_ m e. ( 0 ... ( T x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) = sum_ n e. ( 0 ... ( ( T x. N ) + N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) )
363 nn0sscn 
 |-  NN0 C_ CC
364 363 5 sseldi 
 |-  ( ph -> T e. CC )
365 363 1 sseldi 
 |-  ( ph -> N e. CC )
366 364 365 adddirp1d 
 |-  ( ph -> ( ( T + 1 ) x. N ) = ( ( T x. N ) + N ) )
367 366 oveq2d 
 |-  ( ph -> ( 0 ... ( ( T + 1 ) x. N ) ) = ( 0 ... ( ( T x. N ) + N ) ) )
368 130 363 sstri 
 |-  ( 0 ... ( ( T + 1 ) x. N ) ) C_ CC
369 simplr 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> n e. ( 0 ... ( ( T + 1 ) x. N ) ) )
370 368 369 sseldi 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> n e. CC )
371 45 363 sstri 
 |-  ( 1 ... N ) C_ CC
372 simpr 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> b e. ( 1 ... N ) )
373 371 372 sseldi 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> b e. CC )
374 370 373 npcand 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( n - b ) + b ) = n )
375 374 eqcomd 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> n = ( ( n - b ) + b ) )
376 375 oveq2d 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( Z ^ n ) = ( Z ^ ( ( n - b ) + b ) ) )
377 376 oveq2d 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) = ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) )
378 377 oveq2d 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) ) = ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) )
379 378 sumeq2dv 
 |-  ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) ) = sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) )
380 367 379 sumeq12dv 
 |-  ( ph -> sum_ n e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) ) = sum_ n e. ( 0 ... ( ( T x. N ) + N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) )
381 362 380 eqtr4d 
 |-  ( ph -> sum_ m e. ( 0 ... ( T x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) = sum_ n e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) ) )
382 107 adantlr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) e. CC )
383 110 adantlr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( Z ^ m ) e. CC )
384 77 adantlr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) e. CC )
385 384 adantr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) e. CC )
386 382 383 385 mulassd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) = ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( Z ^ m ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) ) )
387 74 ad4ant13 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( L ` T ) ` b ) e. CC )
388 76 ad4ant13 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( Z ^ b ) e. CC )
389 383 387 388 mulassd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( ( Z ^ m ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ b ) ) = ( ( Z ^ m ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) )
390 387 383 388 mulassd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) x. ( Z ^ b ) ) = ( ( ( L ` T ) ` b ) x. ( ( Z ^ m ) x. ( Z ^ b ) ) ) )
391 383 387 mulcomd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( Z ^ m ) x. ( ( L ` T ) ` b ) ) = ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) )
392 391 oveq1d 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( ( Z ^ m ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ b ) ) = ( ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) x. ( Z ^ b ) ) )
393 108 adantlr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> Z e. CC )
394 75 ad4ant13 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> b e. NN0 )
395 109 adantlr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> m e. NN0 )
396 393 394 395 expaddd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( Z ^ ( m + b ) ) = ( ( Z ^ m ) x. ( Z ^ b ) ) )
397 396 oveq2d 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) = ( ( ( L ` T ) ` b ) x. ( ( Z ^ m ) x. ( Z ^ b ) ) ) )
398 390 392 397 3eqtr4d 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( ( Z ^ m ) x. ( ( L ` T ) ` b ) ) x. ( Z ^ b ) ) = ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) )
399 389 398 eqtr3d 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( Z ^ m ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) = ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) )
400 399 oveq2d 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( Z ^ m ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) ) = ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) )
401 386 400 eqtrd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) = ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) )
402 401 sumeq2dv 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) )
403 89 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( 1 ... N ) ( repr ` T ) m ) e. Fin )
404 111 adantlr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) e. CC )
405 403 384 404 fsummulc1 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) )
406 74 adantlr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( L ` T ) ` b ) e. CC )
407 61 adantlr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> Z e. CC )
408 85 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> m e. NN0 )
409 75 adantlr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> b e. NN0 )
410 408 409 nn0addcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( m + b ) e. NN0 )
411 407 410 expcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( Z ^ ( m + b ) ) e. CC )
412 406 411 mulcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) e. CC )
413 403 412 382 fsummulc1 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) )
414 402 405 413 3eqtr4rd 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) = ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) )
415 414 sumeq2dv 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) = sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) )
416 415 sumeq2dv 
 |-  ( ph -> sum_ m e. ( 0 ... ( T x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) ) = sum_ m e. ( 0 ... ( T x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) )
417 220 381 416 3eqtr2rd 
 |-  ( ph -> sum_ m e. ( 0 ... ( T x. N ) ) sum_ b e. ( 1 ... N ) ( sum_ d e. ( ( 1 ... N ) ( repr ` T ) m ) ( prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) x. ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) = sum_ m e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) )
418 80 113 417 3eqtr2d 
 |-  ( ph -> ( prod_ a e. ( 0 ..^ T ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) x. sum_ b e. ( 1 ... N ) ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) ) = sum_ m e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) )
419 12 79 418 3eqtrd 
 |-  ( ph -> prod_ a e. ( 0 ..^ ( T + 1 ) ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) )