# Metamath Proof Explorer

## Theorem pm2mpval

Description: Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed by AV, 5-Dec-2019)

Ref Expression
Hypotheses pm2mpval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pm2mpval.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pm2mpval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
pm2mpval.m
pm2mpval.e
pm2mpval.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
pm2mpval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pm2mpval.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
pm2mpval.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
Assertion pm2mpval

### Proof

Step Hyp Ref Expression
1 pm2mpval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pm2mpval.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pm2mpval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 pm2mpval.m
5 pm2mpval.e
6 pm2mpval.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
7 pm2mpval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
8 pm2mpval.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
9 pm2mpval.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
10 df-pm2mp
11 10 a1i
12 simpl ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}={N}$
13 fveq2 ${⊢}{r}={R}\to {\mathrm{Poly}}_{1}\left({r}\right)={\mathrm{Poly}}_{1}\left({R}\right)$
14 13 adantl ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Poly}}_{1}\left({r}\right)={\mathrm{Poly}}_{1}\left({R}\right)$
15 12 14 oveq12d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)={N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)$
16 15 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Base}}_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)\right)}$
17 1 oveq2i ${⊢}{N}\mathrm{Mat}{P}={N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)$
18 2 17 eqtri ${⊢}{C}={N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)$
19 18 fveq2i ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)\right)}$
20 3 19 eqtri ${⊢}{B}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({R}\right)\right)}$
21 16 20 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Base}}_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}={B}$
22 21 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\wedge \left({n}={N}\wedge {r}={R}\right)\right)\to {\mathrm{Base}}_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}={B}$
23 ovex ${⊢}{n}\mathrm{Mat}{r}\in \mathrm{V}$
24 fvexd ${⊢}{a}={n}\mathrm{Mat}{r}\to {\mathrm{Poly}}_{1}\left({a}\right)\in \mathrm{V}$
25 simpr ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to {q}={\mathrm{Poly}}_{1}\left({a}\right)$
26 fveq2 ${⊢}{a}={n}\mathrm{Mat}{r}\to {\mathrm{Poly}}_{1}\left({a}\right)={\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)$
27 26 adantr ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to {\mathrm{Poly}}_{1}\left({a}\right)={\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)$
28 25 27 eqtrd ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to {q}={\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)$
29 28 fveq2d ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to {\cdot }_{{q}}={\cdot }_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}$
30 eqidd ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to {m}\mathrm{decompPMat}{k}={m}\mathrm{decompPMat}{k}$
31 28 fveq2d ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to {\mathrm{mulGrp}}_{{q}}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}$
32 31 fveq2d ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to {\cdot }_{{\mathrm{mulGrp}}_{{q}}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}}$
33 eqidd ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to {k}={k}$
34 fveq2 ${⊢}{a}={n}\mathrm{Mat}{r}\to {\mathrm{var}}_{1}\left({a}\right)={\mathrm{var}}_{1}\left({n}\mathrm{Mat}{r}\right)$
35 34 adantr ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to {\mathrm{var}}_{1}\left({a}\right)={\mathrm{var}}_{1}\left({n}\mathrm{Mat}{r}\right)$
36 32 33 35 oveq123d ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to {k}{\cdot }_{{\mathrm{mulGrp}}_{{q}}}{\mathrm{var}}_{1}\left({a}\right)={k}{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}}{\mathrm{var}}_{1}\left({n}\mathrm{Mat}{r}\right)$
37 29 30 36 oveq123d ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to \left({m}\mathrm{decompPMat}{k}\right){\cdot }_{{q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{q}}}{\mathrm{var}}_{1}\left({a}\right)\right)=\left({m}\mathrm{decompPMat}{k}\right){\cdot }_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}}{\mathrm{var}}_{1}\left({n}\mathrm{Mat}{r}\right)\right)$
38 37 mpteq2dv ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to \left({k}\in {ℕ}_{0}⟼\left({m}\mathrm{decompPMat}{k}\right){\cdot }_{{q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{q}}}{\mathrm{var}}_{1}\left({a}\right)\right)\right)=\left({k}\in {ℕ}_{0}⟼\left({m}\mathrm{decompPMat}{k}\right){\cdot }_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}}{\mathrm{var}}_{1}\left({n}\mathrm{Mat}{r}\right)\right)\right)$
39 28 38 oveq12d ${⊢}\left({a}={n}\mathrm{Mat}{r}\wedge {q}={\mathrm{Poly}}_{1}\left({a}\right)\right)\to \underset{{k}\in {ℕ}_{0}}{{\sum }_{{q}}}\left(\left({m}\mathrm{decompPMat}{k}\right){\cdot }_{{q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{q}}}{\mathrm{var}}_{1}\left({a}\right)\right)\right)=\underset{{k}\in {ℕ}_{0}}{{\sum }_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}}\left(\left({m}\mathrm{decompPMat}{k}\right){\cdot }_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}}{\mathrm{var}}_{1}\left({n}\mathrm{Mat}{r}\right)\right)\right)$
40 24 39 csbied
41 23 40 csbie
42 oveq12 ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{Mat}{r}={N}\mathrm{Mat}{R}$
43 42 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)={\mathrm{Poly}}_{1}\left({N}\mathrm{Mat}{R}\right)$
44 7 fveq2i ${⊢}{\mathrm{Poly}}_{1}\left({A}\right)={\mathrm{Poly}}_{1}\left({N}\mathrm{Mat}{R}\right)$
45 8 44 eqtri ${⊢}{Q}={\mathrm{Poly}}_{1}\left({N}\mathrm{Mat}{R}\right)$
46 43 45 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)={Q}$
47 43 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\cdot }_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}={\cdot }_{{\mathrm{Poly}}_{1}\left({N}\mathrm{Mat}{R}\right)}$
48 45 fveq2i ${⊢}{\cdot }_{{Q}}={\cdot }_{{\mathrm{Poly}}_{1}\left({N}\mathrm{Mat}{R}\right)}$
49 4 48 eqtri
50 47 49 syl6eqr
51 eqidd ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {m}\mathrm{decompPMat}{k}={m}\mathrm{decompPMat}{k}$
52 43 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({N}\mathrm{Mat}{R}\right)}$
53 52 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({n}\mathrm{Mat}{r}\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({N}\mathrm{Mat}{R}\right)}}$
54 45 fveq2i ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({N}\mathrm{Mat}{R}\right)}$
55 54 fveq2i ${⊢}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_{1}\left({N}\mathrm{Mat}{R}\right)}}$
56 5 55 eqtri
57 53 56 syl6eqr
58 eqidd ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {k}={k}$
59 42 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{var}}_{1}\left({n}\mathrm{Mat}{r}\right)={\mathrm{var}}_{1}\left({N}\mathrm{Mat}{R}\right)$
60 7 fveq2i ${⊢}{\mathrm{var}}_{1}\left({A}\right)={\mathrm{var}}_{1}\left({N}\mathrm{Mat}{R}\right)$
61 6 60 eqtri ${⊢}{X}={\mathrm{var}}_{1}\left({N}\mathrm{Mat}{R}\right)$
62 59 61 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{var}}_{1}\left({n}\mathrm{Mat}{r}\right)={X}$
63 57 58 62 oveq123d
64 50 51 63 oveq123d
65 64 mpteq2dv
66 46 65 oveq12d
70 simpl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {N}\in \mathrm{Fin}$
71 elex ${⊢}{R}\in {V}\to {R}\in \mathrm{V}$
72 71 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {R}\in \mathrm{V}$
73 3 fvexi ${⊢}{B}\in \mathrm{V}$