Metamath Proof Explorer

Theorem breprexplema

Description: Lemma for breprexp (induction step for weighted sums over representations). (Contributed by Thierry Arnoux, 7-Dec-2021)

Ref Expression
Hypotheses breprexp.n 
|- ( ph -> N e. NN0 )
breprexp.s 
|- ( ph -> S e. NN0 )
breprexplema.m 
|- ( ph -> M e. NN0 )
breprexplema.1 
|- ( ph -> M <_ ( ( S + 1 ) x. N ) )
breprexplema.l 
|- ( ( ( ph /\ x e. ( 0 ..^ ( S + 1 ) ) ) /\ y e. NN ) -> ( ( L ` x ) ` y ) e. CC )
Assertion breprexplema 
|- ( ph -> sum_ d e. ( ( 1 ... N ) ( repr ` ( S + 1 ) ) M ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) = sum_ b e. ( 1 ... N ) sum_ d e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` S ) ` b ) ) )

Proof

Step Hyp Ref Expression
1 breprexp.n 
 |-  ( ph -> N e. NN0 )
2 breprexp.s 
 |-  ( ph -> S e. NN0 )
3 breprexplema.m 
 |-  ( ph -> M e. NN0 )
4 breprexplema.1 
 |-  ( ph -> M <_ ( ( S + 1 ) x. N ) )
5 breprexplema.l 
 |-  ( ( ( ph /\ x e. ( 0 ..^ ( S + 1 ) ) ) /\ y e. NN ) -> ( ( L ` x ) ` y ) e. CC )
6 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
7 6 a1i 
 |-  ( ph -> ( 1 ... N ) C_ NN )
8 3 nn0zd 
 |-  ( ph -> M e. ZZ )
9 eqid 
 |-  ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) = ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) )
10 7 8 2 9 reprsuc 
 |-  ( ph -> ( ( 1 ... N ) ( repr ` ( S + 1 ) ) M ) = U_ b e. ( 1 ... N ) ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) )
11 10 sumeq1d 
 |-  ( ph -> sum_ d e. ( ( 1 ... N ) ( repr ` ( S + 1 ) ) M ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) = sum_ d e. U_ b e. ( 1 ... N ) ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) )
12 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
13 6 a1i 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( 1 ... N ) C_ NN )
14 8 adantr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> M e. ZZ )
15 fzssz 
 |-  ( 1 ... N ) C_ ZZ
16 simpr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> b e. ( 1 ... N ) )
17 15 16 sseldi 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> b e. ZZ )
18 14 17 zsubcld 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( M - b ) e. ZZ )
19 2 adantr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> S e. NN0 )
20 12 adantr 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( 1 ... N ) e. Fin )
21 13 18 19 20 reprfi 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) e. Fin )
22 mptfi 
 |-  ( ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) e. Fin -> ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) e. Fin )
23 21 22 syl 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) e. Fin )
24 rnfi 
 |-  ( ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) e. Fin -> ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) e. Fin )
25 23 24 syl 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) e. Fin )
26 13 18 19 reprval 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) = { c e. ( ( 1 ... N ) ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = ( M - b ) } )
27 ssrab2 
 |-  { c e. ( ( 1 ... N ) ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = ( M - b ) } C_ ( ( 1 ... N ) ^m ( 0 ..^ S ) )
28 26 27 eqsstrdi 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) C_ ( ( 1 ... N ) ^m ( 0 ..^ S ) ) )
29 12 elexd 
 |-  ( ph -> ( 1 ... N ) e. _V )
30 fzonel 
 |-  -. S e. ( 0 ..^ S )
31 30 a1i 
 |-  ( ph -> -. S e. ( 0 ..^ S ) )
32 28 29 2 31 9 actfunsnrndisj 
 |-  ( ph -> Disj_ b e. ( 1 ... N ) ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) )
33 fzofi 
 |-  ( 0 ..^ ( S + 1 ) ) e. Fin
34 33 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) -> ( 0 ..^ ( S + 1 ) ) e. Fin )
35 5 ralrimiva 
 |-  ( ( ph /\ x e. ( 0 ..^ ( S + 1 ) ) ) -> A. y e. NN ( ( L ` x ) ` y ) e. CC )
36 35 ralrimiva 
 |-  ( ph -> A. x e. ( 0 ..^ ( S + 1 ) ) A. y e. NN ( ( L ` x ) ` y ) e. CC )
37 36 ad3antrrr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> A. x e. ( 0 ..^ ( S + 1 ) ) A. y e. NN ( ( L ` x ) ` y ) e. CC )
38 simpr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> a e. ( 0 ..^ ( S + 1 ) ) )
39 nfv 
 |-  F/ v ( ph /\ b e. ( 1 ... N ) )
40 nfcv 
 |-  F/_ v d
41 nfmpt1 
 |-  F/_ v ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) )
42 41 nfrn 
 |-  F/_ v ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) )
43 40 42 nfel 
 |-  F/ v d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) )
44 39 43 nfan 
 |-  F/ v ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) )
45 6 a1i 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> ( 1 ... N ) C_ NN )
46 18 ad3antrrr 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> ( M - b ) e. ZZ )
47 19 ad3antrrr 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> S e. NN0 )
48 simplr 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) )
49 45 46 47 48 reprf 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> v : ( 0 ..^ S ) --> ( 1 ... N ) )
50 16 ad3antrrr 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> b e. ( 1 ... N ) )
51 47 50 fsnd 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> { <. S , b >. } : { S } --> ( 1 ... N ) )
52 fzodisjsn 
 |-  ( ( 0 ..^ S ) i^i { S } ) = (/)
53 52 a1i 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> ( ( 0 ..^ S ) i^i { S } ) = (/) )
54 fun2 
 |-  ( ( ( v : ( 0 ..^ S ) --> ( 1 ... N ) /\ { <. S , b >. } : { S } --> ( 1 ... N ) ) /\ ( ( 0 ..^ S ) i^i { S } ) = (/) ) -> ( v u. { <. S , b >. } ) : ( ( 0 ..^ S ) u. { S } ) --> ( 1 ... N ) )
55 49 51 53 54 syl21anc 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> ( v u. { <. S , b >. } ) : ( ( 0 ..^ S ) u. { S } ) --> ( 1 ... N ) )
56 simpr 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> d = ( v u. { <. S , b >. } ) )
57 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
58 2 57 eleqtrdi 
 |-  ( ph -> S e. ( ZZ>= ` 0 ) )
59 fzosplitsn 
 |-  ( S e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
60 58 59 syl 
 |-  ( ph -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
61 60 ad4antr 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
62 56 61 feq12d 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> ( d : ( 0 ..^ ( S + 1 ) ) --> ( 1 ... N ) <-> ( v u. { <. S , b >. } ) : ( ( 0 ..^ S ) u. { S } ) --> ( 1 ... N ) ) )
63 55 62 mpbird 
 |-  ( ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ d = ( v u. { <. S , b >. } ) ) -> d : ( 0 ..^ ( S + 1 ) ) --> ( 1 ... N ) )
64 simpr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) -> d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) )
65 vex 
 |-  v e. _V
66 snex 
 |-  { <. S , b >. } e. _V
67 65 66 unex 
 |-  ( v u. { <. S , b >. } ) e. _V
68 9 67 elrnmpti 
 |-  ( d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) <-> E. v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) d = ( v u. { <. S , b >. } ) )
69 64 68 sylib 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) -> E. v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) d = ( v u. { <. S , b >. } ) )
70 44 63 69 r19.29af 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) -> d : ( 0 ..^ ( S + 1 ) ) --> ( 1 ... N ) )
71 70 adantr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> d : ( 0 ..^ ( S + 1 ) ) --> ( 1 ... N ) )
72 71 38 ffvelrnd 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> ( d ` a ) e. ( 1 ... N ) )
73 6 72 sseldi 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> ( d ` a ) e. NN )
74 fveq2 
 |-  ( x = a -> ( L ` x ) = ( L ` a ) )
75 74 fveq1d 
 |-  ( x = a -> ( ( L ` x ) ` y ) = ( ( L ` a ) ` y ) )
76 75 eleq1d 
 |-  ( x = a -> ( ( ( L ` x ) ` y ) e. CC <-> ( ( L ` a ) ` y ) e. CC ) )
77 fveq2 
 |-  ( y = ( d ` a ) -> ( ( L ` a ) ` y ) = ( ( L ` a ) ` ( d ` a ) ) )
78 77 eleq1d 
 |-  ( y = ( d ` a ) -> ( ( ( L ` a ) ` y ) e. CC <-> ( ( L ` a ) ` ( d ` a ) ) e. CC ) )
79 76 78 rspc2v 
 |-  ( ( a e. ( 0 ..^ ( S + 1 ) ) /\ ( d ` a ) e. NN ) -> ( A. x e. ( 0 ..^ ( S + 1 ) ) A. y e. NN ( ( L ` x ) ` y ) e. CC -> ( ( L ` a ) ` ( d ` a ) ) e. CC ) )
80 38 73 79 syl2anc 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> ( A. x e. ( 0 ..^ ( S + 1 ) ) A. y e. NN ( ( L ` x ) ` y ) e. CC -> ( ( L ` a ) ` ( d ` a ) ) e. CC ) )
81 37 80 mpd 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> ( ( L ` a ) ` ( d ` a ) ) e. CC )
82 34 81 fprodcl 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) -> prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) e. CC )
83 82 anasss 
 |-  ( ( ph /\ ( b e. ( 1 ... N ) /\ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ) ) -> prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) e. CC )
84 12 25 32 83 fsumiun 
 |-  ( ph -> sum_ d e. U_ b e. ( 1 ... N ) ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) = sum_ b e. ( 1 ... N ) sum_ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) )
85 60 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
86 85 prodeq1d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) = prod_ a e. ( ( 0 ..^ S ) u. { S } ) ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) )
87 nfv 
 |-  F/ a ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) )
88 nfcv 
 |-  F/_ a ( ( L ` S ) ` ( ( e u. { <. S , b >. } ) ` S ) )
89 fzofi 
 |-  ( 0 ..^ S ) e. Fin
90 89 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( 0 ..^ S ) e. Fin )
91 19 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> S e. NN0 )
92 30 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> -. S e. ( 0 ..^ S ) )
93 6 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( 1 ... N ) C_ NN )
94 18 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( M - b ) e. ZZ )
95 simpr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) )
96 93 94 91 95 reprf 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> e : ( 0 ..^ S ) --> ( 1 ... N ) )
97 96 ffnd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> e Fn ( 0 ..^ S ) )
98 97 adantr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> e Fn ( 0 ..^ S ) )
99 16 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> b e. ( 1 ... N ) )
100 fnsng 
 |-  ( ( S e. NN0 /\ b e. ( 1 ... N ) ) -> { <. S , b >. } Fn { S } )
101 91 99 100 syl2anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> { <. S , b >. } Fn { S } )
102 101 adantr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> { <. S , b >. } Fn { S } )
103 52 a1i 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( 0 ..^ S ) i^i { S } ) = (/) )
104 simpr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
105 fvun1 
 |-  ( ( e Fn ( 0 ..^ S ) /\ { <. S , b >. } Fn { S } /\ ( ( ( 0 ..^ S ) i^i { S } ) = (/) /\ a e. ( 0 ..^ S ) ) ) -> ( ( e u. { <. S , b >. } ) ` a ) = ( e ` a ) )
106 98 102 103 104 105 syl112anc 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( e u. { <. S , b >. } ) ` a ) = ( e ` a ) )
107 106 fveq2d 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) = ( ( L ` a ) ` ( e ` a ) ) )
108 36 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> A. x e. ( 0 ..^ ( S + 1 ) ) A. y e. NN ( ( L ` x ) ` y ) e. CC )
109 108 adantr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> A. x e. ( 0 ..^ ( S + 1 ) ) A. y e. NN ( ( L ` x ) ` y ) e. CC )
110 fzossfzop1 
 |-  ( S e. NN0 -> ( 0 ..^ S ) C_ ( 0 ..^ ( S + 1 ) ) )
111 2 110 syl 
 |-  ( ph -> ( 0 ..^ S ) C_ ( 0 ..^ ( S + 1 ) ) )
112 111 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( 0 ..^ S ) C_ ( 0 ..^ ( S + 1 ) ) )
113 112 sselda 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ ( S + 1 ) ) )
114 96 ffvelrnda 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( e ` a ) e. ( 1 ... N ) )
115 6 114 sseldi 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( e ` a ) e. NN )
116 fveq2 
 |-  ( y = ( e ` a ) -> ( ( L ` a ) ` y ) = ( ( L ` a ) ` ( e ` a ) ) )
117 116 eleq1d 
 |-  ( y = ( e ` a ) -> ( ( ( L ` a ) ` y ) e. CC <-> ( ( L ` a ) ` ( e ` a ) ) e. CC ) )
118 76 117 rspc2v 
 |-  ( ( a e. ( 0 ..^ ( S + 1 ) ) /\ ( e ` a ) e. NN ) -> ( A. x e. ( 0 ..^ ( S + 1 ) ) A. y e. NN ( ( L ` x ) ` y ) e. CC -> ( ( L ` a ) ` ( e ` a ) ) e. CC ) )
119 113 115 118 syl2anc 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( A. x e. ( 0 ..^ ( S + 1 ) ) A. y e. NN ( ( L ` x ) ` y ) e. CC -> ( ( L ` a ) ` ( e ` a ) ) e. CC ) )
120 109 119 mpd 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( e ` a ) ) e. CC )
121 107 120 eqeltrd 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) e. CC )
122 fveq2 
 |-  ( a = S -> ( L ` a ) = ( L ` S ) )
123 fveq2 
 |-  ( a = S -> ( ( e u. { <. S , b >. } ) ` a ) = ( ( e u. { <. S , b >. } ) ` S ) )
124 122 123 fveq12d 
 |-  ( a = S -> ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) = ( ( L ` S ) ` ( ( e u. { <. S , b >. } ) ` S ) ) )
125 52 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( 0 ..^ S ) i^i { S } ) = (/) )
126 snidg 
 |-  ( S e. NN0 -> S e. { S } )
127 91 126 syl 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> S e. { S } )
128 fvun2 
 |-  ( ( e Fn ( 0 ..^ S ) /\ { <. S , b >. } Fn { S } /\ ( ( ( 0 ..^ S ) i^i { S } ) = (/) /\ S e. { S } ) ) -> ( ( e u. { <. S , b >. } ) ` S ) = ( { <. S , b >. } ` S ) )
129 97 101 125 127 128 syl112anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( e u. { <. S , b >. } ) ` S ) = ( { <. S , b >. } ` S ) )
130 fvsng 
 |-  ( ( S e. NN0 /\ b e. ( 1 ... N ) ) -> ( { <. S , b >. } ` S ) = b )
131 91 99 130 syl2anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( { <. S , b >. } ` S ) = b )
132 129 131 eqtrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( e u. { <. S , b >. } ) ` S ) = b )
133 132 fveq2d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( L ` S ) ` ( ( e u. { <. S , b >. } ) ` S ) ) = ( ( L ` S ) ` b ) )
134 fzonn0p1 
 |-  ( S e. NN0 -> S e. ( 0 ..^ ( S + 1 ) ) )
135 2 134 syl 
 |-  ( ph -> S e. ( 0 ..^ ( S + 1 ) ) )
136 135 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> S e. ( 0 ..^ ( S + 1 ) ) )
137 6 99 sseldi 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> b e. NN )
138 fveq2 
 |-  ( x = S -> ( L ` x ) = ( L ` S ) )
139 138 fveq1d 
 |-  ( x = S -> ( ( L ` x ) ` y ) = ( ( L ` S ) ` y ) )
140 139 eleq1d 
 |-  ( x = S -> ( ( ( L ` x ) ` y ) e. CC <-> ( ( L ` S ) ` y ) e. CC ) )
141 fveq2 
 |-  ( y = b -> ( ( L ` S ) ` y ) = ( ( L ` S ) ` b ) )
142 141 eleq1d 
 |-  ( y = b -> ( ( ( L ` S ) ` y ) e. CC <-> ( ( L ` S ) ` b ) e. CC ) )
143 140 142 rspc2v 
 |-  ( ( S e. ( 0 ..^ ( S + 1 ) ) /\ b e. NN ) -> ( A. x e. ( 0 ..^ ( S + 1 ) ) A. y e. NN ( ( L ` x ) ` y ) e. CC -> ( ( L ` S ) ` b ) e. CC ) )
144 136 137 143 syl2anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( A. x e. ( 0 ..^ ( S + 1 ) ) A. y e. NN ( ( L ` x ) ` y ) e. CC -> ( ( L ` S ) ` b ) e. CC ) )
145 108 144 mpd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( L ` S ) ` b ) e. CC )
146 133 145 eqeltrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( L ` S ) ` ( ( e u. { <. S , b >. } ) ` S ) ) e. CC )
147 87 88 90 91 92 121 124 146 fprodsplitsn 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> prod_ a e. ( ( 0 ..^ S ) u. { S } ) ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) x. ( ( L ` S ) ` ( ( e u. { <. S , b >. } ) ` S ) ) ) )
148 107 prodeq2dv 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) = prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( e ` a ) ) )
149 148 133 oveq12d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) x. ( ( L ` S ) ` ( ( e u. { <. S , b >. } ) ` S ) ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( e ` a ) ) x. ( ( L ` S ) ` b ) ) )
150 86 147 149 3eqtrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( e ` a ) ) x. ( ( L ` S ) ` b ) ) )
151 150 sumeq2dv 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> sum_ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) = sum_ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( e ` a ) ) x. ( ( L ` S ) ` b ) ) )
152 simpl 
 |-  ( ( d = ( e u. { <. S , b >. } ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> d = ( e u. { <. S , b >. } ) )
153 152 fveq1d 
 |-  ( ( d = ( e u. { <. S , b >. } ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> ( d ` a ) = ( ( e u. { <. S , b >. } ) ` a ) )
154 153 fveq2d 
 |-  ( ( d = ( e u. { <. S , b >. } ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> ( ( L ` a ) ` ( d ` a ) ) = ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) )
155 154 prodeq2dv 
 |-  ( d = ( e u. { <. S , b >. } ) -> prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) = prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) )
156 28 29 2 31 9 actfunsnf1o 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) : ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) -1-1-onto-> ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) )
157 9 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) = ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) )
158 simpr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ v = e ) -> v = e )
159 158 uneq1d 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ v = e ) -> ( v u. { <. S , b >. } ) = ( e u. { <. S , b >. } ) )
160 vex 
 |-  e e. _V
161 160 66 unex 
 |-  ( e u. { <. S , b >. } ) e. _V
162 161 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( e u. { <. S , b >. } ) e. _V )
163 157 159 95 162 fvmptd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) ` e ) = ( e u. { <. S , b >. } ) )
164 155 21 156 163 82 fsumf1o 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> sum_ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) = sum_ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) )
165 simpl 
 |-  ( ( d = e /\ a e. ( 0 ..^ S ) ) -> d = e )
166 165 fveq1d 
 |-  ( ( d = e /\ a e. ( 0 ..^ S ) ) -> ( d ` a ) = ( e ` a ) )
167 166 fveq2d 
 |-  ( ( d = e /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( d ` a ) ) = ( ( L ` a ) ` ( e ` a ) ) )
168 167 prodeq2dv 
 |-  ( d = e -> prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( d ` a ) ) = prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( e ` a ) ) )
169 168 oveq1d 
 |-  ( d = e -> ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` S ) ` b ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( e ` a ) ) x. ( ( L ` S ) ` b ) ) )
170 169 cbvsumv 
 |-  sum_ d e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` S ) ` b ) ) = sum_ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( e ` a ) ) x. ( ( L ` S ) ` b ) )
171 170 a1i 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> sum_ d e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` S ) ` b ) ) = sum_ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( e ` a ) ) x. ( ( L ` S ) ` b ) ) )
172 151 164 171 3eqtr4d 
 |-  ( ( ph /\ b e. ( 1 ... N ) ) -> sum_ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) = sum_ d e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` S ) ` b ) ) )
173 172 sumeq2dv 
 |-  ( ph -> sum_ b e. ( 1 ... N ) sum_ d e. ran ( v e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) |-> ( v u. { <. S , b >. } ) ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) = sum_ b e. ( 1 ... N ) sum_ d e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` S ) ` b ) ) )
174 11 84 173 3eqtrd 
 |-  ( ph -> sum_ d e. ( ( 1 ... N ) ( repr ` ( S + 1 ) ) M ) prod_ a e. ( 0 ..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) = sum_ b e. ( 1 ... N ) sum_ d e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` S ) ` b ) ) )