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 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ 𝐻 ) |
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 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) ∈ 𝐻 ) |