Metamath Proof Explorer


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 )