Metamath Proof Explorer


Theorem mat2pmatbas0

Description: The result of a matrix transformation is a polynomial matrix. (Contributed by AV, 27-Oct-2019)

Ref Expression
Hypotheses mat2pmatbas.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
mat2pmatbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
mat2pmatbas.b 𝐵 = ( Base ‘ 𝐴 )
mat2pmatbas.p 𝑃 = ( Poly1𝑅 )
mat2pmatbas.c 𝐶 = ( 𝑁 Mat 𝑃 )
mat2pmatbas0.h 𝐻 = ( Base ‘ 𝐶 )
Assertion mat2pmatbas0 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑇𝑀 ) ∈ 𝐻 )

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2 mat2pmatbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 mat2pmatbas.b 𝐵 = ( Base ‘ 𝐴 )
4 mat2pmatbas.p 𝑃 = ( Poly1𝑅 )
5 mat2pmatbas.c 𝐶 = ( 𝑁 Mat 𝑃 )
6 mat2pmatbas0.h 𝐻 = ( Base ‘ 𝐶 )
7 1 2 3 4 5 mat2pmatbas ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑇𝑀 ) ∈ ( Base ‘ 𝐶 ) )
8 7 6 eleqtrrdi ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑇𝑀 ) ∈ 𝐻 )