Metamath Proof Explorer

Theorem pm2mp

Description: The transformation of a sum of matrices having scaled monomials with the same power as entries into a sum of scaled monomials as a polynomial over matrices. (Contributed by AV, 12-Nov-2019) (Revised by AV, 7-Dec-2019)

Ref Expression
Hypotheses monmat2matmon.p 
|- P = ( Poly1 ` R )
monmat2matmon.c 
|- C = ( N Mat P )
monmat2matmon.b 
|- B = ( Base ` C )
monmat2matmon.m1 
|- .* = ( .s ` Q )
monmat2matmon.e1 
|- .^ = ( .g ` ( mulGrp ` Q ) )
monmat2matmon.x 
|- X = ( var1 ` A )
monmat2matmon.a 
|- A = ( N Mat R )
monmat2matmon.k 
|- K = ( Base ` A )
monmat2matmon.q 
|- Q = ( Poly1 ` A )
monmat2matmon.i 
|- I = ( N pMatToMatPoly R )
monmat2matmon.e2 
|- E = ( .g ` ( mulGrp ` P ) )
monmat2matmon.y 
|- Y = ( var1 ` R )
monmat2matmon.m2 
|- .x. = ( .s ` C )
monmat2matmon.t 
|- T = ( N matToPolyMat R )
Assertion pm2mp 
|- ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> ( I ` ( C gsum ( n e. NN0 |-> ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( M ` n ) .* ( n .^ X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 monmat2matmon.p 
 |-  P = ( Poly1 ` R )
2 monmat2matmon.c 
 |-  C = ( N Mat P )
3 monmat2matmon.b 
 |-  B = ( Base ` C )
4 monmat2matmon.m1 
 |-  .* = ( .s ` Q )
5 monmat2matmon.e1 
 |-  .^ = ( .g ` ( mulGrp ` Q ) )
6 monmat2matmon.x 
 |-  X = ( var1 ` A )
7 monmat2matmon.a 
 |-  A = ( N Mat R )
8 monmat2matmon.k 
 |-  K = ( Base ` A )
9 monmat2matmon.q 
 |-  Q = ( Poly1 ` A )
10 monmat2matmon.i 
 |-  I = ( N pMatToMatPoly R )
11 monmat2matmon.e2 
 |-  E = ( .g ` ( mulGrp ` P ) )
12 monmat2matmon.y 
 |-  Y = ( var1 ` R )
13 monmat2matmon.m2 
 |-  .x. = ( .s ` C )
14 monmat2matmon.t 
 |-  T = ( N matToPolyMat R )
15 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
16 crngring 
 |-  ( R e. CRing -> R e. Ring )
17 16 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
18 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
19 ringcmn 
 |-  ( C e. Ring -> C e. CMnd )
20 17 18 19 3syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> C e. CMnd )
21 20 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> C e. CMnd )
22 7 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
23 16 22 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
24 9 ply1ring 
 |-  ( A e. Ring -> Q e. Ring )
25 ringmnd 
 |-  ( Q e. Ring -> Q e. Mnd )
26 23 24 25 3syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Q e. Mnd )
27 26 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> Q e. Mnd )
28 nn0ex 
 |-  NN0 e. _V
29 28 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> NN0 e. _V )
30 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
31 1 2 3 4 5 6 7 9 30 10 pm2mpghm 
 |-  ( ( N e. Fin /\ R e. Ring ) -> I e. ( C GrpHom Q ) )
32 16 31 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> I e. ( C GrpHom Q ) )
33 32 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> I e. ( C GrpHom Q ) )
34 ghmmhm 
 |-  ( I e. ( C GrpHom Q ) -> I e. ( C MndHom Q ) )
35 33 34 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> I e. ( C MndHom Q ) )
36 17 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> ( N e. Fin /\ R e. Ring ) )
37 36 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) /\ n e. NN0 ) -> ( N e. Fin /\ R e. Ring ) )
38 elmapi 
 |-  ( M e. ( K ^m NN0 ) -> M : NN0 --> K )
39 38 adantr 
 |-  ( ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) -> M : NN0 --> K )
40 39 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> M : NN0 --> K )
41 40 ffvelrnda 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) /\ n e. NN0 ) -> ( M ` n ) e. K )
42 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) /\ n e. NN0 ) -> n e. NN0 )
43 7 8 14 1 2 3 13 11 12 mat2pmatscmxcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( M ` n ) e. K /\ n e. NN0 ) ) -> ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) e. B )
44 37 41 42 43 syl12anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) /\ n e. NN0 ) -> ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) e. B )
45 fvexd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> ( 0g ` C ) e. _V )
46 ovexd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) /\ n e. NN0 ) -> ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) e. _V )
47 simpr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) -> M e. ( K ^m NN0 ) )
48 fvex 
 |-  ( 0g ` A ) e. _V
49 fsuppmapnn0ub 
 |-  ( ( M e. ( K ^m NN0 ) /\ ( 0g ` A ) e. _V ) -> ( M finSupp ( 0g ` A ) -> E. y e. NN0 A. x e. NN0 ( y < x -> ( M ` x ) = ( 0g ` A ) ) ) )
50 47 48 49 sylancl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) -> ( M finSupp ( 0g ` A ) -> E. y e. NN0 A. x e. NN0 ( y < x -> ( M ` x ) = ( 0g ` A ) ) ) )
51 csbov12g 
 |-  ( x e. NN0 -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( [_ x / n ]_ ( n E Y ) .x. [_ x / n ]_ ( T ` ( M ` n ) ) ) )
52 csbov1g 
 |-  ( x e. NN0 -> [_ x / n ]_ ( n E Y ) = ( [_ x / n ]_ n E Y ) )
53 csbvarg 
 |-  ( x e. NN0 -> [_ x / n ]_ n = x )
54 53 oveq1d 
 |-  ( x e. NN0 -> ( [_ x / n ]_ n E Y ) = ( x E Y ) )
55 52 54 eqtrd 
 |-  ( x e. NN0 -> [_ x / n ]_ ( n E Y ) = ( x E Y ) )
56 csbfv2g 
 |-  ( x e. NN0 -> [_ x / n ]_ ( T ` ( M ` n ) ) = ( T ` [_ x / n ]_ ( M ` n ) ) )
57 csbfv2g 
 |-  ( x e. NN0 -> [_ x / n ]_ ( M ` n ) = ( M ` [_ x / n ]_ n ) )
58 53 fveq2d 
 |-  ( x e. NN0 -> ( M ` [_ x / n ]_ n ) = ( M ` x ) )
59 57 58 eqtrd 
 |-  ( x e. NN0 -> [_ x / n ]_ ( M ` n ) = ( M ` x ) )
60 59 fveq2d 
 |-  ( x e. NN0 -> ( T ` [_ x / n ]_ ( M ` n ) ) = ( T ` ( M ` x ) ) )
61 56 60 eqtrd 
 |-  ( x e. NN0 -> [_ x / n ]_ ( T ` ( M ` n ) ) = ( T ` ( M ` x ) ) )
62 55 61 oveq12d 
 |-  ( x e. NN0 -> ( [_ x / n ]_ ( n E Y ) .x. [_ x / n ]_ ( T ` ( M ` n ) ) ) = ( ( x E Y ) .x. ( T ` ( M ` x ) ) ) )
63 51 62 eqtrd 
 |-  ( x e. NN0 -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( ( x E Y ) .x. ( T ` ( M ` x ) ) ) )
64 63 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( ( x E Y ) .x. ( T ` ( M ` x ) ) ) )
65 64 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) /\ ( M ` x ) = ( 0g ` A ) ) -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( ( x E Y ) .x. ( T ` ( M ` x ) ) ) )
66 fveq2 
 |-  ( ( M ` x ) = ( 0g ` A ) -> ( T ` ( M ` x ) ) = ( T ` ( 0g ` A ) ) )
67 66 oveq2d 
 |-  ( ( M ` x ) = ( 0g ` A ) -> ( ( x E Y ) .x. ( T ` ( M ` x ) ) ) = ( ( x E Y ) .x. ( T ` ( 0g ` A ) ) ) )
68 14 7 8 1 2 3 mat2pmatghm 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom C ) )
69 16 68 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( A GrpHom C ) )
70 69 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> T e. ( A GrpHom C ) )
71 ghmmhm 
 |-  ( T e. ( A GrpHom C ) -> T e. ( A MndHom C ) )
72 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
73 72 15 mhm0 
 |-  ( T e. ( A MndHom C ) -> ( T ` ( 0g ` A ) ) = ( 0g ` C ) )
74 70 71 73 3syl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( T ` ( 0g ` A ) ) = ( 0g ` C ) )
75 74 oveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( ( x E Y ) .x. ( T ` ( 0g ` A ) ) ) = ( ( x E Y ) .x. ( 0g ` C ) ) )
76 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
77 16 76 syl 
 |-  ( R e. CRing -> P e. Ring )
78 2 matlmod 
 |-  ( ( N e. Fin /\ P e. Ring ) -> C e. LMod )
79 77 78 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> C e. LMod )
80 79 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> C e. LMod )
81 77 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. Ring )
82 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
83 82 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
84 81 83 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( mulGrp ` P ) e. Mnd )
85 84 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( mulGrp ` P ) e. Mnd )
86 simpr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> x e. NN0 )
87 16 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
88 eqid 
 |-  ( Base ` P ) = ( Base ` P )
89 12 1 88 vr1cl 
 |-  ( R e. Ring -> Y e. ( Base ` P ) )
90 87 89 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. ( Base ` P ) )
91 90 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> Y e. ( Base ` P ) )
92 82 88 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
93 92 11 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ x e. NN0 /\ Y e. ( Base ` P ) ) -> ( x E Y ) e. ( Base ` P ) )
94 85 86 91 93 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( x E Y ) e. ( Base ` P ) )
95 1 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
96 2 matsca2 
 |-  ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` C ) )
97 95 96 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P = ( Scalar ` C ) )
98 97 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Scalar ` C ) = P )
99 98 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( Scalar ` C ) = P )
100 99 fveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( Base ` ( Scalar ` C ) ) = ( Base ` P ) )
101 94 100 eleqtrrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( x E Y ) e. ( Base ` ( Scalar ` C ) ) )
102 eqid 
 |-  ( Scalar ` C ) = ( Scalar ` C )
103 eqid 
 |-  ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
104 102 13 103 15 lmodvs0 
 |-  ( ( C e. LMod /\ ( x E Y ) e. ( Base ` ( Scalar ` C ) ) ) -> ( ( x E Y ) .x. ( 0g ` C ) ) = ( 0g ` C ) )
105 80 101 104 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( ( x E Y ) .x. ( 0g ` C ) ) = ( 0g ` C ) )
106 75 105 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( ( x E Y ) .x. ( T ` ( 0g ` A ) ) ) = ( 0g ` C ) )
107 67 106 sylan9eqr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) /\ ( M ` x ) = ( 0g ` A ) ) -> ( ( x E Y ) .x. ( T ` ( M ` x ) ) ) = ( 0g ` C ) )
108 65 107 eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) /\ ( M ` x ) = ( 0g ` A ) ) -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( 0g ` C ) )
109 108 ex 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( ( M ` x ) = ( 0g ` A ) -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( 0g ` C ) ) )
110 109 imim2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) /\ x e. NN0 ) -> ( ( y < x -> ( M ` x ) = ( 0g ` A ) ) -> ( y < x -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( 0g ` C ) ) ) )
111 110 ralimdva 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) /\ y e. NN0 ) -> ( A. x e. NN0 ( y < x -> ( M ` x ) = ( 0g ` A ) ) -> A. x e. NN0 ( y < x -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( 0g ` C ) ) ) )
112 111 reximdva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) -> ( E. y e. NN0 A. x e. NN0 ( y < x -> ( M ` x ) = ( 0g ` A ) ) -> E. y e. NN0 A. x e. NN0 ( y < x -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( 0g ` C ) ) ) )
113 50 112 syld 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ M e. ( K ^m NN0 ) ) -> ( M finSupp ( 0g ` A ) -> E. y e. NN0 A. x e. NN0 ( y < x -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( 0g ` C ) ) ) )
114 113 impr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> E. y e. NN0 A. x e. NN0 ( y < x -> [_ x / n ]_ ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) = ( 0g ` C ) ) )
115 45 46 114 mptnn0fsupp 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> ( n e. NN0 |-> ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) ) finSupp ( 0g ` C ) )
116 3 15 21 27 29 35 44 115 gsummptmhm 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> ( Q gsum ( n e. NN0 |-> ( I ` ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) ) ) ) = ( I ` ( C gsum ( n e. NN0 |-> ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) ) ) ) )
117 simpll 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) /\ n e. NN0 ) -> ( N e. Fin /\ R e. CRing ) )
118 1 2 3 4 5 6 7 8 9 10 11 12 13 14 monmat2matmon 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( ( M ` n ) e. K /\ n e. NN0 ) ) -> ( I ` ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) ) = ( ( M ` n ) .* ( n .^ X ) ) )
119 117 41 42 118 syl12anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) /\ n e. NN0 ) -> ( I ` ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) ) = ( ( M ` n ) .* ( n .^ X ) ) )
120 119 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> ( n e. NN0 |-> ( I ` ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) ) ) = ( n e. NN0 |-> ( ( M ` n ) .* ( n .^ X ) ) ) )
121 120 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> ( Q gsum ( n e. NN0 |-> ( I ` ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( M ` n ) .* ( n .^ X ) ) ) ) )
122 116 121 eqtr3d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. ( K ^m NN0 ) /\ M finSupp ( 0g ` A ) ) ) -> ( I ` ( C gsum ( n e. NN0 |-> ( ( n E Y ) .x. ( T ` ( M ` n ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( M ` n ) .* ( n .^ X ) ) ) ) )