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={\mathrm{Poly}}_1\left(R\right)$$
	decpmate.c	$$⊢C=N\mathrm{Mat}P$$
	decpmate.b	$$⊢B={\mathrm{Base}}_C$$
	decpmatcl.a	$$⊢A=N\mathrm{Mat}R$$
	decpmatfsupp.0	$$⊢\underset{\dot{}}{0}=0_A$$
Assertion	decpmatfsupp	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼M\mathrm{decompPMat}k\right)\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		decpmatcl.a	$$⊢A=N\mathrm{Mat}R$$
5		decpmatfsupp.0	$$⊢\underset{\dot{}}{0}=0_A$$
6	5	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
7	6	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
8		ovexd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge M\in B\right)\wedge k\in {\mathbb{N}}_0\right)\to M\mathrm{decompPMat}k\in \mathrm{V}$$
9		oveq2	$$⊢k=x\to M\mathrm{decompPMat}k=M\mathrm{decompPMat}x$$
10	1 2 3 4 5	decpmataa0	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to M\mathrm{decompPMat}x=\underset{\dot{}}{0}\right)$$
11	7 8 9 10	mptnn0fsuppd	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼M\mathrm{decompPMat}k\right)\right)$$