Metamath Proof Explorer

Theorem smupval

Description: Rewrite the elements of the partial sum sequence in terms of sequence multiplication. (Contributed by Mario Carneiro, 20-Sep-2016)

Ref Expression
Hypotheses smupval.a 
|- ( ph -> A C_ NN0 )
smupval.b 
|- ( ph -> B C_ NN0 )
smupval.p 
|- P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
smupval.n 
|- ( ph -> N e. NN0 )
Assertion smupval 
|- ( ph -> ( P ` N ) = ( ( A i^i ( 0 ..^ N ) ) smul B ) )

Proof

Step Hyp Ref Expression
1 smupval.a 
 |-  ( ph -> A C_ NN0 )
2 smupval.b 
 |-  ( ph -> B C_ NN0 )
3 smupval.p 
 |-  P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
4 smupval.n 
 |-  ( ph -> N e. NN0 )
5 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
6 4 5 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
7 eluzfz2b 
 |-  ( N e. ( ZZ>= ` 0 ) <-> N e. ( 0 ... N ) )
8 6 7 sylib 
 |-  ( ph -> N e. ( 0 ... N ) )
9 fveq2 
 |-  ( x = 0 -> ( P ` x ) = ( P ` 0 ) )
10 fveq2 
 |-  ( x = 0 -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) )
11 9 10 eqeq12d 
 |-  ( x = 0 -> ( ( P ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) <-> ( P ` 0 ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) ) )
12 11 imbi2d 
 |-  ( x = 0 -> ( ( ph -> ( P ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) ) <-> ( ph -> ( P ` 0 ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) ) ) )
13 fveq2 
 |-  ( x = k -> ( P ` x ) = ( P ` k ) )
14 fveq2 
 |-  ( x = k -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) )
15 13 14 eqeq12d 
 |-  ( x = k -> ( ( P ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) <-> ( P ` k ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) )
16 15 imbi2d 
 |-  ( x = k -> ( ( ph -> ( P ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) ) <-> ( ph -> ( P ` k ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) ) )
17 fveq2 
 |-  ( x = ( k + 1 ) -> ( P ` x ) = ( P ` ( k + 1 ) ) )
18 fveq2 
 |-  ( x = ( k + 1 ) -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) )
19 17 18 eqeq12d 
 |-  ( x = ( k + 1 ) -> ( ( P ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) <-> ( P ` ( k + 1 ) ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) ) )
20 19 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ph -> ( P ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) ) <-> ( ph -> ( P ` ( k + 1 ) ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) ) ) )
21 fveq2 
 |-  ( x = N -> ( P ` x ) = ( P ` N ) )
22 fveq2 
 |-  ( x = N -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) )
23 21 22 eqeq12d 
 |-  ( x = N -> ( ( P ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) <-> ( P ` N ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) ) )
24 23 imbi2d 
 |-  ( x = N -> ( ( ph -> ( P ` x ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` x ) ) <-> ( ph -> ( P ` N ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) ) ) )
25 1 2 3 smup0 
 |-  ( ph -> ( P ` 0 ) = (/) )
26 inss1 
 |-  ( A i^i ( 0 ..^ N ) ) C_ A
27 26 1 sstrid 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) C_ NN0 )
28 eqid 
 |-  seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
29 27 2 28 smup0 
 |-  ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) = (/) )
30 25 29 eqtr4d 
 |-  ( ph -> ( P ` 0 ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) )
31 30 a1i 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( ph -> ( P ` 0 ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` 0 ) ) )
32 oveq1 
 |-  ( ( P ` k ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) -> ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) = ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) )
33 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> A C_ NN0 )
34 2 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> B C_ NN0 )
35 elfzouz 
 |-  ( k e. ( 0 ..^ N ) -> k e. ( ZZ>= ` 0 ) )
36 35 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ( ZZ>= ` 0 ) )
37 36 5 eleqtrrdi 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. NN0 )
38 33 34 3 37 smupp1 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( P ` ( k + 1 ) ) = ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) )
39 27 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( A i^i ( 0 ..^ N ) ) C_ NN0 )
40 39 34 28 37 smupp1 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) sadd { n e. NN0 | ( k e. ( A i^i ( 0 ..^ N ) ) /\ ( n - k ) e. B ) } ) )
41 elin 
 |-  ( k e. ( A i^i ( 0 ..^ N ) ) <-> ( k e. A /\ k e. ( 0 ..^ N ) ) )
42 41 rbaib 
 |-  ( k e. ( 0 ..^ N ) -> ( k e. ( A i^i ( 0 ..^ N ) ) <-> k e. A ) )
43 42 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k e. ( A i^i ( 0 ..^ N ) ) <-> k e. A ) )
44 43 anbi1d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( k e. ( A i^i ( 0 ..^ N ) ) /\ ( n - k ) e. B ) <-> ( k e. A /\ ( n - k ) e. B ) ) )
45 44 rabbidv 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> { n e. NN0 | ( k e. ( A i^i ( 0 ..^ N ) ) /\ ( n - k ) e. B ) } = { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } )
46 45 oveq2d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) sadd { n e. NN0 | ( k e. ( A i^i ( 0 ..^ N ) ) /\ ( n - k ) e. B ) } ) = ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) )
47 40 46 eqtrd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) = ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) )
48 38 47 eqeq12d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( P ` ( k + 1 ) ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) <-> ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) = ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) ) )
49 32 48 syl5ibr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( P ` k ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) -> ( P ` ( k + 1 ) ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) ) )
50 49 expcom 
 |-  ( k e. ( 0 ..^ N ) -> ( ph -> ( ( P ` k ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) -> ( P ` ( k + 1 ) ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) ) ) )
51 50 a2d 
 |-  ( k e. ( 0 ..^ N ) -> ( ( ph -> ( P ` k ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) -> ( ph -> ( P ` ( k + 1 ) ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) ) ) )
52 12 16 20 24 31 51 fzind2 
 |-  ( N e. ( 0 ... N ) -> ( ph -> ( P ` N ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) ) )
53 8 52 mpcom 
 |-  ( ph -> ( P ` N ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) )
54 inss2 
 |-  ( A i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
55 54 a1i 
 |-  ( ph -> ( A i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) )
56 4 nn0zd 
 |-  ( ph -> N e. ZZ )
57 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
58 56 57 syl 
 |-  ( ph -> N e. ( ZZ>= ` N ) )
59 27 2 28 4 55 58 smupvallem 
 |-  ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. ( A i^i ( 0 ..^ N ) ) /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) = ( ( A i^i ( 0 ..^ N ) ) smul B ) )
60 53 59 eqtrd 
 |-  ( ph -> ( P ` N ) = ( ( A i^i ( 0 ..^ N ) ) smul B ) )