Metamath Proof Explorer

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 ConstPolyMat R$
		m2cpmfo.t	$⊢ T = N matToPolyMat R$
		m2cpmfo.a	$⊢ A = N Mat R$
		m2cpmfo.k	$⊢ K = {Base}_{A}$
	Assertion	m2cpmf1o	$⊢ (N \in Fin \land R \in Ring) \to T : K \underset{1-1 onto}{⟶} S$

Proof

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