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 sselid 
 |-  ( ( 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 vex 
 |-  v e. _V
65 snex 
 |-  { <. S , b >. } e. _V
66 64 65 unex 
 |-  ( v u. { <. S , b >. } ) e. _V
67 9 66 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 >. } ) )
68 67 bilani 
 |-  ( ( ( 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 >. } ) )
69 44 63 68 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 ) )
70 69 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 ) )
71 70 38 ffvelcdmd 
 |-  ( ( ( ( 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 ) )
72 6 71 sselid 
 |-  ( ( ( ( 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 )
73 fveq2 
 |-  ( x = a -> ( L ` x ) = ( L ` a ) )
74 73 fveq1d 
 |-  ( x = a -> ( ( L ` x ) ` y ) = ( ( L ` a ) ` y ) )
75 74 eleq1d 
 |-  ( x = a -> ( ( ( L ` x ) ` y ) e. CC <-> ( ( L ` a ) ` y ) e. CC ) )
76 fveq2 
 |-  ( y = ( d ` a ) -> ( ( L ` a ) ` y ) = ( ( L ` a ) ` ( d ` a ) ) )
77 76 eleq1d 
 |-  ( y = ( d ` a ) -> ( ( ( L ` a ) ` y ) e. CC <-> ( ( L ` a ) ` ( d ` a ) ) e. CC ) )
78 75 77 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 ) )
79 38 72 78 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 ) )
80 37 79 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 )
81 34 80 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 )
82 81 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 )
83 12 25 32 82 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 ) ) )
84 60 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( 0 ..^ ( S + 1 ) ) = ( ( 0 ..^ S ) u. { S } ) )
85 84 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 ) ) )
86 nfv 
 |-  F/ a ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) )
87 nfcv 
 |-  F/_ a ( ( L ` S ) ` ( ( e u. { <. S , b >. } ) ` S ) )
88 fzofi 
 |-  ( 0 ..^ S ) e. Fin
89 88 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( 0 ..^ S ) e. Fin )
90 19 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> S e. NN0 )
91 30 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> -. S e. ( 0 ..^ S ) )
92 6 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( 1 ... N ) C_ NN )
93 18 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( M - b ) e. ZZ )
94 simpr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) )
95 92 93 90 94 reprf 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> e : ( 0 ..^ S ) --> ( 1 ... N ) )
96 95 ffnd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> e Fn ( 0 ..^ S ) )
97 96 adantr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> e Fn ( 0 ..^ S ) )
98 16 adantr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> b e. ( 1 ... N ) )
99 fnsng 
 |-  ( ( S e. NN0 /\ b e. ( 1 ... N ) ) -> { <. S , b >. } Fn { S } )
100 90 98 99 syl2anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> { <. S , b >. } Fn { S } )
101 100 adantr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> { <. S , b >. } Fn { S } )
102 52 a1i 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( 0 ..^ S ) i^i { S } ) = (/) )
103 simpr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
104 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 ) )
105 97 101 102 103 104 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 ) )
106 105 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 ) ) )
107 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 )
108 107 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 )
109 fzossfzop1 
 |-  ( S e. NN0 -> ( 0 ..^ S ) C_ ( 0 ..^ ( S + 1 ) ) )
110 2 109 syl 
 |-  ( ph -> ( 0 ..^ S ) C_ ( 0 ..^ ( S + 1 ) ) )
111 110 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( 0 ..^ S ) C_ ( 0 ..^ ( S + 1 ) ) )
112 111 sselda 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ ( S + 1 ) ) )
113 95 ffvelcdmda 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( e ` a ) e. ( 1 ... N ) )
114 6 113 sselid 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( e ` a ) e. NN )
115 fveq2 
 |-  ( y = ( e ` a ) -> ( ( L ` a ) ` y ) = ( ( L ` a ) ` ( e ` a ) ) )
116 115 eleq1d 
 |-  ( y = ( e ` a ) -> ( ( ( L ` a ) ` y ) e. CC <-> ( ( L ` a ) ` ( e ` a ) ) e. CC ) )
117 75 116 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 ) )
118 112 114 117 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 ) )
119 108 118 mpd 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( e ` a ) ) e. CC )
120 106 119 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 )
121 fveq2 
 |-  ( a = S -> ( L ` a ) = ( L ` S ) )
122 fveq2 
 |-  ( a = S -> ( ( e u. { <. S , b >. } ) ` a ) = ( ( e u. { <. S , b >. } ) ` S ) )
123 121 122 fveq12d 
 |-  ( a = S -> ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) = ( ( L ` S ) ` ( ( e u. { <. S , b >. } ) ` S ) ) )
124 52 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( 0 ..^ S ) i^i { S } ) = (/) )
125 snidg 
 |-  ( S e. NN0 -> S e. { S } )
126 90 125 syl 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> S e. { S } )
127 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 ) )
128 96 100 124 126 127 syl112anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( e u. { <. S , b >. } ) ` S ) = ( { <. S , b >. } ` S ) )
129 fvsng 
 |-  ( ( S e. NN0 /\ b e. ( 1 ... N ) ) -> ( { <. S , b >. } ` S ) = b )
130 90 98 129 syl2anc 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( { <. S , b >. } ` S ) = b )
131 128 130 eqtrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( e u. { <. S , b >. } ) ` S ) = b )
132 131 fveq2d 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( L ` S ) ` ( ( e u. { <. S , b >. } ) ` S ) ) = ( ( L ` S ) ` b ) )
133 fzonn0p1 
 |-  ( S e. NN0 -> S e. ( 0 ..^ ( S + 1 ) ) )
134 2 133 syl 
 |-  ( ph -> S e. ( 0 ..^ ( S + 1 ) ) )
135 134 ad2antrr 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> S e. ( 0 ..^ ( S + 1 ) ) )
136 6 98 sselid 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> b e. NN )
137 fveq2 
 |-  ( x = S -> ( L ` x ) = ( L ` S ) )
138 137 fveq1d 
 |-  ( x = S -> ( ( L ` x ) ` y ) = ( ( L ` S ) ` y ) )
139 138 eleq1d 
 |-  ( x = S -> ( ( ( L ` x ) ` y ) e. CC <-> ( ( L ` S ) ` y ) e. CC ) )
140 fveq2 
 |-  ( y = b -> ( ( L ` S ) ` y ) = ( ( L ` S ) ` b ) )
141 140 eleq1d 
 |-  ( y = b -> ( ( ( L ` S ) ` y ) e. CC <-> ( ( L ` S ) ` b ) e. CC ) )
142 139 141 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 ) )
143 135 136 142 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 ) )
144 107 143 mpd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( L ` S ) ` b ) e. CC )
145 132 144 eqeltrd 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( ( L ` S ) ` ( ( e u. { <. S , b >. } ) ` S ) ) e. CC )
146 86 87 89 90 91 120 123 145 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 ) ) ) )
147 106 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 ) ) )
148 147 132 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 ) ) )
149 85 146 148 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 ) ) )
150 149 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 ) ) )
151 simpl 
 |-  ( ( d = ( e u. { <. S , b >. } ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> d = ( e u. { <. S , b >. } ) )
152 151 fveq1d 
 |-  ( ( d = ( e u. { <. S , b >. } ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> ( d ` a ) = ( ( e u. { <. S , b >. } ) ` a ) )
153 152 fveq2d 
 |-  ( ( d = ( e u. { <. S , b >. } ) /\ a e. ( 0 ..^ ( S + 1 ) ) ) -> ( ( L ` a ) ` ( d ` a ) ) = ( ( L ` a ) ` ( ( e u. { <. S , b >. } ) ` a ) ) )
154 153 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 ) ) )
155 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 >. } ) ) )
156 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 >. } ) ) )
157 simpr 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ v = e ) -> v = e )
158 157 uneq1d 
 |-  ( ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) /\ v = e ) -> ( v u. { <. S , b >. } ) = ( e u. { <. S , b >. } ) )
159 vex 
 |-  e e. _V
160 159 65 unex 
 |-  ( e u. { <. S , b >. } ) e. _V
161 160 a1i 
 |-  ( ( ( ph /\ b e. ( 1 ... N ) ) /\ e e. ( ( 1 ... N ) ( repr ` S ) ( M - b ) ) ) -> ( e u. { <. S , b >. } ) e. _V )
162 156 158 94 161 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 >. } ) )
163 154 21 155 162 81 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 ) ) )
164 simpl 
 |-  ( ( d = e /\ a e. ( 0 ..^ S ) ) -> d = e )
165 164 fveq1d 
 |-  ( ( d = e /\ a e. ( 0 ..^ S ) ) -> ( d ` a ) = ( e ` a ) )
166 165 fveq2d 
 |-  ( ( d = e /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( d ` a ) ) = ( ( L ` a ) ` ( e ` a ) ) )
167 166 prodeq2dv 
 |-  ( d = e -> prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( d ` a ) ) = prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( e ` a ) ) )
168 167 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 ) ) )
169 168 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 ) )
170 169 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 ) ) )
171 150 163 170 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 ) ) )
172 171 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 ) ) )
173 11 83 172 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 ) ) )