Metamath Proof Explorer

Theorem decpmatval0

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power, most general version. (Contributed by AV, 2-Dec-2019)

Ref Expression
Assertion decpmatval0 
|- ( ( M e. V /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )

Proof

Step Hyp Ref Expression
1 df-decpmat 
 |-  decompPMat = ( m e. _V , k e. NN0 |-> ( i e. dom dom m , j e. dom dom m |-> ( ( coe1 ` ( i m j ) ) ` k ) ) )
2 1 a1i 
 |-  ( ( M e. V /\ K e. NN0 ) -> decompPMat = ( m e. _V , k e. NN0 |-> ( i e. dom dom m , j e. dom dom m |-> ( ( coe1 ` ( i m j ) ) ` k ) ) ) )
3 dmeq 
 |-  ( m = M -> dom m = dom M )
4 3 adantr 
 |-  ( ( m = M /\ k = K ) -> dom m = dom M )
5 4 dmeqd 
 |-  ( ( m = M /\ k = K ) -> dom dom m = dom dom M )
6 oveq 
 |-  ( m = M -> ( i m j ) = ( i M j ) )
7 6 fveq2d 
 |-  ( m = M -> ( coe1 ` ( i m j ) ) = ( coe1 ` ( i M j ) ) )
8 7 adantr 
 |-  ( ( m = M /\ k = K ) -> ( coe1 ` ( i m j ) ) = ( coe1 ` ( i M j ) ) )
9 simpr 
 |-  ( ( m = M /\ k = K ) -> k = K )
10 8 9 fveq12d 
 |-  ( ( m = M /\ k = K ) -> ( ( coe1 ` ( i m j ) ) ` k ) = ( ( coe1 ` ( i M j ) ) ` K ) )
11 5 5 10 mpoeq123dv 
 |-  ( ( m = M /\ k = K ) -> ( i e. dom dom m , j e. dom dom m |-> ( ( coe1 ` ( i m j ) ) ` k ) ) = ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )
12 11 adantl 
 |-  ( ( ( M e. V /\ K e. NN0 ) /\ ( m = M /\ k = K ) ) -> ( i e. dom dom m , j e. dom dom m |-> ( ( coe1 ` ( i m j ) ) ` k ) ) = ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )
13 elex 
 |-  ( M e. V -> M e. _V )
14 13 adantr 
 |-  ( ( M e. V /\ K e. NN0 ) -> M e. _V )
15 simpr 
 |-  ( ( M e. V /\ K e. NN0 ) -> K e. NN0 )
16 dmexg 
 |-  ( M e. V -> dom M e. _V )
17 16 dmexd 
 |-  ( M e. V -> dom dom M e. _V )
18 17 17 jca 
 |-  ( M e. V -> ( dom dom M e. _V /\ dom dom M e. _V ) )
19 18 adantr 
 |-  ( ( M e. V /\ K e. NN0 ) -> ( dom dom M e. _V /\ dom dom M e. _V ) )
20 mpoexga 
 |-  ( ( dom dom M e. _V /\ dom dom M e. _V ) -> ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` K ) ) e. _V )
21 19 20 syl 
 |-  ( ( M e. V /\ K e. NN0 ) -> ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` K ) ) e. _V )
22 2 12 14 15 21 ovmpod 
 |-  ( ( M e. V /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )