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 e. Fin /\ R e. Ring ) -> T : K -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 e. Fin /\ R e. Ring ) -> T : K -1-1-> S )
6	1 2 3 4	m2cpmfo	|- ( ( N e. Fin /\ R e. Ring ) -> T : K -onto-> S )
7		df-f1o	|- ( T : K -1-1-onto-> S <-> ( T : K -1-1-> S /\ T : K -onto-> S ) )
8	5 6 7	sylanbrc	|- ( ( N e. Fin /\ R e. Ring ) -> T : K -1-1-onto-> S )