Metamath Proof Explorer

Theorem mat2pmatf

Description: The matrix transformation is a function from the matrices to the polynomial matrices. (Contributed by AV, 27-Oct-2019)

Ref Expression
Hypotheses mat2pmatbas.t ⊢ T = N matToPolyMat R
mat2pmatbas.a ⊢ A = N Mat R
mat2pmatbas.b ⊢ B = Base A
mat2pmatbas.p ⊢ P = Poly 1 ⁡ R
mat2pmatbas.c ⊢ C = N Mat P
mat2pmatbas0.h ⊢ H = Base C
Assertion mat2pmatf ⊢ N ∈ Fin ∧ R ∈ Ring → T : B ⟶ H

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t ⊢ T = N matToPolyMat R
2 mat2pmatbas.a ⊢ A = N Mat R
3 mat2pmatbas.b ⊢ B = Base A
4 mat2pmatbas.p ⊢ P = Poly 1 ⁡ R
5 mat2pmatbas.c ⊢ C = N Mat P
6 mat2pmatbas0.h ⊢ H = Base C
7 simpl ⊢ N ∈ Fin ∧ R ∈ Ring → N ∈ Fin
8 7 7 jca ⊢ N ∈ Fin ∧ R ∈ Ring → N ∈ Fin ∧ N ∈ Fin
9 8 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B → N ∈ Fin ∧ N ∈ Fin
10 mpoexga ⊢ N ∈ Fin ∧ N ∈ Fin → x ∈ N , y ∈ N ⟼ algSc ⁡ P ⁡ x m y ∈ V
11 9 10 syl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B → x ∈ N , y ∈ N ⟼ algSc ⁡ P ⁡ x m y ∈ V
12 eqid ⊢ algSc ⁡ P = algSc ⁡ P
13 1 2 3 4 12 mat2pmatfval ⊢ N ∈ Fin ∧ R ∈ Ring → T = m ∈ B ⟼ x ∈ N , y ∈ N ⟼ algSc ⁡ P ⁡ x m y
14 1 2 3 4 5 6 mat2pmatbas0 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B → T ⁡ m ∈ H
15 14 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B → T ⁡ m ∈ H
16 11 13 15 fmpt2d ⊢ N ∈ Fin ∧ R ∈ Ring → T : B ⟶ H