# 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}\mathrm{ConstPolyMat}{R}$
m2cpm.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
m2cpm.a ${⊢}{A}={N}\mathrm{Mat}{R}$
m2cpm.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion m2cpmf1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}\underset{1-1}{⟶}{S}$

### Proof

Step Hyp Ref Expression
1 m2cpm.s ${⊢}{S}={N}\mathrm{ConstPolyMat}{R}$
2 m2cpm.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
3 m2cpm.a ${⊢}{A}={N}\mathrm{Mat}{R}$
4 m2cpm.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
5 eqid ${⊢}{\mathrm{Poly}}_{1}\left({R}\right)={\mathrm{Poly}}_{1}\left({R}\right)$
6 eqid ${⊢}{N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)={N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)$
7 eqid ${⊢}{\mathrm{Base}}_{\left({N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)\right)}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)\right)}$
8 2 3 4 5 6 7 mat2pmatf1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}\underset{1-1}{⟶}{\mathrm{Base}}_{\left({N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)\right)}$
9 1 2 3 4 m2cpmf ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}⟶{S}$
10 9 frnd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \mathrm{ran}{T}\subseteq {S}$
11 f1ssr ${⊢}\left({T}:{B}\underset{1-1}{⟶}{\mathrm{Base}}_{\left({N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)\right)}\wedge \mathrm{ran}{T}\subseteq {S}\right)\to {T}:{B}\underset{1-1}{⟶}{S}$
12 8 10 11 syl2anc ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}\underset{1-1}{⟶}{S}$