# Metamath Proof Explorer

## Theorem decpmate

Description: An entry of the matrix consisting of the coefficients in the entries of a polynomial matrix is the corresponding coefficient in the polynomial entry of the given matrix. (Contributed by AV, 28-Sep-2019) (Revised by AV, 2-Dec-2019)

Ref Expression
Hypotheses decpmate.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
decpmate.c ${⊢}{C}={N}\mathrm{Mat}{P}$
decpmate.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
Assertion decpmate ${⊢}\left(\left({R}\in {V}\wedge {M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {I}\left({M}\mathrm{decompPMat}{K}\right){J}={\mathrm{coe}}_{1}\left({I}{M}{J}\right)\left({K}\right)$

### Proof

Step Hyp Ref Expression
1 decpmate.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 decpmate.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 decpmate.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 2 3 decpmatval ${⊢}\left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\to {M}\mathrm{decompPMat}{K}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({K}\right)\right)$
5 4 3adant1 ${⊢}\left({R}\in {V}\wedge {M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\to {M}\mathrm{decompPMat}{K}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({K}\right)\right)$
6 5 adantr ${⊢}\left(\left({R}\in {V}\wedge {M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {M}\mathrm{decompPMat}{K}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({K}\right)\right)$
7 oveq12 ${⊢}\left({i}={I}\wedge {j}={J}\right)\to {i}{M}{j}={I}{M}{J}$
8 7 fveq2d ${⊢}\left({i}={I}\wedge {j}={J}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)={\mathrm{coe}}_{1}\left({I}{M}{J}\right)$
9 8 fveq1d ${⊢}\left({i}={I}\wedge {j}={J}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({K}\right)={\mathrm{coe}}_{1}\left({I}{M}{J}\right)\left({K}\right)$
10 9 adantl ${⊢}\left(\left(\left({R}\in {V}\wedge {M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\wedge \left({i}={I}\wedge {j}={J}\right)\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({K}\right)={\mathrm{coe}}_{1}\left({I}{M}{J}\right)\left({K}\right)$
11 simprl ${⊢}\left(\left({R}\in {V}\wedge {M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {I}\in {N}$
12 simprr ${⊢}\left(\left({R}\in {V}\wedge {M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {J}\in {N}$
13 fvexd ${⊢}\left(\left({R}\in {V}\wedge {M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {\mathrm{coe}}_{1}\left({I}{M}{J}\right)\left({K}\right)\in \mathrm{V}$
14 6 10 11 12 13 ovmpod ${⊢}\left(\left({R}\in {V}\wedge {M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {I}\left({M}\mathrm{decompPMat}{K}\right){J}={\mathrm{coe}}_{1}\left({I}{M}{J}\right)\left({K}\right)$