Theorem mat2pmatbas0

Description: The result of a matrix transformation is a polynomial matrix. (Contributed by AV, 27-Oct-2019)

	Ref	Expression
Hypotheses	mat2pmatbas.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	mat2pmatbas.a	$$⊢A=N\mathrm{Mat}R$$
	mat2pmatbas.b	$$⊢B={\mathrm{Base}}_A$$
	mat2pmatbas.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	mat2pmatbas.c	$$⊢C=N\mathrm{Mat}P$$
	mat2pmatbas0.h	$$⊢H={\mathrm{Base}}_C$$
Assertion	mat2pmatbas0	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to T\left(M\right)\in H$$

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	$$⊢T=N\mathrm{matToPolyMat}R$$
2		mat2pmatbas.a	$$⊢A=N\mathrm{Mat}R$$
3		mat2pmatbas.b	$$⊢B={\mathrm{Base}}_A$$
4		mat2pmatbas.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
5		mat2pmatbas.c	$$⊢C=N\mathrm{Mat}P$$
6		mat2pmatbas0.h	$$⊢H={\mathrm{Base}}_C$$
7	1 2 3 4 5	mat2pmatbas	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to T\left(M\right)\in {\mathrm{Base}}_C$$
8	7 6	eleqtrrdi	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge M\in B\right)\to T\left(M\right)\in H$$