Metamath Proof Explorer

Theorem decpmatfsupp

Description: The mapping to the matrices consisting of the coefficients in the polynomial entries of a given matrix for the same power is finitely supported. (Contributed by AV, 5-Oct-2019) (Revised by AV, 3-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$
		decpmatfsupp.0	$⊢ \underset{˙}{0} = 0_{A}$
	Assertion	decpmatfsupp	$⊢ (R \in Ring \land M \in B) \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ M decompPMat 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		decpmatcl.a	$⊢ A = N Mat R$
5		decpmatfsupp.0	$⊢ \underset{˙}{0} = 0_{A}$
6	5	fvexi	$⊢ \underset{˙}{0} \in V$
7	6	a1i	$⊢ (R \in Ring \land M \in B) \to \underset{˙}{0} \in V$
8		ovexd	$⊢ ((R \in Ring \land M \in B) \land k \in ℕ_{0}) \to M decompPMat k \in V$
9		oveq2	$⊢ k = x \to M decompPMat k = M decompPMat x$
10	1 2 3 4 5	decpmataa0	$⊢ (R \in Ring \land M \in B) \to \exists s \in ℕ_{0} \forall x \in ℕ_{0} (s < x \to M decompPMat x = \underset{˙}{0})$
11	7 8 9 10	mptnn0fsuppd	$⊢ (R \in Ring \land M \in B) \to {finSupp}_{\underset{˙}{0}} ((k \in ℕ_{0} ⟼ M decompPMat k))$