decpmatcl

Description: Closure of the decomposition of a polynomial matrix: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power is a 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}$
	decpmatcl.a	$⊢ A = N Mat R$
	decpmatcl.d	$⊢ D = {Base}_{A}$
Assertion	decpmatcl	$⊢ (R \in V \land M \in B \land K \in ℕ_{0}) \to M decompPMat K \in D$

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		decpmatcl.a	$⊢ A = N Mat R$
5		decpmatcl.d	$⊢ D = {Base}_{A}$
6	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))$
7	6	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))$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	2 3	matrcl	$⊢ M \in B \to (N \in Fin \land P \in V)$
10	9	simpld	$⊢ M \in B \to N \in Fin$
11	10	3ad2ant2	$⊢ (R \in V \land M \in B \land K \in ℕ_{0}) \to N \in Fin$
12		simp1	$⊢ (R \in V \land M \in B \land K \in ℕ_{0}) \to R \in V$
13		eqid	$⊢ {Base}_{P} = {Base}_{P}$
14		simp2	$⊢ ((R \in V \land M \in B \land K \in ℕ_{0}) \land i \in N \land j \in N) \to i \in N$
15		simp3	$⊢ ((R \in V \land M \in B \land K \in ℕ_{0}) \land i \in N \land j \in N) \to j \in N$
16		simp2	$⊢ (R \in V \land M \in B \land K \in ℕ_{0}) \to M \in B$
17	16	3ad2ant1	$⊢ ((R \in V \land M \in B \land K \in ℕ_{0}) \land i \in N \land j \in N) \to M \in B$
18	2 13 3 14 15 17	matecld	$⊢ ((R \in V \land M \in B \land K \in ℕ_{0}) \land i \in N \land j \in N) \to i M j \in {Base}_{P}$
19		simp3	$⊢ (R \in V \land M \in B \land K \in ℕ_{0}) \to K \in ℕ_{0}$
20	19	3ad2ant1	$⊢ ((R \in V \land M \in B \land K \in ℕ_{0}) \land i \in N \land j \in N) \to K \in ℕ_{0}$
21		eqid	$⊢ {coe}_{1} (i M j) = {coe}_{1} (i M j)$
22	21 13 1 8	coe1fvalcl	$⊢ (i M j \in {Base}_{P} \land K \in ℕ_{0}) \to {coe}_{1} (i M j) (K) \in {Base}_{R}$
23	18 20 22	syl2anc	$⊢ ((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 {Base}_{R}$
24	4 8 5 11 12 23	matbas2d	$⊢ (R \in V \land M \in B \land K \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i M j) (K)) \in D$
25	7 24	eqeltrd	$⊢ (R \in V \land M \in B \land K \in ℕ_{0}) \to M decompPMat K \in D$

Metamath Proof Explorer

Theorem decpmatcl

Proof