Metamath Proof Explorer

Theorem decpmatval

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

		Ref	Expression
	Hypotheses	decpmatval.a	$⊢ A = N Mat R$
		decpmatval.b	$⊢ B = {Base}_{A}$
	Assertion	decpmatval	$⊢ (M \in B \land K \in ℕ_{0}) \to M decompPMat K = (i \in N, j \in N ⟼ {coe}_{1} (i M j) (K))$

Proof

Step	Hyp	Ref	Expression
1		decpmatval.a	$⊢ A = N Mat R$
2		decpmatval.b	$⊢ B = {Base}_{A}$
3		decpmatval0	$⊢ (M \in B \land K \in ℕ_{0}) \to M decompPMat K = (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (K))$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	1 4 2	matbas2i	$⊢ M \in B \to M \in ({Base}_{R}^{(N \times N)})$
6		elmapi	$⊢ M \in ({Base}_{R}^{(N \times N)}) \to M : N \times N ⟶ {Base}_{R}$
7		fdm	$⊢ M : N \times N ⟶ {Base}_{R} \to dom M = N \times N$
8	7	dmeqd	$⊢ M : N \times N ⟶ {Base}_{R} \to dom dom M = dom (N \times N)$
9		dmxpid	$⊢ dom (N \times N) = N$
10	8 9	syl6eq	$⊢ M : N \times N ⟶ {Base}_{R} \to dom dom M = N$
11	5 6 10	3syl	$⊢ M \in B \to dom dom M = N$
12	11	adantr	$⊢ (M \in B \land K \in ℕ_{0}) \to dom dom M = N$
13		eqidd	$⊢ (M \in B \land K \in ℕ_{0}) \to {coe}_{1} (i M j) (K) = {coe}_{1} (i M j) (K)$
14	12 12 13	mpoeq123dv	$⊢ (M \in B \land K \in ℕ_{0}) \to (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (K)) = (i \in N, j \in N ⟼ {coe}_{1} (i M j) (K))$
15	3 14	eqtrd	$⊢ (M \in B \land K \in ℕ_{0}) \to M decompPMat K = (i \in N, j \in N ⟼ {coe}_{1} (i M j) (K))$