Metamath Proof Explorer

Theorem m2cpmf

Description: The matrix transformation is a 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 m2cpmf ⊢ N ∈ Fin ∧ R ∈ Ring → T : B ⟶ 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 simpl ⊢ N ∈ Fin ∧ R ∈ Ring → N ∈ Fin
6 5 5 jca ⊢ N ∈ Fin ∧ R ∈ Ring → N ∈ Fin ∧ N ∈ Fin
7 6 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B → N ∈ Fin ∧ N ∈ Fin
8 mpoexga ⊢ N ∈ Fin ∧ N ∈ Fin → i ∈ N , j ∈ N ⟼ algSc ⁡ Poly 1 ⁡ R ⁡ i m j ∈ V
9 7 8 syl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B → i ∈ N , j ∈ N ⟼ algSc ⁡ Poly 1 ⁡ R ⁡ i m j ∈ V
10 eqid ⊢ Poly 1 ⁡ R = Poly 1 ⁡ R
11 eqid ⊢ algSc ⁡ Poly 1 ⁡ R = algSc ⁡ Poly 1 ⁡ R
12 2 3 4 10 11 mat2pmatfval ⊢ N ∈ Fin ∧ R ∈ Ring → T = m ∈ B ⟼ i ∈ N , j ∈ N ⟼ algSc ⁡ Poly 1 ⁡ R ⁡ i m j
13 1 2 3 4 m2cpm ⊢ N ∈ Fin ∧ R ∈ Ring ∧ b ∈ B → T ⁡ b ∈ S
14 13 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ b ∈ B → T ⁡ b ∈ S
15 9 12 14 fmpt2d ⊢ N ∈ Fin ∧ R ∈ Ring → T : B ⟶ S