# Metamath Proof Explorer

## Theorem mat2pmatbas

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

Ref Expression
Hypotheses mat2pmatbas.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
mat2pmatbas.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mat2pmatbas.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
mat2pmatbas.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
mat2pmatbas.c ${⊢}{C}={N}\mathrm{Mat}{P}$
Assertion mat2pmatbas ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {T}\left({M}\right)\in {\mathrm{Base}}_{{C}}$

### Proof

Step Hyp Ref Expression
1 mat2pmatbas.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
2 mat2pmatbas.a ${⊢}{A}={N}\mathrm{Mat}{R}$
3 mat2pmatbas.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
4 mat2pmatbas.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
5 mat2pmatbas.c ${⊢}{C}={N}\mathrm{Mat}{P}$
6 eqid ${⊢}\mathrm{algSc}\left({P}\right)=\mathrm{algSc}\left({P}\right)$
7 1 2 3 4 6 mat2pmatval ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {T}\left({M}\right)=\left({x}\in {N},{y}\in {N}⟼\mathrm{algSc}\left({P}\right)\left({x}{M}{y}\right)\right)$
8 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
9 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
10 simp1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {N}\in \mathrm{Fin}$
11 4 fvexi ${⊢}{P}\in \mathrm{V}$
12 11 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {P}\in \mathrm{V}$
13 eqid ${⊢}\mathrm{Scalar}\left({P}\right)=\mathrm{Scalar}\left({P}\right)$
14 4 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
15 14 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {P}\in \mathrm{Ring}$
16 15 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {P}\in \mathrm{Ring}$
17 4 ply1lmod ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{LMod}$
18 17 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {P}\in \mathrm{LMod}$
19 18 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {P}\in \mathrm{LMod}$
20 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
21 6 13 16 19 20 8 asclf ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to \mathrm{algSc}\left({P}\right):{\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}⟶{\mathrm{Base}}_{{P}}$
22 4 ply1sca ${⊢}{R}\in \mathrm{Ring}\to {R}=\mathrm{Scalar}\left({P}\right)$
23 22 fveq2d ${⊢}{R}\in \mathrm{Ring}\to {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
24 23 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
25 24 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
26 25 feq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to \left(\mathrm{algSc}\left({P}\right):{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{P}}↔\mathrm{algSc}\left({P}\right):{\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}⟶{\mathrm{Base}}_{{P}}\right)$
27 21 26 mpbird ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to \mathrm{algSc}\left({P}\right):{\mathrm{Base}}_{{R}}⟶{\mathrm{Base}}_{{P}}$
28 simp2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {x}\in {N}$
29 simp3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {y}\in {N}$
30 3 eleq2i ${⊢}{M}\in {B}↔{M}\in {\mathrm{Base}}_{{A}}$
31 30 biimpi ${⊢}{M}\in {B}\to {M}\in {\mathrm{Base}}_{{A}}$
32 31 3ad2ant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {M}\in {\mathrm{Base}}_{{A}}$
33 32 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {M}\in {\mathrm{Base}}_{{A}}$
34 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
35 2 34 matecl ${⊢}\left({x}\in {N}\wedge {y}\in {N}\wedge {M}\in {\mathrm{Base}}_{{A}}\right)\to {x}{M}{y}\in {\mathrm{Base}}_{{R}}$
36 28 29 33 35 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {x}{M}{y}\in {\mathrm{Base}}_{{R}}$
37 27 36 ffvelrnd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to \mathrm{algSc}\left({P}\right)\left({x}{M}{y}\right)\in {\mathrm{Base}}_{{P}}$
38 5 8 9 10 12 37 matbas2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to \left({x}\in {N},{y}\in {N}⟼\mathrm{algSc}\left({P}\right)\left({x}{M}{y}\right)\right)\in {\mathrm{Base}}_{{C}}$
39 7 38 eqeltrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {T}\left({M}\right)\in {\mathrm{Base}}_{{C}}$