Theorem m2cpmf1

Description: The matrix transformation is a 1-1 function from the matrices to the constant polynomial matrices. (Contributed by AV, 18-Nov-2019)

	Ref	Expression
Hypotheses	m2cpm.s	$$⊢S=N\mathrm{ConstPolyMat}R$$
	m2cpm.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	m2cpm.a	$$⊢A=N\mathrm{Mat}R$$
	m2cpm.b	$$⊢B={\mathrm{Base}}_A$$
Assertion	m2cpmf1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B\underset{1-1}{⟶}S$$

Proof

Step	Hyp	Ref	Expression
1		m2cpm.s	$$⊢S=N\mathrm{ConstPolyMat}R$$
2		m2cpm.t	$$⊢T=N\mathrm{matToPolyMat}R$$
3		m2cpm.a	$$⊢A=N\mathrm{Mat}R$$
4		m2cpm.b	$$⊢B={\mathrm{Base}}_A$$
5		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
6		eqid	$$⊢N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)=N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)$$
7		eqid	$$⊢{\mathrm{Base}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}$$
8	2 3 4 5 6 7	mat2pmatf1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B\underset{1-1}{⟶}{\mathrm{Base}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}$$
9	1 2 3 4	m2cpmf	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B⟶S$$
10	9	frnd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to \mathrm{ran}T\subseteq S$$
11		f1ssr	$$⊢\left(T:B\underset{1-1}{⟶}{\mathrm{Base}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\wedge \mathrm{ran}T\subseteq S\right)\to T:B\underset{1-1}{⟶}S$$
12	8 10 11	syl2anc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B\underset{1-1}{⟶}S$$