Metamath Proof Explorer

Theorem pmatcollpw3lem

Description: Lemma for pmatcollpw3 and pmatcollpw3fi : Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 8-Dec-2019)

Ref Expression
Hypotheses pmatcollpw.p 
|- P = ( Poly1 ` R )
pmatcollpw.c 
|- C = ( N Mat P )
pmatcollpw.b 
|- B = ( Base ` C )
pmatcollpw.m 
|- .* = ( .s ` C )
pmatcollpw.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
pmatcollpw.x 
|- X = ( var1 ` R )
pmatcollpw.t 
|- T = ( N matToPolyMat R )
pmatcollpw3.a 
|- A = ( N Mat R )
pmatcollpw3.d 
|- D = ( Base ` A )
Assertion pmatcollpw3lem 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( M = ( C gsum ( n e. I |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) -> E. f e. ( D ^m I ) M = ( C gsum ( n e. I |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw.p 
 |-  P = ( Poly1 ` R )
2 pmatcollpw.c 
 |-  C = ( N Mat P )
3 pmatcollpw.b 
 |-  B = ( Base ` C )
4 pmatcollpw.m 
 |-  .* = ( .s ` C )
5 pmatcollpw.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpw.x 
 |-  X = ( var1 ` R )
7 pmatcollpw.t 
 |-  T = ( N matToPolyMat R )
8 pmatcollpw3.a 
 |-  A = ( N Mat R )
9 pmatcollpw3.d 
 |-  D = ( Base ` A )
10 dmeq 
 |-  ( x = y -> dom x = dom y )
11 10 dmeqd 
 |-  ( x = y -> dom dom x = dom dom y )
12 oveq 
 |-  ( x = y -> ( i x j ) = ( i y j ) )
13 12 fveq2d 
 |-  ( x = y -> ( coe1 ` ( i x j ) ) = ( coe1 ` ( i y j ) ) )
14 13 fveq1d 
 |-  ( x = y -> ( ( coe1 ` ( i x j ) ) ` k ) = ( ( coe1 ` ( i y j ) ) ` k ) )
15 11 11 14 mpoeq123dv 
 |-  ( x = y -> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) = ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` k ) ) )
16 fveq2 
 |-  ( k = l -> ( ( coe1 ` ( i y j ) ) ` k ) = ( ( coe1 ` ( i y j ) ) ` l ) )
17 16 mpoeq3dv 
 |-  ( k = l -> ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` k ) ) = ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` l ) ) )
18 15 17 cbvmpov 
 |-  ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) = ( y e. B , l e. I |-> ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` l ) ) )
19 dmexg 
 |-  ( y e. B -> dom y e. _V )
20 19 dmexd 
 |-  ( y e. B -> dom dom y e. _V )
21 20 20 jca 
 |-  ( y e. B -> ( dom dom y e. _V /\ dom dom y e. _V ) )
22 21 ad2antrl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ ( y e. B /\ l e. I ) ) -> ( dom dom y e. _V /\ dom dom y e. _V ) )
23 mpoexga 
 |-  ( ( dom dom y e. _V /\ dom dom y e. _V ) -> ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` l ) ) e. _V )
24 22 23 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ ( y e. B /\ l e. I ) ) -> ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` l ) ) e. _V )
25 24 ralrimivva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> A. y e. B A. l e. I ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` l ) ) e. _V )
26 simprr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> I =/= (/) )
27 nn0ex 
 |-  NN0 e. _V
28 27 ssex 
 |-  ( I C_ NN0 -> I e. _V )
29 28 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> I e. _V )
30 simp3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> M e. B )
31 30 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> M e. B )
32 18 25 26 29 31 mpocurryvald 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) = ( l e. I |-> [_ M / y ]_ ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` l ) ) ) )
33 fveq2 
 |-  ( l = k -> ( ( coe1 ` ( i y j ) ) ` l ) = ( ( coe1 ` ( i y j ) ) ` k ) )
34 33 mpoeq3dv 
 |-  ( l = k -> ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` l ) ) = ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` k ) ) )
35 34 csbeq2dv 
 |-  ( l = k -> [_ M / y ]_ ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` l ) ) = [_ M / y ]_ ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` k ) ) )
36 eqcom 
 |-  ( x = y <-> y = x )
37 eqcom 
 |-  ( ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) = ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` k ) ) <-> ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` k ) ) = ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) )
38 15 36 37 3imtr3i 
 |-  ( y = x -> ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` k ) ) = ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) )
39 38 cbvcsbv 
 |-  [_ M / y ]_ ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` k ) ) = [_ M / x ]_ ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) )
40 35 39 eqtrdi 
 |-  ( l = k -> [_ M / y ]_ ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` l ) ) = [_ M / x ]_ ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) )
41 40 cbvmptv 
 |-  ( l e. I |-> [_ M / y ]_ ( i e. dom dom y , j e. dom dom y |-> ( ( coe1 ` ( i y j ) ) ` l ) ) ) = ( k e. I |-> [_ M / x ]_ ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) )
42 32 41 eqtrdi 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) = ( k e. I |-> [_ M / x ]_ ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) )
43 dmeq 
 |-  ( x = M -> dom x = dom M )
44 43 dmeqd 
 |-  ( x = M -> dom dom x = dom dom M )
45 oveq 
 |-  ( x = M -> ( i x j ) = ( i M j ) )
46 45 fveq2d 
 |-  ( x = M -> ( coe1 ` ( i x j ) ) = ( coe1 ` ( i M j ) ) )
47 46 fveq1d 
 |-  ( x = M -> ( ( coe1 ` ( i x j ) ) ` k ) = ( ( coe1 ` ( i M j ) ) ` k ) )
48 44 44 47 mpoeq123dv 
 |-  ( x = M -> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) = ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` k ) ) )
49 48 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ x = M ) -> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) = ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` k ) ) )
50 30 49 csbied 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> [_ M / x ]_ ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) = ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` k ) ) )
51 eqid 
 |-  ( Base ` P ) = ( Base ` P )
52 2 51 3 matbas2i 
 |-  ( M e. B -> M e. ( ( Base ` P ) ^m ( N X. N ) ) )
53 elmapi 
 |-  ( M e. ( ( Base ` P ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` P ) )
54 fdm 
 |-  ( M : ( N X. N ) --> ( Base ` P ) -> dom M = ( N X. N ) )
55 54 dmeqd 
 |-  ( M : ( N X. N ) --> ( Base ` P ) -> dom dom M = dom ( N X. N ) )
56 dmxpid 
 |-  dom ( N X. N ) = N
57 55 56 eqtr2di 
 |-  ( M : ( N X. N ) --> ( Base ` P ) -> N = dom dom M )
58 52 53 57 3syl 
 |-  ( M e. B -> N = dom dom M )
59 58 3ad2ant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> N = dom dom M )
60 59 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ m = M ) -> N = dom dom M )
61 simpr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ m = M ) -> m = M )
62 61 oveqd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ m = M ) -> ( i m j ) = ( i M j ) )
63 62 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ m = M ) -> ( coe1 ` ( i m j ) ) = ( coe1 ` ( i M j ) ) )
64 63 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ m = M ) -> ( ( coe1 ` ( i m j ) ) ` k ) = ( ( coe1 ` ( i M j ) ) ` k ) )
65 60 60 64 mpoeq123dv 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ m = M ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) = ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` k ) ) )
66 30 65 csbied 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) = ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` k ) ) )
67 50 66 eqtr4d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> [_ M / x ]_ ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) = [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) )
68 67 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> [_ M / x ]_ ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) = [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) )
69 68 mpteq2dv 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( k e. I |-> [_ M / x ]_ ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) = ( k e. I |-> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) ) )
70 42 69 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) = ( k e. I |-> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) ) )
71 oveq 
 |-  ( m = M -> ( i m j ) = ( i M j ) )
72 71 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ m = M ) -> ( i m j ) = ( i M j ) )
73 72 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ m = M ) -> ( coe1 ` ( i m j ) ) = ( coe1 ` ( i M j ) ) )
74 73 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ m = M ) -> ( ( coe1 ` ( i m j ) ) ` k ) = ( ( coe1 ` ( i M j ) ) ` k ) )
75 74 mpoeq3dv 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ m = M ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` k ) ) )
76 30 75 csbied 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` k ) ) )
77 76 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) -> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` k ) ) )
78 eqid 
 |-  ( Base ` R ) = ( Base ` R )
79 simpll1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) -> N e. Fin )
80 simpll2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) -> R e. CRing )
81 simp2 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) /\ i e. N /\ j e. N ) -> i e. N )
82 simp3 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) /\ i e. N /\ j e. N ) -> j e. N )
83 31 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) -> M e. B )
84 83 3ad2ant1 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) /\ i e. N /\ j e. N ) -> M e. B )
85 2 51 3 81 82 84 matecld 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) /\ i e. N /\ j e. N ) -> ( i M j ) e. ( Base ` P ) )
86 ssel 
 |-  ( I C_ NN0 -> ( k e. I -> k e. NN0 ) )
87 86 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( k e. I -> k e. NN0 ) )
88 87 imp 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) -> k e. NN0 )
89 88 3ad2ant1 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) /\ i e. N /\ j e. N ) -> k e. NN0 )
90 eqid 
 |-  ( coe1 ` ( i M j ) ) = ( coe1 ` ( i M j ) )
91 90 51 1 78 coe1fvalcl 
 |-  ( ( ( i M j ) e. ( Base ` P ) /\ k e. NN0 ) -> ( ( coe1 ` ( i M j ) ) ` k ) e. ( Base ` R ) )
92 85 89 91 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i M j ) ) ` k ) e. ( Base ` R ) )
93 8 78 9 79 80 92 matbas2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` k ) ) e. D )
94 77 93 eqeltrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ k e. I ) -> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) e. D )
95 94 fmpttd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( k e. I |-> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) ) : I --> D )
96 9 fvexi 
 |-  D e. _V
97 96 a1i 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> D e. _V )
98 28 adantr 
 |-  ( ( I C_ NN0 /\ I =/= (/) ) -> I e. _V )
99 elmapg 
 |-  ( ( D e. _V /\ I e. _V ) -> ( ( k e. I |-> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) ) e. ( D ^m I ) <-> ( k e. I |-> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) ) : I --> D ) )
100 97 98 99 syl2an 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( ( k e. I |-> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) ) e. ( D ^m I ) <-> ( k e. I |-> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) ) : I --> D ) )
101 95 100 mpbird 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( k e. I |-> [_ M / m ]_ ( i e. N , j e. N |-> ( ( coe1 ` ( i m j ) ) ` k ) ) ) e. ( D ^m I ) )
102 70 101 eqeltrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) e. ( D ^m I ) )
103 fveq1 
 |-  ( f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) -> ( f ` n ) = ( ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ` n ) )
104 103 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) -> ( f ` n ) = ( ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ` n ) )
105 104 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) /\ n e. I ) -> ( f ` n ) = ( ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ` n ) )
106 eqid 
 |-  ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) = ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) )
107 dmexg 
 |-  ( x e. B -> dom x e. _V )
108 107 dmexd 
 |-  ( x e. B -> dom dom x e. _V )
109 108 108 jca 
 |-  ( x e. B -> ( dom dom x e. _V /\ dom dom x e. _V ) )
110 109 ad2antrl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) /\ ( x e. B /\ k e. I ) ) -> ( dom dom x e. _V /\ dom dom x e. _V ) )
111 mpoexga 
 |-  ( ( dom dom x e. _V /\ dom dom x e. _V ) -> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) e. _V )
112 110 111 syl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) /\ ( x e. B /\ k e. I ) ) -> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) e. _V )
113 112 ralrimivva 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) -> A. x e. B A. k e. I ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) e. _V )
114 29 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) -> I e. _V )
115 31 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) -> M e. B )
116 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) -> n e. I )
117 106 113 114 115 116 fvmpocurryd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) -> ( ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ` n ) = ( M ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) n ) )
118 df-decpmat 
 |-  decompPMat = ( x e. _V , k e. NN0 |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) )
119 118 reseq1i 
 |-  ( decompPMat |` ( B X. I ) ) = ( ( x e. _V , k e. NN0 |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) |` ( B X. I ) )
120 ssv 
 |-  B C_ _V
121 120 a1i 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> B C_ _V )
122 simpl 
 |-  ( ( I C_ NN0 /\ I =/= (/) ) -> I C_ NN0 )
123 121 122 anim12i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( B C_ _V /\ I C_ NN0 ) )
124 123 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) -> ( B C_ _V /\ I C_ NN0 ) )
125 resmpo 
 |-  ( ( B C_ _V /\ I C_ NN0 ) -> ( ( x e. _V , k e. NN0 |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) |` ( B X. I ) ) = ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) )
126 124 125 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) -> ( ( x e. _V , k e. NN0 |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) |` ( B X. I ) ) = ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) )
127 119 126 syl5req 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) -> ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) = ( decompPMat |` ( B X. I ) ) )
128 127 oveqd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) -> ( M ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) n ) = ( M ( decompPMat |` ( B X. I ) ) n ) )
129 117 128 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ n e. I ) -> ( ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ` n ) = ( M ( decompPMat |` ( B X. I ) ) n ) )
130 129 adantlr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) /\ n e. I ) -> ( ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ` n ) = ( M ( decompPMat |` ( B X. I ) ) n ) )
131 105 130 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) /\ n e. I ) -> ( f ` n ) = ( M ( decompPMat |` ( B X. I ) ) n ) )
132 131 fveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) /\ n e. I ) -> ( T ` ( f ` n ) ) = ( T ` ( M ( decompPMat |` ( B X. I ) ) n ) ) )
133 30 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) -> M e. B )
134 ovres 
 |-  ( ( M e. B /\ n e. I ) -> ( M ( decompPMat |` ( B X. I ) ) n ) = ( M decompPMat n ) )
135 133 134 sylan 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) /\ n e. I ) -> ( M ( decompPMat |` ( B X. I ) ) n ) = ( M decompPMat n ) )
136 135 fveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) /\ n e. I ) -> ( T ` ( M ( decompPMat |` ( B X. I ) ) n ) ) = ( T ` ( M decompPMat n ) ) )
137 132 136 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) /\ n e. I ) -> ( T ` ( f ` n ) ) = ( T ` ( M decompPMat n ) ) )
138 137 oveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) /\ n e. I ) -> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) = ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) )
139 138 mpteq2dva 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) -> ( n e. I |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) = ( n e. I |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) )
140 139 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) -> ( C gsum ( n e. I |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) = ( C gsum ( n e. I |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
141 140 eqeq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) /\ f = ( curry ( x e. B , k e. I |-> ( i e. dom dom x , j e. dom dom x |-> ( ( coe1 ` ( i x j ) ) ` k ) ) ) ` M ) ) -> ( M = ( C gsum ( n e. I |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) <-> M = ( C gsum ( n e. I |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) ) )
142 102 141 rspcedv 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( I C_ NN0 /\ I =/= (/) ) ) -> ( M = ( C gsum ( n e. I |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) -> E. f e. ( D ^m I ) M = ( C gsum ( n e. I |-> ( ( n .^ X ) .* ( T ` ( f ` n ) ) ) ) ) ) )