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=NmatToPolyMatR
mat2pmatbas.a A=NMatR
mat2pmatbas.b B=BaseA
mat2pmatbas.p P=Poly1R
mat2pmatbas.c C=NMatP
mat2pmatbas0.h H=BaseC
Assertion mat2pmatf NFinRRingT:BH

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t T=NmatToPolyMatR
2 mat2pmatbas.a A=NMatR
3 mat2pmatbas.b B=BaseA
4 mat2pmatbas.p P=Poly1R
5 mat2pmatbas.c C=NMatP
6 mat2pmatbas0.h H=BaseC
7 simpl NFinRRingNFin
8 7 7 jca NFinRRingNFinNFin
9 8 adantr NFinRRingmBNFinNFin
10 mpoexga NFinNFinxN,yNalgScPxmyV
11 9 10 syl NFinRRingmBxN,yNalgScPxmyV
12 eqid algScP=algScP
13 1 2 3 4 12 mat2pmatfval NFinRRingT=mBxN,yNalgScPxmy
14 1 2 3 4 5 6 mat2pmatbas0 NFinRRingmBTmH
15 14 3expa NFinRRingmBTmH
16 11 13 15 fmpt2d NFinRRingT:BH