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 = {Poly}_{1} (R)$
		decpmate.c	$⊢ C = N Mat P$
		decpmate.b	$⊢ B = {Base}_{C}$
	Assertion	decpmate	$⊢ ((R \in V \land M \in B \land K \in ℕ_{0}) \land (I \in N \land J \in N)) \to I (M decompPMat K) J = {coe}_{1} (I M J) (K)$

Proof

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