This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem breprexpnat

Description: Express the S th power of the finite series in terms of the number of representations of integers m as sums of S terms of elements of A , bounded by N . Proposition of Nathanson p. 123. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses breprexp.n 
|- ( ph -> N e. NN0 )
breprexp.s 
|- ( ph -> S e. NN0 )
breprexp.z 
|- ( ph -> Z e. CC )
breprexpnat.a 
|- ( ph -> A C_ NN )
breprexpnat.p 
|- P = sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b )
breprexpnat.r 
|- R = ( # ` ( ( A i^i ( 1 ... N ) ) ( repr ` S ) m ) )
Assertion breprexpnat 
|- ( ph -> ( P ^ S ) = sum_ m e. ( 0 ... ( S x. N ) ) ( R 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 breprexpnat.a 
 |-  ( ph -> A C_ NN )
5 breprexpnat.p 
 |-  P = sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b )
6 breprexpnat.r 
 |-  R = ( # ` ( ( A i^i ( 1 ... N ) ) ( repr ` S ) m ) )
7 fvex 
 |-  ( ( _Ind ` NN ) ` A ) e. _V
8 7 fconst 
 |-  ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) : ( 0 ..^ S ) --> { ( ( _Ind ` NN ) ` A ) }
9 nnex 
 |-  NN e. _V
10 indf 
 |-  ( ( NN e. _V /\ A C_ NN ) -> ( ( _Ind ` NN ) ` A ) : NN --> { 0 , 1 } )
11 9 4 10 sylancr 
 |-  ( ph -> ( ( _Ind ` NN ) ` A ) : NN --> { 0 , 1 } )
12 0cn 
 |-  0 e. CC
13 ax-1cn 
 |-  1 e. CC
14 prssi 
 |-  ( ( 0 e. CC /\ 1 e. CC ) -> { 0 , 1 } C_ CC )
15 12 13 14 mp2an 
 |-  { 0 , 1 } C_ CC
16 fss 
 |-  ( ( ( ( _Ind ` NN ) ` A ) : NN --> { 0 , 1 } /\ { 0 , 1 } C_ CC ) -> ( ( _Ind ` NN ) ` A ) : NN --> CC )
17 11 15 16 sylancl 
 |-  ( ph -> ( ( _Ind ` NN ) ` A ) : NN --> CC )
18 cnex 
 |-  CC e. _V
19 18 9 elmap 
 |-  ( ( ( _Ind ` NN ) ` A ) e. ( CC ^m NN ) <-> ( ( _Ind ` NN ) ` A ) : NN --> CC )
20 17 19 sylibr 
 |-  ( ph -> ( ( _Ind ` NN ) ` A ) e. ( CC ^m NN ) )
21 7 snss 
 |-  ( ( ( _Ind ` NN ) ` A ) e. ( CC ^m NN ) <-> { ( ( _Ind ` NN ) ` A ) } C_ ( CC ^m NN ) )
22 20 21 sylib 
 |-  ( ph -> { ( ( _Ind ` NN ) ` A ) } C_ ( CC ^m NN ) )
23 fss 
 |-  ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) : ( 0 ..^ S ) --> { ( ( _Ind ` NN ) ` A ) } /\ { ( ( _Ind ` NN ) ` A ) } C_ ( CC ^m NN ) ) -> ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) : ( 0 ..^ S ) --> ( CC ^m NN ) )
24 8 22 23 sylancr 
 |-  ( ph -> ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) : ( 0 ..^ S ) --> ( CC ^m NN ) )
25 1 2 3 24 breprexp 
 |-  ( ph -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
26 7 fvconst2 
 |-  ( a e. ( 0 ..^ S ) -> ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) = ( ( _Ind ` NN ) ` A ) )
27 26 ad2antlr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) = ( ( _Ind ` NN ) ` A ) )
28 27 fveq1d 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` b ) = ( ( ( _Ind ` NN ) ` A ) ` b ) )
29 28 oveq1d 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` b ) x. ( Z ^ b ) ) = ( ( ( ( _Ind ` NN ) ` A ) ` b ) x. ( Z ^ b ) ) )
30 29 sumeq2dv 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> sum_ b e. ( 1 ... N ) ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` b ) x. ( Z ^ b ) ) = sum_ b e. ( 1 ... N ) ( ( ( ( _Ind ` NN ) ` A ) ` b ) x. ( Z ^ b ) ) )
31 9 a1i 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> NN e. _V )
32 fzfi 
 |-  ( 1 ... N ) e. Fin
33 32 a1i 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> ( 1 ... N ) e. Fin )
34 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
35 34 a1i 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> ( 1 ... N ) C_ NN )
36 4 adantr 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> A C_ NN )
37 3 ad2antrr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> Z e. CC )
38 nnssnn0 
 |-  NN C_ NN0
39 34 38 sstri 
 |-  ( 1 ... N ) C_ NN0
40 simpr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> b e. ( 1 ... N ) )
41 39 40 sselid 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> b e. NN0 )
42 37 41 expcld 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( Z ^ b ) e. CC )
43 31 33 35 36 42 indsumin 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> sum_ b e. ( 1 ... N ) ( ( ( ( _Ind ` NN ) ` A ) ` b ) x. ( Z ^ b ) ) = sum_ b e. ( ( 1 ... N ) i^i A ) ( Z ^ b ) )
44 incom 
 |-  ( ( 1 ... N ) i^i A ) = ( A i^i ( 1 ... N ) )
45 44 a1i 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> ( ( 1 ... N ) i^i A ) = ( A i^i ( 1 ... N ) ) )
46 45 sumeq1d 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> sum_ b e. ( ( 1 ... N ) i^i A ) ( Z ^ b ) = sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) )
47 30 43 46 3eqtrd 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> sum_ b e. ( 1 ... N ) ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` b ) x. ( Z ^ b ) ) = sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) )
48 47 prodeq2dv 
 |-  ( ph -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` b ) x. ( Z ^ b ) ) = prod_ a e. ( 0 ..^ S ) sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) )
49 fzofi 
 |-  ( 0 ..^ S ) e. Fin
50 49 a1i 
 |-  ( ph -> ( 0 ..^ S ) e. Fin )
51 inss2 
 |-  ( A i^i ( 1 ... N ) ) C_ ( 1 ... N )
52 ssfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( A i^i ( 1 ... N ) ) C_ ( 1 ... N ) ) -> ( A i^i ( 1 ... N ) ) e. Fin )
53 32 51 52 mp2an 
 |-  ( A i^i ( 1 ... N ) ) e. Fin
54 53 a1i 
 |-  ( ph -> ( A i^i ( 1 ... N ) ) e. Fin )
55 3 adantr 
 |-  ( ( ph /\ b e. ( A i^i ( 1 ... N ) ) ) -> Z e. CC )
56 51 39 sstri 
 |-  ( A i^i ( 1 ... N ) ) C_ NN0
57 simpr 
 |-  ( ( ph /\ b e. ( A i^i ( 1 ... N ) ) ) -> b e. ( A i^i ( 1 ... N ) ) )
58 56 57 sselid 
 |-  ( ( ph /\ b e. ( A i^i ( 1 ... N ) ) ) -> b e. NN0 )
59 55 58 expcld 
 |-  ( ( ph /\ b e. ( A i^i ( 1 ... N ) ) ) -> ( Z ^ b ) e. CC )
60 54 59 fsumcl 
 |-  ( ph -> sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) e. CC )
61 fprodconst 
 |-  ( ( ( 0 ..^ S ) e. Fin /\ sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) e. CC ) -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) = ( sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) ^ ( # ` ( 0 ..^ S ) ) ) )
62 50 60 61 syl2anc 
 |-  ( ph -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) = ( sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) ^ ( # ` ( 0 ..^ S ) ) ) )
63 hashfzo0 
 |-  ( S e. NN0 -> ( # ` ( 0 ..^ S ) ) = S )
64 2 63 syl 
 |-  ( ph -> ( # ` ( 0 ..^ S ) ) = S )
65 64 oveq2d 
 |-  ( ph -> ( sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) ^ ( # ` ( 0 ..^ S ) ) ) = ( sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) ^ S ) )
66 48 62 65 3eqtrd 
 |-  ( ph -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` b ) x. ( Z ^ b ) ) = ( sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) ^ S ) )
67 34 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 1 ... N ) C_ NN )
68 fzssz 
 |-  ( 0 ... ( S x. N ) ) C_ ZZ
69 simpr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. ( 0 ... ( S x. N ) ) )
70 68 69 sselid 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. ZZ )
71 2 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> S e. NN0 )
72 32 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 1 ... N ) e. Fin )
73 67 70 71 72 reprfi 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( 1 ... N ) ( repr ` S ) m ) e. Fin )
74 3 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> Z e. CC )
75 fz0ssnn0 
 |-  ( 0 ... ( S x. N ) ) C_ NN0
76 75 69 sselid 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. NN0 )
77 74 76 expcld 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( Z ^ m ) e. CC )
78 49 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( 0 ..^ S ) e. Fin )
79 11 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( _Ind ` NN ) ` A ) : NN --> { 0 , 1 } )
80 34 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( 1 ... N ) C_ NN )
81 70 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> m e. ZZ )
82 71 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> S e. NN0 )
83 simpr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> c e. ( ( 1 ... N ) ( repr ` S ) m ) )
84 80 81 82 83 reprf 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> c : ( 0 ..^ S ) --> ( 1 ... N ) )
85 84 ffvelcdmda 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. ( 1 ... N ) )
86 34 85 sselid 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. NN )
87 79 86 ffvelcdmd 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) e. { 0 , 1 } )
88 15 87 sselid 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) e. CC )
89 78 88 fprodcl 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) e. CC )
90 73 77 89 fsummulc1 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
91 4 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> A C_ NN )
92 91 70 71 72 67 hashreprin 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( # ` ( ( A i^i ( 1 ... N ) ) ( repr ` S ) m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
93 92 oveq1d 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( # ` ( ( A i^i ( 1 ... N ) ) ( repr ` S ) m ) ) x. ( Z ^ m ) ) = ( sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
94 26 fveq1d 
 |-  ( a e. ( 0 ..^ S ) -> ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) = ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
95 94 adantl 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) = ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
96 95 prodeq2dv 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) = prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
97 96 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) = prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
98 97 oveq1d 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
99 98 sumeq2dv 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
100 90 93 99 3eqtr4rd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( ( # ` ( ( A i^i ( 1 ... N ) ) ( repr ` S ) m ) ) x. ( Z ^ m ) ) )
101 100 sumeq2dv 
 |-  ( ph -> sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ m e. ( 0 ... ( S x. N ) ) ( ( # ` ( ( A i^i ( 1 ... N ) ) ( repr ` S ) m ) ) x. ( Z ^ m ) ) )
102 25 66 101 3eqtr3d 
 |-  ( ph -> ( sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) ^ S ) = sum_ m e. ( 0 ... ( S x. N ) ) ( ( # ` ( ( A i^i ( 1 ... N ) ) ( repr ` S ) m ) ) x. ( Z ^ m ) ) )
103 5 oveq1i 
 |-  ( P ^ S ) = ( sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b ) ^ S )
104 6 oveq1i 
 |-  ( R x. ( Z ^ m ) ) = ( ( # ` ( ( A i^i ( 1 ... N ) ) ( repr ` S ) m ) ) x. ( Z ^ m ) )
105 104 a1i 
 |-  ( m e. ( 0 ... ( S x. N ) ) -> ( R x. ( Z ^ m ) ) = ( ( # ` ( ( A i^i ( 1 ... N ) ) ( repr ` S ) m ) ) x. ( Z ^ m ) ) )
106 105 sumeq2i 
 |-  sum_ m e. ( 0 ... ( S x. N ) ) ( R x. ( Z ^ m ) ) = sum_ m e. ( 0 ... ( S x. N ) ) ( ( # ` ( ( A i^i ( 1 ... N ) ) ( repr ` S ) m ) ) x. ( Z ^ m ) )
107 102 103 106 3eqtr4g 
 |-  ( ph -> ( P ^ S ) = sum_ m e. ( 0 ... ( S x. N ) ) ( R x. ( Z ^ m ) ) )