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 Fin R 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 Poly 1 R = Poly 1 R
6 eqid N Mat Poly 1 R = N Mat Poly 1 R
7 eqid Base N Mat Poly 1 R = Base N Mat Poly 1 R
8 2 3 4 5 6 7 mat2pmatf1 N Fin R Ring T : B 1-1 Base N Mat Poly 1 R
9 1 2 3 4 m2cpmf N Fin R Ring T : B S
10 9 frnd N Fin R Ring ran T S
11 f1ssr T : B 1-1 Base N Mat Poly 1 R ran T S T : B 1-1 S
12 8 10 11 syl2anc N Fin R Ring T : B 1-1 S