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 ConstPolyMat R )
	m2cpm.t	|- T = ( N matToPolyMat R )
	m2cpm.a	|- A = ( N Mat R )
	m2cpm.b	|- B = ( Base ` A )
Assertion	m2cpmf1	|- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> S )

Proof

Step	Hyp	Ref	Expression
1		m2cpm.s	|- S = ( N ConstPolyMat R )
2		m2cpm.t	|- T = ( N matToPolyMat R )
3		m2cpm.a	|- A = ( N Mat R )
4		m2cpm.b	|- B = ( Base ` A )
5		eqid	|- ( Poly1 ` R ) = ( Poly1 ` R )
6		eqid	|- ( N Mat ( Poly1 ` R ) ) = ( N Mat ( Poly1 ` R ) )
7		eqid	|- ( Base ` ( N Mat ( Poly1 ` R ) ) ) = ( Base ` ( N Mat ( Poly1 ` R ) ) )
8	2 3 4 5 6 7	mat2pmatf1	|- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
9	1 2 3 4	m2cpmf	|- ( ( N e. Fin /\ R e. Ring ) -> T : B --> S )
10	9	frnd	|- ( ( N e. Fin /\ R e. Ring ) -> ran T C_ S )
11		f1ssr	|- ( ( T : B -1-1-> ( Base ` ( N Mat ( Poly1 ` R ) ) ) /\ ran T C_ S ) -> T : B -1-1-> S )
12	8 10 11	syl2anc	|- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> S )