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 simpr 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> m e. ( 0 ... ( T x. N ) ) )
84 83 elfzelzd 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> m e. ZZ )
85 5 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> T e. NN0 )
86 58 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> ( 1 ... N ) e. Fin )
87 82 84 85 86 reprfi 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> ( ( 1 ... N ) ( repr ` T ) m ) e. Fin )
88 15 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( 0 ..^ T ) e. Fin )
89 1 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> N e. NN0 )
90 89 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> N e. NN0 )
91 2 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> S e. NN0 )
92 3 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> Z e. CC )
93 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 ) )
94 37 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( 0 ..^ T ) C_ ( 0 ..^ S ) )
95 94 sselda 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> a e. ( 0 ..^ S ) )
96 40 a1i 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> ( 1 ... N ) C_ NN )
97 84 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> m e. ZZ )
98 85 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> T e. NN0 )
99 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 ) )
100 96 97 98 99 reprf 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> d : ( 0 ..^ T ) --> ( 1 ... N ) )
101 simpr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> a e. ( 0 ..^ T ) )
102 100 101 ffvelcdmd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> ( d ` a ) e. ( 1 ... N ) )
103 40 102 sselid 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) /\ a e. ( 0 ..^ T ) ) -> ( d ` a ) e. NN )
104 90 91 92 93 95 103 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 )
105 88 104 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 )
106 3 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> Z e. CC )
107 fz0ssnn0 
 |-  ( 0 ... ( T x. N ) ) C_ NN0
108 107 83 sselid 
 |-  ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) -> m e. NN0 )
109 108 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> m e. NN0 )
110 106 109 expcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( Z ^ m ) e. CC )
111 105 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 87 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 simpr 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> m e. ( 0 ... ( ( T + 1 ) x. N ) ) )
116 115 elfzelzd 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> m e. ZZ )
117 116 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> m e. ZZ )
118 simpr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> b e. ( 1 ... N ) )
119 118 elfzelzd 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> b e. ZZ )
120 117 119 zsubcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( m - b ) e. ZZ )
121 5 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> T e. NN0 )
122 121 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> T e. NN0 )
123 58 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( 1 ... N ) e. Fin )
124 123 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( 1 ... N ) e. Fin )
125 114 120 122 124 reprfi 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) e. Fin )
126 74 adantlr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( L ` T ) ` b ) e. CC )
127 3 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> Z e. CC )
128 fz0ssnn0 
 |-  ( 0 ... ( ( T + 1 ) x. N ) ) C_ NN0
129 128 115 sselid 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> m e. NN0 )
130 127 129 expcld 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( Z ^ m ) e. CC )
131 130 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( Z ^ m ) e. CC )
132 126 131 mulcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) e. CC )
133 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 )
134 1 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> N e. NN0 )
135 134 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> N e. NN0 )
136 135 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 )
137 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 )
138 127 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 )
139 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 ) )
140 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 ) )
141 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 )
142 120 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 )
143 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 ) ) -> T e. NN0 )
144 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 ) ) )
145 141 142 143 144 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 ) )
146 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 ) )
147 145 146 ffvelcdmd 
 |-  ( ( ( ( ( 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 ) )
148 40 147 sselid 
 |-  ( ( ( ( ( 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 )
149 136 137 138 139 140 148 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 )
150 133 149 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 )
151 125 132 150 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 ) ) ) )
152 151 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 ) ) ) )
153 elfzle2 
 |-  ( m e. ( 0 ... ( ( T + 1 ) x. N ) ) -> m <_ ( ( T + 1 ) x. N ) )
154 153 adantl 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> m <_ ( ( T + 1 ) x. N ) )
155 134 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> N e. NN0 )
156 2 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> S e. NN0 )
157 127 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> Z e. CC )
158 4 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
159 25 peano2zd 
 |-  ( ph -> ( T + 1 ) e. ZZ )
160 eluz 
 |-  ( ( ( T + 1 ) e. ZZ /\ S e. ZZ ) -> ( S e. ( ZZ>= ` ( T + 1 ) ) <-> ( T + 1 ) <_ S ) )
161 160 biimpar 
 |-  ( ( ( ( T + 1 ) e. ZZ /\ S e. ZZ ) /\ ( T + 1 ) <_ S ) -> S e. ( ZZ>= ` ( T + 1 ) ) )
162 159 26 6 161 syl21anc 
 |-  ( ph -> S e. ( ZZ>= ` ( T + 1 ) ) )
163 fzoss2 
 |-  ( S e. ( ZZ>= ` ( T + 1 ) ) -> ( 0 ..^ ( T + 1 ) ) C_ ( 0 ..^ S ) )
164 162 163 syl 
 |-  ( ph -> ( 0 ..^ ( T + 1 ) ) C_ ( 0 ..^ S ) )
165 164 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> ( 0 ..^ ( T + 1 ) ) C_ ( 0 ..^ S ) )
166 simplr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> x e. ( 0 ..^ ( T + 1 ) ) )
167 165 166 sseldd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> x e. ( 0 ..^ S ) )
168 simpr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> y e. NN )
169 155 156 157 158 167 168 breprexplemb 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ x e. ( 0 ..^ ( T + 1 ) ) ) /\ y e. NN ) -> ( ( L ` x ) ` y ) e. CC )
170 134 121 129 154 169 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 ) ) )
171 170 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 ) ) )
172 126 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 )
173 150 172 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 )
174 125 173 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 )
175 123 130 174 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 ) ) )
176 125 131 173 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 ) ) )
177 131 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 )
178 150 172 177 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 ) ) ) )
179 178 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 ) ) ) )
180 176 179 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 ) ) ) )
181 180 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 ) ) ) )
182 171 175 181 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 ) ) ) )
183 40 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( 1 ... N ) C_ NN )
184 1nn0 
 |-  1 e. NN0
185 184 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> 1 e. NN0 )
186 121 185 nn0addcld 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( T + 1 ) e. NN0 )
187 183 116 186 123 reprfi 
 |-  ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) -> ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) e. Fin )
188 fzofi 
 |-  ( 0 ..^ ( T + 1 ) ) e. Fin
189 188 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) -> ( 0 ..^ ( T + 1 ) ) e. Fin )
190 134 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 )
191 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 )
192 127 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 )
193 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 ) )
194 164 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ d e. ( ( 1 ... N ) ( repr ` ( T + 1 ) ) m ) ) -> ( 0 ..^ ( T + 1 ) ) C_ ( 0 ..^ S ) )
195 194 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 ) )
196 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 )
197 116 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 )
198 186 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 )
199 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 ) )
200 196 197 198 199 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 ) )
201 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 ) ) )
202 200 201 ffvelcdmd 
 |-  ( ( ( ( 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 ) )
203 40 202 sselid 
 |-  ( ( ( ( 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 )
204 190 191 192 193 195 203 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 )
205 189 204 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 )
206 187 130 205 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 ) ) )
207 152 182 206 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 ) ) ) )
208 207 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 ) ) ) )
209 oveq1 
 |-  ( n = m -> ( n - b ) = ( m - b ) )
210 209 oveq2d 
 |-  ( n = m -> ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) = ( ( 1 ... N ) ( repr ` T ) ( m - b ) ) )
211 210 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 ) ) )
212 oveq2 
 |-  ( n = m -> ( Z ^ n ) = ( Z ^ m ) )
213 212 oveq2d 
 |-  ( n = m -> ( ( ( L ` T ) ` b ) x. ( Z ^ n ) ) = ( ( ( L ` T ) ` b ) x. ( Z ^ m ) ) )
214 211 213 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 ) ) ) )
215 214 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 ) ) ) )
216 215 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 ) ) ) )
217 216 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 ) ) )
218 208 217 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 ) ) ) )
219 5 1 nn0mulcld 
 |-  ( ph -> ( T x. N ) e. NN0 )
220 oveq2 
 |-  ( m = ( n - b ) -> ( ( 1 ... N ) ( repr ` T ) m ) = ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) )
221 220 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 ) ) )
222 oveq1 
 |-  ( m = ( n - b ) -> ( m + b ) = ( ( n - b ) + b ) )
223 222 oveq2d 
 |-  ( m = ( n - b ) -> ( Z ^ ( m + b ) ) = ( Z ^ ( ( n - b ) + b ) ) )
224 223 oveq2d 
 |-  ( m = ( n - b ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) = ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) )
225 221 224 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 ) ) ) ) )
226 40 a1i 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( 1 ... N ) C_ NN )
227 uzssz 
 |-  ( ZZ>= ` -u b ) C_ ZZ
228 simp2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> m e. ( ZZ>= ` -u b ) )
229 227 228 sselid 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> m e. ZZ )
230 5 3ad2ant1 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> T e. NN0 )
231 58 3ad2ant1 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( 1 ... N ) e. Fin )
232 226 229 230 231 reprfi 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( ( 1 ... N ) ( repr ` T ) m ) e. Fin )
233 15 a1i 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( 0 ..^ T ) e. Fin )
234 59 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> N e. NN0 )
235 234 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 )
236 60 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> S 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 ) ) -> S e. NN0 )
238 61 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> Z e. CC )
239 238 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 )
240 62 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
241 240 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 ) )
242 37 3ad2ant1 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( 0 ..^ T ) C_ ( 0 ..^ S ) )
243 242 adantr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( 0 ..^ T ) C_ ( 0 ..^ S ) )
244 243 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 ) )
245 40 a1i 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( 1 ... N ) C_ NN )
246 229 adantr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> m e. ZZ )
247 230 adantr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> T e. NN0 )
248 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 ) )
249 245 246 247 248 reprf 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> d : ( 0 ..^ T ) --> ( 1 ... N ) )
250 249 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 ) )
251 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 ) )
252 250 251 ffvelcdmd 
 |-  ( ( ( ( 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 ) )
253 40 252 sselid 
 |-  ( ( ( ( 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 )
254 235 237 239 241 244 253 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 )
255 233 254 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 )
256 232 255 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 )
257 71 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> T e. ( 0 ..^ S ) )
258 73 3adant2 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> b e. NN )
259 234 236 238 240 257 258 breprexplemb 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( ( L ` T ) ` b ) e. CC )
260 229 zcnd 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> m e. CC )
261 simp3 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> b e. ( 1 ... N ) )
262 261 elfzelzd 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> b e. ZZ )
263 262 zcnd 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> b e. CC )
264 260 263 subnegd 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( m - -u b ) = ( m + b ) )
265 262 znegcld 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> -u b e. ZZ )
266 eluzle 
 |-  ( m e. ( ZZ>= ` -u b ) -> -u b <_ m )
267 228 266 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> -u b <_ m )
268 znn0sub 
 |-  ( ( -u b e. ZZ /\ m e. ZZ ) -> ( -u b <_ m <-> ( m - -u b ) e. NN0 ) )
269 268 biimpa 
 |-  ( ( ( -u b e. ZZ /\ m e. ZZ ) /\ -u b <_ m ) -> ( m - -u b ) e. NN0 )
270 265 229 267 269 syl21anc 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( m - -u b ) e. NN0 )
271 264 270 eqeltrrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( m + b ) e. NN0 )
272 238 271 expcld 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( Z ^ ( m + b ) ) e. CC )
273 259 272 mulcld 
 |-  ( ( ph /\ m e. ( ZZ>= ` -u b ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) e. CC )
274 256 273 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 )
275 59 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> N e. NN0 )
276 ssidd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( 1 ... N ) C_ ( 1 ... N ) )
277 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 ) ) )
278 277 elfzelzd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> n e. ZZ )
279 simplr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> b e. ( 1 ... N ) )
280 279 elfzelzd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> b e. ZZ )
281 278 280 zsubcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( n - b ) e. ZZ )
282 5 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> T e. NN0 )
283 27 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> T e. RR )
284 275 nn0red 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> N e. RR )
285 283 284 remulcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( T x. N ) e. RR )
286 280 zred 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> b e. RR )
287 219 adantr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( T x. N ) e. NN0 )
288 287 75 nn0addcld 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( T x. N ) + b ) e. NN0 )
289 184 a1i 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> 1 e. NN0 )
290 288 289 nn0addcld 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( ( T x. N ) + b ) + 1 ) e. NN0 )
291 fz2ssnn0 
 |-  ( ( ( ( T x. N ) + b ) + 1 ) e. NN0 -> ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) C_ NN0 )
292 290 291 syl 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) C_ NN0 )
293 292 sselda 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> n e. NN0 )
294 293 nn0red 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> n e. RR )
295 25 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> T e. ZZ )
296 275 nn0zd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> N e. ZZ )
297 295 296 zmulcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( T x. N ) e. ZZ )
298 297 280 zaddcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( T x. N ) + b ) e. ZZ )
299 elfzle1 
 |-  ( n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) -> ( ( ( T x. N ) + b ) + 1 ) <_ n )
300 277 299 syl 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( ( T x. N ) + b ) + 1 ) <_ n )
301 zltp1le 
 |-  ( ( ( ( T x. N ) + b ) e. ZZ /\ n e. ZZ ) -> ( ( ( T x. N ) + b ) < n <-> ( ( ( T x. N ) + b ) + 1 ) <_ n ) )
302 301 biimpar 
 |-  ( ( ( ( ( T x. N ) + b ) e. ZZ /\ n e. ZZ ) /\ ( ( ( T x. N ) + b ) + 1 ) <_ n ) -> ( ( T x. N ) + b ) < n )
303 298 278 300 302 syl21anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( T x. N ) + b ) < n )
304 ltaddsub 
 |-  ( ( ( T x. N ) e. RR /\ b e. RR /\ n e. RR ) -> ( ( ( T x. N ) + b ) < n <-> ( T x. N ) < ( n - b ) ) )
305 304 biimpa 
 |-  ( ( ( ( T x. N ) e. RR /\ b e. RR /\ n e. RR ) /\ ( ( T x. N ) + b ) < n ) -> ( T x. N ) < ( n - b ) )
306 285 286 294 303 305 syl31anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( T x. N ) < ( n - b ) )
307 275 276 281 282 306 reprgt 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) = (/) )
308 307 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 ) ) )
309 sum0 
 |-  sum_ d e. (/) prod_ a e. ( 0 ..^ T ) ( ( L ` a ) ` ( d ` a ) ) = 0
310 308 309 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 )
311 310 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 ) ) ) ) )
312 74 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( L ` T ) ` b ) e. CC )
313 61 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> Z e. CC )
314 278 zcnd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> n e. CC )
315 280 zcnd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> b e. CC )
316 314 315 npcand 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( n - b ) + b ) = n )
317 316 293 eqeltrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( ( n - b ) + b ) e. NN0 )
318 313 317 expcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( ( ( ( T x. N ) + b ) + 1 ) ... ( ( T x. N ) + N ) ) ) -> ( Z ^ ( ( n - b ) + b ) ) e. CC )
319 312 318 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 )
320 319 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 )
321 311 320 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 )
322 40 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( 1 ... N ) C_ NN )
323 fzossfz 
 |-  ( 0 ..^ b ) C_ ( 0 ... b )
324 fzssz 
 |-  ( 0 ... b ) C_ ZZ
325 323 324 sstri 
 |-  ( 0 ..^ b ) C_ ZZ
326 simpr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n e. ( 0 ..^ b ) )
327 325 326 sselid 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n e. ZZ )
328 simplr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> b e. ( 1 ... N ) )
329 328 elfzelzd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> b e. ZZ )
330 327 329 zsubcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( n - b ) e. ZZ )
331 5 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> T e. NN0 )
332 330 zred 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( n - b ) e. RR )
333 0red 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> 0 e. RR )
334 27 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> T e. RR )
335 elfzolt2 
 |-  ( n e. ( 0 ..^ b ) -> n < b )
336 335 adantl 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n < b )
337 327 zred 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n e. RR )
338 329 zred 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> b e. RR )
339 337 338 sublt0d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( n - b ) < 0 <-> n < b ) )
340 336 339 mpbird 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( n - b ) < 0 )
341 63 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> 0 <_ T )
342 332 333 334 340 341 ltletrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( n - b ) < T )
343 322 330 331 342 reprlt 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( 1 ... N ) ( repr ` T ) ( n - b ) ) = (/) )
344 343 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 ) ) )
345 344 309 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 )
346 345 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 ) ) ) ) )
347 74 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( L ` T ) ` b ) e. CC )
348 61 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> Z e. CC )
349 337 recnd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n e. CC )
350 338 recnd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> b e. CC )
351 349 350 npcand 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( n - b ) + b ) = n )
352 fzo0ssnn0 
 |-  ( 0 ..^ b ) C_ NN0
353 352 326 sselid 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> n e. NN0 )
354 351 353 eqeltrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( n - b ) + b ) e. NN0 )
355 348 354 expcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( Z ^ ( ( n - b ) + b ) ) e. CC )
356 347 355 mulcld 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) e. CC )
357 356 mul02d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ n e. ( 0 ..^ b ) ) -> ( 0 x. ( ( ( L ` T ) ` b ) x. ( Z ^ ( ( n - b ) + b ) ) ) ) = 0 )
358 346 357 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 )
359 219 1 225 274 321 358 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 ) ) ) ) )
360 nn0sscn 
 |-  NN0 C_ CC
361 360 5 sselid 
 |-  ( ph -> T e. CC )
362 360 1 sselid 
 |-  ( ph -> N e. CC )
363 361 362 adddirp1d 
 |-  ( ph -> ( ( T + 1 ) x. N ) = ( ( T x. N ) + N ) )
364 363 oveq2d 
 |-  ( ph -> ( 0 ... ( ( T + 1 ) x. N ) ) = ( 0 ... ( ( T x. N ) + N ) ) )
365 128 360 sstri 
 |-  ( 0 ... ( ( T + 1 ) x. N ) ) C_ CC
366 simplr 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> n e. ( 0 ... ( ( T + 1 ) x. N ) ) )
367 365 366 sselid 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> n e. CC )
368 45 360 sstri 
 |-  ( 1 ... N ) C_ CC
369 simpr 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> b e. ( 1 ... N ) )
370 368 369 sselid 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> b e. CC )
371 367 370 npcand 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( n - b ) + b ) = n )
372 371 eqcomd 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> n = ( ( n - b ) + b ) )
373 372 oveq2d 
 |-  ( ( ( ph /\ n e. ( 0 ... ( ( T + 1 ) x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( Z ^ n ) = ( Z ^ ( ( n - b ) + b ) ) )
374 373 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 ) ) ) )
375 374 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 ) ) ) ) )
376 375 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 ) ) ) ) )
377 364 376 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 ) ) ) ) )
378 359 377 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 ) ) ) )
379 105 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 )
380 110 adantlr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( Z ^ m ) e. CC )
381 77 adantlr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ b ) ) e. CC )
382 381 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 )
383 379 380 382 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 ) ) ) ) )
384 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 )
385 76 ad4ant13 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> ( Z ^ b ) e. CC )
386 380 384 385 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 ) ) ) )
387 384 380 385 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 ) ) ) )
388 380 384 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 ) ) )
389 388 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 ) ) )
390 106 adantlr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> Z e. CC )
391 75 ad4ant13 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> b e. NN0 )
392 109 adantlr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) /\ d e. ( ( 1 ... N ) ( repr ` T ) m ) ) -> m e. NN0 )
393 390 391 392 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 ) ) )
394 393 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 ) ) ) )
395 387 389 394 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 ) ) ) )
396 386 395 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 ) ) ) )
397 396 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 ) ) ) ) )
398 383 397 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 ) ) ) ) )
399 398 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 ) ) ) ) )
400 87 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( 1 ... N ) ( repr ` T ) m ) e. Fin )
401 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 )
402 400 381 401 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 ) ) ) )
403 74 adantlr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( L ` T ) ` b ) e. CC )
404 61 adantlr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> Z e. CC )
405 108 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> m e. NN0 )
406 75 adantlr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> b e. NN0 )
407 405 406 nn0addcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( m + b ) e. NN0 )
408 404 407 expcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( Z ^ ( m + b ) ) e. CC )
409 403 408 mulcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( T x. N ) ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` T ) ` b ) x. ( Z ^ ( m + b ) ) ) e. CC )
410 400 409 379 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 ) ) ) ) )
411 399 402 410 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 ) ) ) )
412 411 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 ) ) ) )
413 412 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 ) ) ) )
414 218 378 413 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 ) ) )
415 80 113 414 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 ) ) )
416 12 79 415 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 ) ) )