# Metamath Proof Explorer

## Theorem pm2mpfo

Description: The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 12-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpfo.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pm2mpfo.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pm2mpfo.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
pm2mpfo.m
pm2mpfo.e
pm2mpfo.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
pm2mpfo.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pm2mpfo.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
pm2mpfo.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
pm2mpfo.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
Assertion pm2mpfo ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}\underset{onto}{⟶}{L}$

### Proof

Step Hyp Ref Expression
1 pm2mpfo.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pm2mpfo.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pm2mpfo.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 pm2mpfo.m
5 pm2mpfo.e
6 pm2mpfo.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
7 pm2mpfo.a ${⊢}{A}={N}\mathrm{Mat}{R}$
8 pm2mpfo.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
9 pm2mpfo.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
10 pm2mpfo.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
11 1 2 3 4 5 6 7 8 10 9 pm2mpf ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}⟶{L}$
12 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
13 eqid ${⊢}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
14 eqid ${⊢}{\mathrm{var}}_{1}\left({R}\right)={\mathrm{var}}_{1}\left({R}\right)$
15 eqid ${⊢}\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)=\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)$
16 7 8 9 12 13 14 15 1 10 mp2pm2mp ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {p}\in {L}\right)\to {T}\left(\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\right)={p}$
17 16 3expa ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {p}\in {L}\right)\to {T}\left(\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\right)={p}$
18 7 8 9 1 12 13 14 15 2 3 mply1topmatcl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {p}\in {L}\right)\to \left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\in {B}$
19 18 3expa ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {p}\in {L}\right)\to \left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\in {B}$
20 simpr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {p}\in {L}\right)\wedge {f}=\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\right)\to {f}=\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)$
21 20 fveq2d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {p}\in {L}\right)\wedge {f}=\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\right)\to {T}\left({f}\right)={T}\left(\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\right)$
22 21 eqeq2d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {p}\in {L}\right)\wedge {f}=\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\right)\to \left({p}={T}\left({f}\right)↔{p}={T}\left(\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\right)\right)$
23 19 22 rspcedv ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {p}\in {L}\right)\to \left({p}={T}\left(\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\right)\to \exists {f}\in {B}\phantom{\rule{.4em}{0ex}}{p}={T}\left({f}\right)\right)$
24 23 com12 ${⊢}{p}={T}\left(\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {p}\in {L}\right)\to \exists {f}\in {B}\phantom{\rule{.4em}{0ex}}{p}={T}\left({f}\right)\right)$
25 24 eqcoms ${⊢}{T}\left(\left({l}\in {L}⟼\left({i}\in {N},{j}\in {N}⟼\underset{{k}\in {ℕ}_{0}}{{\sum }_{{P}}}\left(\left({i}{\mathrm{coe}}_{1}\left({l}\right)\left({k}\right){j}\right){\cdot }_{{P}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\right)\right)\left({p}\right)\right)={p}\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {p}\in {L}\right)\to \exists {f}\in {B}\phantom{\rule{.4em}{0ex}}{p}={T}\left({f}\right)\right)$
26 17 25 mpcom ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {p}\in {L}\right)\to \exists {f}\in {B}\phantom{\rule{.4em}{0ex}}{p}={T}\left({f}\right)$
27 26 ralrimiva ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \forall {p}\in {L}\phantom{\rule{.4em}{0ex}}\exists {f}\in {B}\phantom{\rule{.4em}{0ex}}{p}={T}\left({f}\right)$
28 dffo3 ${⊢}{T}:{B}\underset{onto}{⟶}{L}↔\left({T}:{B}⟶{L}\wedge \forall {p}\in {L}\phantom{\rule{.4em}{0ex}}\exists {f}\in {B}\phantom{\rule{.4em}{0ex}}{p}={T}\left({f}\right)\right)$
29 11 27 28 sylanbrc ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}\underset{onto}{⟶}{L}$