Theorem m2cpmf1o

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

	Ref	Expression
Hypotheses	m2cpmfo.s	$$⊢S=N\mathrm{ConstPolyMat}R$$
	m2cpmfo.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	m2cpmfo.a	$$⊢A=N\mathrm{Mat}R$$
	m2cpmfo.k	$$⊢K={\mathrm{Base}}_A$$
Assertion	m2cpmf1o	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:K\underset{1-1\; onto}{⟶}S$$

Proof

Step	Hyp	Ref	Expression
1		m2cpmfo.s	$$⊢S=N\mathrm{ConstPolyMat}R$$
2		m2cpmfo.t	$$⊢T=N\mathrm{matToPolyMat}R$$
3		m2cpmfo.a	$$⊢A=N\mathrm{Mat}R$$
4		m2cpmfo.k	$$⊢K={\mathrm{Base}}_A$$
5	1 2 3 4	m2cpmf1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:K\underset{1-1}{⟶}S$$
6	1 2 3 4	m2cpmfo	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:K\underset{onto}{⟶}S$$
7		df-f1o	$$⊢T:K\underset{1-1\; onto}{⟶}S\leftrightarrow \left(T:K\underset{1-1}{⟶}S\wedge T:K\underset{onto}{⟶}S\right)$$
8	5 6 7	sylanbrc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:K\underset{1-1\; onto}{⟶}S$$