Metamath Proof Explorer

Theorem smueqlem

Description: Any element of a sequence multiplication only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 20-Sep-2016)

Ref Expression
Hypotheses smueq.a 
|- ( ph -> A C_ NN0 )
smueq.b 
|- ( ph -> B C_ NN0 )
smueq.n 
|- ( ph -> N e. NN0 )
smueq.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 ) ) ) )
smueq.q 
|- Q = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. ( B i^i ( 0 ..^ N ) ) ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
Assertion smueqlem 
|- ( ph -> ( ( A smul B ) i^i ( 0 ..^ N ) ) = ( ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )

Proof

Step Hyp Ref Expression
1 smueq.a 
 |-  ( ph -> A C_ NN0 )
2 smueq.b 
 |-  ( ph -> B C_ NN0 )
3 smueq.n 
 |-  ( ph -> N e. NN0 )
4 smueq.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 ) ) ) )
5 smueq.q 
 |-  Q = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. ( B i^i ( 0 ..^ N ) ) ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
6 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> A C_ NN0 )
7 2 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> B C_ NN0 )
8 elfzouz 
 |-  ( k e. ( 0 ..^ N ) -> k e. ( ZZ>= ` 0 ) )
9 8 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ( ZZ>= ` 0 ) )
10 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
11 9 10 eleqtrrdi 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. NN0 )
12 11 nn0zd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ZZ )
13 12 peano2zd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k + 1 ) e. ZZ )
14 3 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> N e. NN0 )
15 14 nn0zd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> N e. ZZ )
16 elfzolt2 
 |-  ( k e. ( 0 ..^ N ) -> k < N )
17 16 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k < N )
18 nn0ltp1le 
 |-  ( ( k e. NN0 /\ N e. NN0 ) -> ( k < N <-> ( k + 1 ) <_ N ) )
19 11 14 18 syl2anc 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k < N <-> ( k + 1 ) <_ N ) )
20 17 19 mpbid 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k + 1 ) <_ N )
21 eluz2 
 |-  ( N e. ( ZZ>= ` ( k + 1 ) ) <-> ( ( k + 1 ) e. ZZ /\ N e. ZZ /\ ( k + 1 ) <_ N ) )
22 13 15 20 21 syl3anbrc 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> N e. ( ZZ>= ` ( k + 1 ) ) )
23 6 7 4 11 22 smuval2 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k e. ( A smul B ) <-> k e. ( P ` N ) ) )
24 3 10 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
25 eluzfz2b 
 |-  ( N e. ( ZZ>= ` 0 ) <-> N e. ( 0 ... N ) )
26 24 25 sylib 
 |-  ( ph -> N e. ( 0 ... N ) )
27 fveq2 
 |-  ( x = 0 -> ( P ` x ) = ( P ` 0 ) )
28 27 ineq1d 
 |-  ( x = 0 -> ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( P ` 0 ) i^i ( 0 ..^ N ) ) )
29 fveq2 
 |-  ( x = 0 -> ( Q ` x ) = ( Q ` 0 ) )
30 29 ineq1d 
 |-  ( x = 0 -> ( ( Q ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` 0 ) i^i ( 0 ..^ N ) ) )
31 28 30 eqeq12d 
 |-  ( x = 0 -> ( ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` x ) i^i ( 0 ..^ N ) ) <-> ( ( P ` 0 ) i^i ( 0 ..^ N ) ) = ( ( Q ` 0 ) i^i ( 0 ..^ N ) ) ) )
32 31 imbi2d 
 |-  ( x = 0 -> ( ( ph -> ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` x ) i^i ( 0 ..^ N ) ) ) <-> ( ph -> ( ( P ` 0 ) i^i ( 0 ..^ N ) ) = ( ( Q ` 0 ) i^i ( 0 ..^ N ) ) ) ) )
33 fveq2 
 |-  ( x = i -> ( P ` x ) = ( P ` i ) )
34 33 ineq1d 
 |-  ( x = i -> ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( P ` i ) i^i ( 0 ..^ N ) ) )
35 fveq2 
 |-  ( x = i -> ( Q ` x ) = ( Q ` i ) )
36 35 ineq1d 
 |-  ( x = i -> ( ( Q ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` i ) i^i ( 0 ..^ N ) ) )
37 34 36 eqeq12d 
 |-  ( x = i -> ( ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` x ) i^i ( 0 ..^ N ) ) <-> ( ( P ` i ) i^i ( 0 ..^ N ) ) = ( ( Q ` i ) i^i ( 0 ..^ N ) ) ) )
38 37 imbi2d 
 |-  ( x = i -> ( ( ph -> ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` x ) i^i ( 0 ..^ N ) ) ) <-> ( ph -> ( ( P ` i ) i^i ( 0 ..^ N ) ) = ( ( Q ` i ) i^i ( 0 ..^ N ) ) ) ) )
39 fveq2 
 |-  ( x = ( i + 1 ) -> ( P ` x ) = ( P ` ( i + 1 ) ) )
40 39 ineq1d 
 |-  ( x = ( i + 1 ) -> ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( P ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) )
41 fveq2 
 |-  ( x = ( i + 1 ) -> ( Q ` x ) = ( Q ` ( i + 1 ) ) )
42 41 ineq1d 
 |-  ( x = ( i + 1 ) -> ( ( Q ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) )
43 40 42 eqeq12d 
 |-  ( x = ( i + 1 ) -> ( ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` x ) i^i ( 0 ..^ N ) ) <-> ( ( P ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) = ( ( Q ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) ) )
44 43 imbi2d 
 |-  ( x = ( i + 1 ) -> ( ( ph -> ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` x ) i^i ( 0 ..^ N ) ) ) <-> ( ph -> ( ( P ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) = ( ( Q ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) ) ) )
45 fveq2 
 |-  ( x = N -> ( P ` x ) = ( P ` N ) )
46 45 ineq1d 
 |-  ( x = N -> ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( P ` N ) i^i ( 0 ..^ N ) ) )
47 fveq2 
 |-  ( x = N -> ( Q ` x ) = ( Q ` N ) )
48 47 ineq1d 
 |-  ( x = N -> ( ( Q ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` N ) i^i ( 0 ..^ N ) ) )
49 46 48 eqeq12d 
 |-  ( x = N -> ( ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` x ) i^i ( 0 ..^ N ) ) <-> ( ( P ` N ) i^i ( 0 ..^ N ) ) = ( ( Q ` N ) i^i ( 0 ..^ N ) ) ) )
50 49 imbi2d 
 |-  ( x = N -> ( ( ph -> ( ( P ` x ) i^i ( 0 ..^ N ) ) = ( ( Q ` x ) i^i ( 0 ..^ N ) ) ) <-> ( ph -> ( ( P ` N ) i^i ( 0 ..^ N ) ) = ( ( Q ` N ) i^i ( 0 ..^ N ) ) ) ) )
51 1 2 4 smup0 
 |-  ( ph -> ( P ` 0 ) = (/) )
52 inss1 
 |-  ( B i^i ( 0 ..^ N ) ) C_ B
53 52 2 sstrid 
 |-  ( ph -> ( B i^i ( 0 ..^ N ) ) C_ NN0 )
54 1 53 5 smup0 
 |-  ( ph -> ( Q ` 0 ) = (/) )
55 51 54 eqtr4d 
 |-  ( ph -> ( P ` 0 ) = ( Q ` 0 ) )
56 55 ineq1d 
 |-  ( ph -> ( ( P ` 0 ) i^i ( 0 ..^ N ) ) = ( ( Q ` 0 ) i^i ( 0 ..^ N ) ) )
57 56 a1i 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( ph -> ( ( P ` 0 ) i^i ( 0 ..^ N ) ) = ( ( Q ` 0 ) i^i ( 0 ..^ N ) ) ) )
58 oveq1 
 |-  ( ( ( P ` i ) i^i ( 0 ..^ N ) ) = ( ( Q ` i ) i^i ( 0 ..^ N ) ) -> ( ( ( P ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) = ( ( ( Q ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) )
59 58 ineq1d 
 |-  ( ( ( P ` i ) i^i ( 0 ..^ N ) ) = ( ( Q ` i ) i^i ( 0 ..^ N ) ) -> ( ( ( ( P ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) = ( ( ( ( Q ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )
60 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> A C_ NN0 )
61 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> B C_ NN0 )
62 elfzonn0 
 |-  ( i e. ( 0 ..^ N ) -> i e. NN0 )
63 62 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> i e. NN0 )
64 60 61 4 63 smupp1 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( P ` ( i + 1 ) ) = ( ( P ` i ) sadd { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } ) )
65 64 ineq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( P ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) = ( ( ( P ` i ) sadd { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } ) i^i ( 0 ..^ N ) ) )
66 1 2 4 smupf 
 |-  ( ph -> P : NN0 --> ~P NN0 )
67 ffvelcdm 
 |-  ( ( P : NN0 --> ~P NN0 /\ i e. NN0 ) -> ( P ` i ) e. ~P NN0 )
68 66 62 67 syl2an 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( P ` i ) e. ~P NN0 )
69 68 elpwid 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( P ` i ) C_ NN0 )
70 ssrab2 
 |-  { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } C_ NN0
71 70 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } C_ NN0 )
72 3 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> N e. NN0 )
73 69 71 72 sadeq 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( ( P ` i ) sadd { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } ) i^i ( 0 ..^ N ) ) = ( ( ( ( P ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )
74 65 73 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( P ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) = ( ( ( ( P ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )
75 53 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( B i^i ( 0 ..^ N ) ) C_ NN0 )
76 60 75 5 63 smupp1 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( Q ` ( i + 1 ) ) = ( ( Q ` i ) sadd { n e. NN0 | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } ) )
77 76 ineq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( Q ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) = ( ( ( Q ` i ) sadd { n e. NN0 | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } ) i^i ( 0 ..^ N ) ) )
78 1 53 5 smupf 
 |-  ( ph -> Q : NN0 --> ~P NN0 )
79 ffvelcdm 
 |-  ( ( Q : NN0 --> ~P NN0 /\ i e. NN0 ) -> ( Q ` i ) e. ~P NN0 )
80 78 62 79 syl2an 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( Q ` i ) e. ~P NN0 )
81 80 elpwid 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( Q ` i ) C_ NN0 )
82 ssrab2 
 |-  { n e. NN0 | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } C_ NN0
83 82 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> { n e. NN0 | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } C_ NN0 )
84 81 83 72 sadeq 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( ( Q ` i ) sadd { n e. NN0 | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } ) i^i ( 0 ..^ N ) ) = ( ( ( ( Q ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )
85 elinel2 
 |-  ( n e. ( NN0 i^i ( 0 ..^ N ) ) -> n e. ( 0 ..^ N ) )
86 61 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> B C_ NN0 )
87 86 sseld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( ( n - i ) e. B -> ( n - i ) e. NN0 ) )
88 elfzo0 
 |-  ( n e. ( 0 ..^ N ) <-> ( n e. NN0 /\ N e. NN /\ n < N ) )
89 88 simp2bi 
 |-  ( n e. ( 0 ..^ N ) -> N e. NN )
90 89 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> N e. NN )
91 elfzonn0 
 |-  ( n e. ( 0 ..^ N ) -> n e. NN0 )
92 91 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> n e. NN0 )
93 92 nn0red 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> n e. RR )
94 63 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> i e. NN0 )
95 94 nn0red 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> i e. RR )
96 93 95 resubcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( n - i ) e. RR )
97 90 nnred 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> N e. RR )
98 94 nn0ge0d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> 0 <_ i )
99 93 95 subge02d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( 0 <_ i <-> ( n - i ) <_ n ) )
100 98 99 mpbid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( n - i ) <_ n )
101 elfzolt2 
 |-  ( n e. ( 0 ..^ N ) -> n < N )
102 101 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> n < N )
103 96 93 97 100 102 lelttrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( n - i ) < N )
104 90 103 jca 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( N e. NN /\ ( n - i ) < N ) )
105 elfzo0 
 |-  ( ( n - i ) e. ( 0 ..^ N ) <-> ( ( n - i ) e. NN0 /\ N e. NN /\ ( n - i ) < N ) )
106 3anass 
 |-  ( ( ( n - i ) e. NN0 /\ N e. NN /\ ( n - i ) < N ) <-> ( ( n - i ) e. NN0 /\ ( N e. NN /\ ( n - i ) < N ) ) )
107 105 106 bitri 
 |-  ( ( n - i ) e. ( 0 ..^ N ) <-> ( ( n - i ) e. NN0 /\ ( N e. NN /\ ( n - i ) < N ) ) )
108 107 baib 
 |-  ( ( n - i ) e. NN0 -> ( ( n - i ) e. ( 0 ..^ N ) <-> ( N e. NN /\ ( n - i ) < N ) ) )
109 104 108 syl5ibrcom 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( ( n - i ) e. NN0 -> ( n - i ) e. ( 0 ..^ N ) ) )
110 87 109 syld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( ( n - i ) e. B -> ( n - i ) e. ( 0 ..^ N ) ) )
111 110 pm4.71rd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( ( n - i ) e. B <-> ( ( n - i ) e. ( 0 ..^ N ) /\ ( n - i ) e. B ) ) )
112 ancom 
 |-  ( ( ( n - i ) e. ( 0 ..^ N ) /\ ( n - i ) e. B ) <-> ( ( n - i ) e. B /\ ( n - i ) e. ( 0 ..^ N ) ) )
113 elin 
 |-  ( ( n - i ) e. ( B i^i ( 0 ..^ N ) ) <-> ( ( n - i ) e. B /\ ( n - i ) e. ( 0 ..^ N ) ) )
114 112 113 bitr4i 
 |-  ( ( ( n - i ) e. ( 0 ..^ N ) /\ ( n - i ) e. B ) <-> ( n - i ) e. ( B i^i ( 0 ..^ N ) ) )
115 111 114 bitr2di 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( ( n - i ) e. ( B i^i ( 0 ..^ N ) ) <-> ( n - i ) e. B ) )
116 115 anbi2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( 0 ..^ N ) ) -> ( ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) <-> ( i e. A /\ ( n - i ) e. B ) ) )
117 85 116 sylan2 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ n e. ( NN0 i^i ( 0 ..^ N ) ) ) -> ( ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) <-> ( i e. A /\ ( n - i ) e. B ) ) )
118 117 rabbidva 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> { n e. ( NN0 i^i ( 0 ..^ N ) ) | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } = { n e. ( NN0 i^i ( 0 ..^ N ) ) | ( i e. A /\ ( n - i ) e. B ) } )
119 inrab2 
 |-  ( { n e. NN0 | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } i^i ( 0 ..^ N ) ) = { n e. ( NN0 i^i ( 0 ..^ N ) ) | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) }
120 inrab2 
 |-  ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) = { n e. ( NN0 i^i ( 0 ..^ N ) ) | ( i e. A /\ ( n - i ) e. B ) }
121 118 119 120 3eqtr4g 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( { n e. NN0 | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } i^i ( 0 ..^ N ) ) = ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) )
122 121 oveq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( ( Q ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } i^i ( 0 ..^ N ) ) ) = ( ( ( Q ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) )
123 122 ineq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( ( ( Q ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. ( B i^i ( 0 ..^ N ) ) ) } i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) = ( ( ( ( Q ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )
124 77 84 123 3eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( Q ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) = ( ( ( ( Q ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )
125 74 124 eqeq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( ( P ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) = ( ( Q ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) <-> ( ( ( ( P ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) = ( ( ( ( Q ` i ) i^i ( 0 ..^ N ) ) sadd ( { n e. NN0 | ( i e. A /\ ( n - i ) e. B ) } i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) )
126 59 125 imbitrrid 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( ( P ` i ) i^i ( 0 ..^ N ) ) = ( ( Q ` i ) i^i ( 0 ..^ N ) ) -> ( ( P ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) = ( ( Q ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) ) )
127 126 expcom 
 |-  ( i e. ( 0 ..^ N ) -> ( ph -> ( ( ( P ` i ) i^i ( 0 ..^ N ) ) = ( ( Q ` i ) i^i ( 0 ..^ N ) ) -> ( ( P ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) = ( ( Q ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) ) ) )
128 127 a2d 
 |-  ( i e. ( 0 ..^ N ) -> ( ( ph -> ( ( P ` i ) i^i ( 0 ..^ N ) ) = ( ( Q ` i ) i^i ( 0 ..^ N ) ) ) -> ( ph -> ( ( P ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) = ( ( Q ` ( i + 1 ) ) i^i ( 0 ..^ N ) ) ) ) )
129 32 38 44 50 57 128 fzind2 
 |-  ( N e. ( 0 ... N ) -> ( ph -> ( ( P ` N ) i^i ( 0 ..^ N ) ) = ( ( Q ` N ) i^i ( 0 ..^ N ) ) ) )
130 26 129 mpcom 
 |-  ( ph -> ( ( P ` N ) i^i ( 0 ..^ N ) ) = ( ( Q ` N ) i^i ( 0 ..^ N ) ) )
131 130 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( P ` N ) i^i ( 0 ..^ N ) ) = ( ( Q ` N ) i^i ( 0 ..^ N ) ) )
132 131 eleq2d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k e. ( ( P ` N ) i^i ( 0 ..^ N ) ) <-> k e. ( ( Q ` N ) i^i ( 0 ..^ N ) ) ) )
133 elin 
 |-  ( k e. ( ( P ` N ) i^i ( 0 ..^ N ) ) <-> ( k e. ( P ` N ) /\ k e. ( 0 ..^ N ) ) )
134 133 rbaib 
 |-  ( k e. ( 0 ..^ N ) -> ( k e. ( ( P ` N ) i^i ( 0 ..^ N ) ) <-> k e. ( P ` N ) ) )
135 134 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k e. ( ( P ` N ) i^i ( 0 ..^ N ) ) <-> k e. ( P ` N ) ) )
136 elin 
 |-  ( k e. ( ( Q ` N ) i^i ( 0 ..^ N ) ) <-> ( k e. ( Q ` N ) /\ k e. ( 0 ..^ N ) ) )
137 136 rbaib 
 |-  ( k e. ( 0 ..^ N ) -> ( k e. ( ( Q ` N ) i^i ( 0 ..^ N ) ) <-> k e. ( Q ` N ) ) )
138 137 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k e. ( ( Q ` N ) i^i ( 0 ..^ N ) ) <-> k e. ( Q ` N ) ) )
139 132 135 138 3bitr3d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k e. ( P ` N ) <-> k e. ( Q ` N ) ) )
140 53 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( B i^i ( 0 ..^ N ) ) C_ NN0 )
141 6 140 5 14 smupval 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( Q ` N ) = ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) )
142 141 eleq2d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k e. ( Q ` N ) <-> k e. ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) ) )
143 23 139 142 3bitrd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k e. ( A smul B ) <-> k e. ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) ) )
144 143 ex 
 |-  ( ph -> ( k e. ( 0 ..^ N ) -> ( k e. ( A smul B ) <-> k e. ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) ) ) )
145 144 pm5.32rd 
 |-  ( ph -> ( ( k e. ( A smul B ) /\ k e. ( 0 ..^ N ) ) <-> ( k e. ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) /\ k e. ( 0 ..^ N ) ) ) )
146 elin 
 |-  ( k e. ( ( A smul B ) i^i ( 0 ..^ N ) ) <-> ( k e. ( A smul B ) /\ k e. ( 0 ..^ N ) ) )
147 elin 
 |-  ( k e. ( ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) <-> ( k e. ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) /\ k e. ( 0 ..^ N ) ) )
148 145 146 147 3bitr4g 
 |-  ( ph -> ( k e. ( ( A smul B ) i^i ( 0 ..^ N ) ) <-> k e. ( ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) ) )
149 148 eqrdv 
 |-  ( ph -> ( ( A smul B ) i^i ( 0 ..^ N ) ) = ( ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )