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 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
m2cpm.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
m2cpm.a 𝐴 = ( 𝑁 Mat 𝑅 )
m2cpm.b 𝐵 = ( Base ‘ 𝐴 )
Assertion m2cpmf1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵1-1𝑆 )

Proof

Step Hyp Ref Expression
1 m2cpm.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 m2cpm.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
3 m2cpm.a 𝐴 = ( 𝑁 Mat 𝑅 )
4 m2cpm.b 𝐵 = ( Base ‘ 𝐴 )
5 eqid ( Poly1𝑅 ) = ( Poly1𝑅 )
6 eqid ( 𝑁 Mat ( Poly1𝑅 ) ) = ( 𝑁 Mat ( Poly1𝑅 ) )
7 eqid ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) = ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) )
8 2 3 4 5 6 7 mat2pmatf1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵1-1→ ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) )
9 1 2 3 4 m2cpmf ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵𝑆 )
10 9 frnd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ran 𝑇𝑆 )
11 f1ssr ( ( 𝑇 : 𝐵1-1→ ( Base ‘ ( 𝑁 Mat ( Poly1𝑅 ) ) ) ∧ ran 𝑇𝑆 ) → 𝑇 : 𝐵1-1𝑆 )
12 8 10 11 syl2anc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵1-1𝑆 )