Metamath Proof Explorer

Theorem coe1mul3

Description: The coefficient vector of multiplication in the univariate polynomial ring, at indices high enough that at most one component can be active in the sum. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses coe1mul3.s 
|- Y = ( Poly1 ` R )
coe1mul3.t 
|- .xb = ( .r ` Y )
coe1mul3.u 
|- .x. = ( .r ` R )
coe1mul3.b 
|- B = ( Base ` Y )
coe1mul3.d 
|- D = ( deg1 ` R )
coe1mul3.r 
|- ( ph -> R e. Ring )
coe1mul3.f1 
|- ( ph -> F e. B )
coe1mul3.f2 
|- ( ph -> I e. NN0 )
coe1mul3.f3 
|- ( ph -> ( D ` F ) <_ I )
coe1mul3.g1 
|- ( ph -> G e. B )
coe1mul3.g2 
|- ( ph -> J e. NN0 )
coe1mul3.g3 
|- ( ph -> ( D ` G ) <_ J )
Assertion coe1mul3 
|- ( ph -> ( ( coe1 ` ( F .xb G ) ) ` ( I + J ) ) = ( ( ( coe1 ` F ) ` I ) .x. ( ( coe1 ` G ) ` J ) ) )

Proof

Step Hyp Ref Expression
1 coe1mul3.s 
 |-  Y = ( Poly1 ` R )
2 coe1mul3.t 
 |-  .xb = ( .r ` Y )
3 coe1mul3.u 
 |-  .x. = ( .r ` R )
4 coe1mul3.b 
 |-  B = ( Base ` Y )
5 coe1mul3.d 
 |-  D = ( deg1 ` R )
6 coe1mul3.r 
 |-  ( ph -> R e. Ring )
7 coe1mul3.f1 
 |-  ( ph -> F e. B )
8 coe1mul3.f2 
 |-  ( ph -> I e. NN0 )
9 coe1mul3.f3 
 |-  ( ph -> ( D ` F ) <_ I )
10 coe1mul3.g1 
 |-  ( ph -> G e. B )
11 coe1mul3.g2 
 |-  ( ph -> J e. NN0 )
12 coe1mul3.g3 
 |-  ( ph -> ( D ` G ) <_ J )
13 1 2 3 4 coe1mul 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .xb G ) ) = ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( x - y ) ) ) ) ) ) )
14 6 7 10 13 syl3anc 
 |-  ( ph -> ( coe1 ` ( F .xb G ) ) = ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( x - y ) ) ) ) ) ) )
15 14 fveq1d 
 |-  ( ph -> ( ( coe1 ` ( F .xb G ) ) ` ( I + J ) ) = ( ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( x - y ) ) ) ) ) ) ` ( I + J ) ) )
16 8 11 nn0addcld 
 |-  ( ph -> ( I + J ) e. NN0 )
17 oveq2 
 |-  ( x = ( I + J ) -> ( 0 ... x ) = ( 0 ... ( I + J ) ) )
18 fvoveq1 
 |-  ( x = ( I + J ) -> ( ( coe1 ` G ) ` ( x - y ) ) = ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) )
19 18 oveq2d 
 |-  ( x = ( I + J ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( x - y ) ) ) = ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) )
20 17 19 mpteq12dv 
 |-  ( x = ( I + J ) -> ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( x - y ) ) ) ) = ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) )
21 20 oveq2d 
 |-  ( x = ( I + J ) -> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( x - y ) ) ) ) ) = ( R gsum ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) ) )
22 eqid 
 |-  ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( x - y ) ) ) ) ) ) = ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( x - y ) ) ) ) ) )
23 ovex 
 |-  ( R gsum ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) ) e. _V
24 21 22 23 fvmpt 
 |-  ( ( I + J ) e. NN0 -> ( ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( x - y ) ) ) ) ) ) ` ( I + J ) ) = ( R gsum ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) ) )
25 16 24 syl 
 |-  ( ph -> ( ( x e. NN0 |-> ( R gsum ( y e. ( 0 ... x ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( x - y ) ) ) ) ) ) ` ( I + J ) ) = ( R gsum ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) ) )
26 eqid 
 |-  ( Base ` R ) = ( Base ` R )
27 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
28 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
29 6 28 syl 
 |-  ( ph -> R e. Mnd )
30 ovexd 
 |-  ( ph -> ( 0 ... ( I + J ) ) e. _V )
31 8 nn0red 
 |-  ( ph -> I e. RR )
32 nn0addge1 
 |-  ( ( I e. RR /\ J e. NN0 ) -> I <_ ( I + J ) )
33 31 11 32 syl2anc 
 |-  ( ph -> I <_ ( I + J ) )
34 fznn0 
 |-  ( ( I + J ) e. NN0 -> ( I e. ( 0 ... ( I + J ) ) <-> ( I e. NN0 /\ I <_ ( I + J ) ) ) )
35 16 34 syl 
 |-  ( ph -> ( I e. ( 0 ... ( I + J ) ) <-> ( I e. NN0 /\ I <_ ( I + J ) ) ) )
36 8 33 35 mpbir2and 
 |-  ( ph -> I e. ( 0 ... ( I + J ) ) )
37 6 adantr 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> R e. Ring )
38 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
39 38 4 1 26 coe1f 
 |-  ( F e. B -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
40 7 39 syl 
 |-  ( ph -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
41 elfznn0 
 |-  ( y e. ( 0 ... ( I + J ) ) -> y e. NN0 )
42 ffvelrn 
 |-  ( ( ( coe1 ` F ) : NN0 --> ( Base ` R ) /\ y e. NN0 ) -> ( ( coe1 ` F ) ` y ) e. ( Base ` R ) )
43 40 41 42 syl2an 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( ( coe1 ` F ) ` y ) e. ( Base ` R ) )
44 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
45 44 4 1 26 coe1f 
 |-  ( G e. B -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
46 10 45 syl 
 |-  ( ph -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
47 fznn0sub 
 |-  ( y e. ( 0 ... ( I + J ) ) -> ( ( I + J ) - y ) e. NN0 )
48 ffvelrn 
 |-  ( ( ( coe1 ` G ) : NN0 --> ( Base ` R ) /\ ( ( I + J ) - y ) e. NN0 ) -> ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) e. ( Base ` R ) )
49 46 47 48 syl2an 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) e. ( Base ` R ) )
50 26 3 ringcl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` F ) ` y ) e. ( Base ` R ) /\ ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) e. ( Base ` R ) ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) e. ( Base ` R ) )
51 37 43 49 50 syl3anc 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) e. ( Base ` R ) )
52 51 fmpttd 
 |-  ( ph -> ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) : ( 0 ... ( I + J ) ) --> ( Base ` R ) )
53 eldifsn 
 |-  ( y e. ( ( 0 ... ( I + J ) ) \ { I } ) <-> ( y e. ( 0 ... ( I + J ) ) /\ y =/= I ) )
54 41 adantl 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> y e. NN0 )
55 54 nn0red 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> y e. RR )
56 31 adantr 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> I e. RR )
57 55 56 lttri2d 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( y =/= I <-> ( y < I \/ I < y ) ) )
58 10 ad2antrr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> G e. B )
59 47 adantl 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( ( I + J ) - y ) e. NN0 )
60 59 adantr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> ( ( I + J ) - y ) e. NN0 )
61 5 1 4 deg1xrcl 
 |-  ( G e. B -> ( D ` G ) e. RR* )
62 10 61 syl 
 |-  ( ph -> ( D ` G ) e. RR* )
63 62 ad2antrr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> ( D ` G ) e. RR* )
64 11 nn0red 
 |-  ( ph -> J e. RR )
65 64 rexrd 
 |-  ( ph -> J e. RR* )
66 65 ad2antrr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> J e. RR* )
67 16 nn0red 
 |-  ( ph -> ( I + J ) e. RR )
68 67 adantr 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( I + J ) e. RR )
69 68 55 resubcld 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( ( I + J ) - y ) e. RR )
70 69 rexrd 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( ( I + J ) - y ) e. RR* )
71 70 adantr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> ( ( I + J ) - y ) e. RR* )
72 12 ad2antrr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> ( D ` G ) <_ J )
73 64 adantr 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> J e. RR )
74 55 56 73 ltadd1d 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( y < I <-> ( y + J ) < ( I + J ) ) )
75 55 73 68 ltaddsub2d 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( ( y + J ) < ( I + J ) <-> J < ( ( I + J ) - y ) ) )
76 74 75 bitrd 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( y < I <-> J < ( ( I + J ) - y ) ) )
77 76 biimpa 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> J < ( ( I + J ) - y ) )
78 63 66 71 72 77 xrlelttrd 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> ( D ` G ) < ( ( I + J ) - y ) )
79 5 1 4 27 44 deg1lt 
 |-  ( ( G e. B /\ ( ( I + J ) - y ) e. NN0 /\ ( D ` G ) < ( ( I + J ) - y ) ) -> ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) = ( 0g ` R ) )
80 58 60 78 79 syl3anc 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) = ( 0g ` R ) )
81 80 oveq2d 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( ( ( coe1 ` F ) ` y ) .x. ( 0g ` R ) ) )
82 26 3 27 ringrz 
 |-  ( ( R e. Ring /\ ( ( coe1 ` F ) ` y ) e. ( Base ` R ) ) -> ( ( ( coe1 ` F ) ` y ) .x. ( 0g ` R ) ) = ( 0g ` R ) )
83 37 43 82 syl2anc 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( ( ( coe1 ` F ) ` y ) .x. ( 0g ` R ) ) = ( 0g ` R ) )
84 83 adantr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> ( ( ( coe1 ` F ) ` y ) .x. ( 0g ` R ) ) = ( 0g ` R ) )
85 81 84 eqtrd 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ y < I ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( 0g ` R ) )
86 7 ad2antrr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> F e. B )
87 54 adantr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> y e. NN0 )
88 5 1 4 deg1xrcl 
 |-  ( F e. B -> ( D ` F ) e. RR* )
89 7 88 syl 
 |-  ( ph -> ( D ` F ) e. RR* )
90 89 ad2antrr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> ( D ` F ) e. RR* )
91 31 rexrd 
 |-  ( ph -> I e. RR* )
92 91 ad2antrr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> I e. RR* )
93 55 rexrd 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> y e. RR* )
94 93 adantr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> y e. RR* )
95 9 ad2antrr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> ( D ` F ) <_ I )
96 simpr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> I < y )
97 90 92 94 95 96 xrlelttrd 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> ( D ` F ) < y )
98 5 1 4 27 38 deg1lt 
 |-  ( ( F e. B /\ y e. NN0 /\ ( D ` F ) < y ) -> ( ( coe1 ` F ) ` y ) = ( 0g ` R ) )
99 86 87 97 98 syl3anc 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> ( ( coe1 ` F ) ` y ) = ( 0g ` R ) )
100 99 oveq1d 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( ( 0g ` R ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) )
101 26 3 27 ringlz 
 |-  ( ( R e. Ring /\ ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) e. ( Base ` R ) ) -> ( ( 0g ` R ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( 0g ` R ) )
102 37 49 101 syl2anc 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( ( 0g ` R ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( 0g ` R ) )
103 102 adantr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> ( ( 0g ` R ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( 0g ` R ) )
104 100 103 eqtrd 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ I < y ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( 0g ` R ) )
105 85 104 jaodan 
 |-  ( ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) /\ ( y < I \/ I < y ) ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( 0g ` R ) )
106 105 ex 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( ( y < I \/ I < y ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( 0g ` R ) ) )
107 57 106 sylbid 
 |-  ( ( ph /\ y e. ( 0 ... ( I + J ) ) ) -> ( y =/= I -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( 0g ` R ) ) )
108 107 impr 
 |-  ( ( ph /\ ( y e. ( 0 ... ( I + J ) ) /\ y =/= I ) ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( 0g ` R ) )
109 53 108 sylan2b 
 |-  ( ( ph /\ y e. ( ( 0 ... ( I + J ) ) \ { I } ) ) -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( 0g ` R ) )
110 109 30 suppss2 
 |-  ( ph -> ( ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) supp ( 0g ` R ) ) C_ { I } )
111 26 27 29 30 36 52 110 gsumpt 
 |-  ( ph -> ( R gsum ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) ) = ( ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) ` I ) )
112 fveq2 
 |-  ( y = I -> ( ( coe1 ` F ) ` y ) = ( ( coe1 ` F ) ` I ) )
113 oveq2 
 |-  ( y = I -> ( ( I + J ) - y ) = ( ( I + J ) - I ) )
114 113 fveq2d 
 |-  ( y = I -> ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) = ( ( coe1 ` G ) ` ( ( I + J ) - I ) ) )
115 112 114 oveq12d 
 |-  ( y = I -> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) = ( ( ( coe1 ` F ) ` I ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - I ) ) ) )
116 eqid 
 |-  ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) = ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) )
117 ovex 
 |-  ( ( ( coe1 ` F ) ` I ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - I ) ) ) e. _V
118 115 116 117 fvmpt 
 |-  ( I e. ( 0 ... ( I + J ) ) -> ( ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) ` I ) = ( ( ( coe1 ` F ) ` I ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - I ) ) ) )
119 36 118 syl 
 |-  ( ph -> ( ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) ` I ) = ( ( ( coe1 ` F ) ` I ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - I ) ) ) )
120 8 nn0cnd 
 |-  ( ph -> I e. CC )
121 11 nn0cnd 
 |-  ( ph -> J e. CC )
122 120 121 pncan2d 
 |-  ( ph -> ( ( I + J ) - I ) = J )
123 122 fveq2d 
 |-  ( ph -> ( ( coe1 ` G ) ` ( ( I + J ) - I ) ) = ( ( coe1 ` G ) ` J ) )
124 123 oveq2d 
 |-  ( ph -> ( ( ( coe1 ` F ) ` I ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - I ) ) ) = ( ( ( coe1 ` F ) ` I ) .x. ( ( coe1 ` G ) ` J ) ) )
125 111 119 124 3eqtrd 
 |-  ( ph -> ( R gsum ( y e. ( 0 ... ( I + J ) ) |-> ( ( ( coe1 ` F ) ` y ) .x. ( ( coe1 ` G ) ` ( ( I + J ) - y ) ) ) ) ) = ( ( ( coe1 ` F ) ` I ) .x. ( ( coe1 ` G ) ` J ) ) )
126 15 25 125 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( F .xb G ) ) ` ( I + J ) ) = ( ( ( coe1 ` F ) ` I ) .x. ( ( coe1 ` G ) ` J ) ) )