# Metamath Proof Explorer

## Theorem pm2mpmhmlem1

Description: Lemma 1 for pm2mpmhm . (Contributed by AV, 21-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 pm2mpmhmlem1

### 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 fvexd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {0}_{{Q}}\in \mathrm{V}$
12 ovexd
13 oveq2 ${⊢}{l}={n}\to \left(0\dots {l}\right)=\left(0\dots {n}\right)$
14 oveq1 ${⊢}{l}={n}\to {l}-{k}={n}-{k}$
15 14 oveq2d ${⊢}{l}={n}\to {y}\mathrm{decompPMat}\left({l}-{k}\right)={y}\mathrm{decompPMat}\left({n}-{k}\right)$
16 15 oveq2d ${⊢}{l}={n}\to \left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({l}-{k}\right)\right)=\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{k}\right)\right)$
17 13 16 mpteq12dv ${⊢}{l}={n}\to \left({k}\in \left(0\dots {l}\right)⟼\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({l}-{k}\right)\right)\right)=\left({k}\in \left(0\dots {n}\right)⟼\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{k}\right)\right)\right)$
18 17 oveq2d ${⊢}{l}={n}\to \underset{{k}=0}{\overset{{l}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({l}-{k}\right)\right)\right)=\underset{{k}=0}{\overset{{n}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{k}\right)\right)\right)$
19 oveq1
20 18 19 oveq12d
21 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {N}\in \mathrm{Fin}$
22 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {R}\in \mathrm{Ring}$
23 1 2 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Ring}$
24 23 anim1i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({C}\in \mathrm{Ring}\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)$
25 3anass ${⊢}\left({C}\in \mathrm{Ring}\wedge {x}\in {B}\wedge {y}\in {B}\right)↔\left({C}\in \mathrm{Ring}\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)$
26 24 25 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({C}\in \mathrm{Ring}\wedge {x}\in {B}\wedge {y}\in {B}\right)$
27 eqid ${⊢}{\cdot }_{{C}}={\cdot }_{{C}}$
28 3 27 ringcl ${⊢}\left({C}\in \mathrm{Ring}\wedge {x}\in {B}\wedge {y}\in {B}\right)\to {x}{\cdot }_{{C}}{y}\in {B}$
29 26 28 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{C}}{y}\in {B}$
30 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
31 1 2 3 30 pmatcoe1fsupp ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}{\cdot }_{{C}}{y}\in {B}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)$
32 21 22 29 31 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{n}\to \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)$
33 fvoveq1 ${⊢}{a}={i}\to {\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)={\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){b}\right)$
34 33 fveq1d ${⊢}{a}={i}\to {\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)$
35 34 eqeq1d ${⊢}{a}={i}\to \left({\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}↔{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)$
36 oveq2 ${⊢}{b}={j}\to {i}\left({x}{\cdot }_{{C}}{y}\right){b}={i}\left({x}{\cdot }_{{C}}{y}\right){j}$
37 36 fveq2d ${⊢}{b}={j}\to {\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){b}\right)={\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)$
38 37 fveq1d ${⊢}{b}={j}\to {\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({n}\right)$
39 38 eqeq1d ${⊢}{b}={j}\to \left({\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}↔{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({n}\right)={0}_{{R}}\right)$
40 35 39 rspc2va ${⊢}\left(\left({i}\in {N}\wedge {j}\in {N}\right)\wedge \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)\to {\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({n}\right)={0}_{{R}}$
41 40 expcom ${⊢}\forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\to \left(\left({i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({n}\right)={0}_{{R}}\right)$
42 41 adantl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)\to \left(\left({i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({n}\right)={0}_{{R}}\right)$
43 42 3impib ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({n}\right)={0}_{{R}}$
44 43 mpoeq3dva ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({n}\right)\right)=\left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)$
45 7 30 mat0op ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {0}_{{A}}=\left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)$
46 45 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)\to {0}_{{A}}=\left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)$
47 7 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
48 8 ply1sca ${⊢}{A}\in \mathrm{Ring}\to {A}=\mathrm{Scalar}\left({Q}\right)$
49 47 48 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
50 49 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
51 50 fveq2d ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)\to {0}_{{A}}={0}_{\mathrm{Scalar}\left({Q}\right)}$
52 44 46 51 3eqtr2d ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\wedge \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\forall {b}\in {N}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({a}\left({x}{\cdot }_{{C}}{y}\right){b}\right)\left({n}\right)={0}_{{R}}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({n}\right)\right)={0}_{\mathrm{Scalar}\left({Q}\right)}$
53 52 oveq1d
54 8 ply1lmod ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{LMod}$
55 47 54 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{LMod}$
56 55 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {Q}\in \mathrm{LMod}$
57 47 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {A}\in \mathrm{Ring}$
58 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
59 8 6 58 5 9 ply1moncl
60 57 59 sylan
61 eqid ${⊢}\mathrm{Scalar}\left({Q}\right)=\mathrm{Scalar}\left({Q}\right)$
62 eqid ${⊢}{0}_{\mathrm{Scalar}\left({Q}\right)}={0}_{\mathrm{Scalar}\left({Q}\right)}$
63 eqid ${⊢}{0}_{{Q}}={0}_{{Q}}$
64 9 61 4 62 63 lmod0vs
65 56 60 64 syl2an2r
67 53 66 eqtrd
68 67 ex
69 68 imim2d
70 69 ralimdva
71 70 reximdv
72 32 71 mpd
73 2 3 decpmatval ${⊢}\left({x}{\cdot }_{{C}}{y}\in {B}\wedge {n}\in {ℕ}_{0}\right)\to \left({x}{\cdot }_{{C}}{y}\right)\mathrm{decompPMat}{n}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({n}\right)\right)$
74 29 73 sylan ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({x}{\cdot }_{{C}}{y}\right)\mathrm{decompPMat}{n}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({n}\right)\right)$
75 74 oveq1d
76 75 eqeq1d
77 76 imbi2d
78 77 ralbidva
79 78 rexbidv
80 72 79 mpbird
81 1 2 3 7 decpmatmul ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({x}{\cdot }_{{C}}{y}\right)\mathrm{decompPMat}{n}=\underset{{k}=0}{\overset{{n}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{k}\right)\right)\right)$
82 81 ad4ant234 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({x}{\cdot }_{{C}}{y}\right)\mathrm{decompPMat}{n}=\underset{{k}=0}{\overset{{n}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{k}\right)\right)\right)$
83 82 eqcomd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \underset{{k}=0}{\overset{{n}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{k}\right)\right)\right)=\left({x}{\cdot }_{{C}}{y}\right)\mathrm{decompPMat}{n}$
84 83 oveq1d
85 84 eqeq1d
86 85 imbi2d
87 86 ralbidva
88 87 rexbidv
89 80 88 mpbird
90 11 12 20 89 mptnn0fsuppd