# Metamath Proof Explorer

## Theorem decpmatmullem

Description: Lemma for decpmatmul . (Contributed by AV, 20-Oct-2019) (Revised by AV, 3-Dec-2019)

Ref Expression
Hypotheses decpmatmul.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
decpmatmul.c ${⊢}{C}={N}\mathrm{Mat}{P}$
decpmatmul.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
Assertion decpmatmullem ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {I}\left(\left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}\right){J}=\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\underset{{l}=0}{\overset{{K}}{{\sum }_{{R}}}},\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 decpmatmul.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 decpmatmul.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 decpmatmul.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 simpr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}\in \mathrm{Ring}$
5 4 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {R}\in \mathrm{Ring}$
6 1 2 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Ring}$
7 6 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to {C}\in \mathrm{Ring}$
8 simpl ${⊢}\left({U}\in {B}\wedge {W}\in {B}\right)\to {U}\in {B}$
9 8 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to {U}\in {B}$
10 simpr ${⊢}\left({U}\in {B}\wedge {W}\in {B}\right)\to {W}\in {B}$
11 10 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to {W}\in {B}$
12 eqid ${⊢}{\cdot }_{{C}}={\cdot }_{{C}}$
13 3 12 ringcl ${⊢}\left({C}\in \mathrm{Ring}\wedge {U}\in {B}\wedge {W}\in {B}\right)\to {U}{\cdot }_{{C}}{W}\in {B}$
14 7 9 11 13 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to {U}{\cdot }_{{C}}{W}\in {B}$
15 14 3adant3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {U}{\cdot }_{{C}}{W}\in {B}$
16 simp33 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {K}\in {ℕ}_{0}$
17 3simpa ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\to \left({I}\in {N}\wedge {J}\in {N}\right)$
18 17 3ad2ant3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to \left({I}\in {N}\wedge {J}\in {N}\right)$
19 1 2 3 decpmate ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {U}{\cdot }_{{C}}{W}\in {B}\wedge {K}\in {ℕ}_{0}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {I}\left(\left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}\right){J}={\mathrm{coe}}_{1}\left({I}\left({U}{\cdot }_{{C}}{W}\right){J}\right)\left({K}\right)$
20 5 15 16 18 19 syl31anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {I}\left(\left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}\right){J}={\mathrm{coe}}_{1}\left({I}\left({U}{\cdot }_{{C}}{W}\right){J}\right)\left({K}\right)$
21 1 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
22 eqid ${⊢}{P}\mathrm{maMul}⟨{N},{N},{N}⟩={P}\mathrm{maMul}⟨{N},{N},{N}⟩$
23 2 22 matmulr ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)\to {P}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{C}}$
24 23 eqcomd ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)\to {\cdot }_{{C}}={P}\mathrm{maMul}⟨{N},{N},{N}⟩$
25 21 24 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {\cdot }_{{C}}={P}\mathrm{maMul}⟨{N},{N},{N}⟩$
26 25 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {\cdot }_{{C}}={P}\mathrm{maMul}⟨{N},{N},{N}⟩$
27 26 oveqd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {U}{\cdot }_{{C}}{W}={U}\left({P}\mathrm{maMul}⟨{N},{N},{N}⟩\right){W}$
28 27 oveqd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {I}\left({U}{\cdot }_{{C}}{W}\right){J}={I}\left({U}\left({P}\mathrm{maMul}⟨{N},{N},{N}⟩\right){W}\right){J}$
29 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
30 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
31 21 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {P}\in \mathrm{Ring}$
32 31 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {P}\in \mathrm{Ring}$
33 simpl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {N}\in \mathrm{Fin}$
34 33 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {N}\in \mathrm{Fin}$
35 2 29 matbas2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)\to {{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{C}}$
36 35 3 syl6reqr ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)\to {B}={{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}$
37 21 36 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {B}={{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}$
38 37 eleq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({U}\in {B}↔{U}\in \left({{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}\right)\right)$
39 38 biimpcd ${⊢}{U}\in {B}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {U}\in \left({{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}\right)\right)$
40 39 adantr ${⊢}\left({U}\in {B}\wedge {W}\in {B}\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {U}\in \left({{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}\right)\right)$
41 40 impcom ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to {U}\in \left({{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}\right)$
42 41 3adant3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {U}\in \left({{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}\right)$
43 21 35 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{C}}$
44 43 3 syl6reqr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {B}={{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}$
45 44 eleq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({W}\in {B}↔{W}\in \left({{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}\right)\right)$
46 45 biimpcd ${⊢}{W}\in {B}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {W}\in \left({{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}\right)\right)$
47 46 adantl ${⊢}\left({U}\in {B}\wedge {W}\in {B}\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {W}\in \left({{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}\right)\right)$
48 47 impcom ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to {W}\in \left({{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}\right)$
49 48 3adant3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {W}\in \left({{\mathrm{Base}}_{{P}}}^{\left({N}×{N}\right)}\right)$
50 simp31 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {I}\in {N}$
51 simp32 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {J}\in {N}$
52 22 29 30 32 34 34 34 42 49 50 51 mamufv ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {I}\left({U}\left({P}\mathrm{maMul}⟨{N},{N},{N}⟩\right){W}\right){J}=\underset{{t}\in {N}}{{\sum }_{{P}}}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)$
53 28 52 eqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {I}\left({U}{\cdot }_{{C}}{W}\right){J}=\underset{{t}\in {N}}{{\sum }_{{P}}}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)$
54 53 fveq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {\mathrm{coe}}_{1}\left({I}\left({U}{\cdot }_{{C}}{W}\right){J}\right)={\mathrm{coe}}_{1}\left(\underset{{t}\in {N}}{{\sum }_{{P}}}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)\right)$
55 54 fveq1d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {\mathrm{coe}}_{1}\left({I}\left({U}{\cdot }_{{C}}{W}\right){J}\right)\left({K}\right)={\mathrm{coe}}_{1}\left(\underset{{t}\in {N}}{{\sum }_{{P}}}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)\right)\left({K}\right)$
56 32 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {P}\in \mathrm{Ring}$
57 50 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {I}\in {N}$
58 simpr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {t}\in {N}$
59 simpl2l ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {U}\in {B}$
60 2 29 3 57 58 59 matecld ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {I}{U}{t}\in {\mathrm{Base}}_{{P}}$
61 51 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {J}\in {N}$
62 simpl2r ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {W}\in {B}$
63 2 29 3 58 61 62 matecld ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {t}{W}{J}\in {\mathrm{Base}}_{{P}}$
64 29 30 ringcl ${⊢}\left({P}\in \mathrm{Ring}\wedge {I}{U}{t}\in {\mathrm{Base}}_{{P}}\wedge {t}{W}{J}\in {\mathrm{Base}}_{{P}}\right)\to \left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\in {\mathrm{Base}}_{{P}}$
65 56 60 63 64 syl3anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to \left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\in {\mathrm{Base}}_{{P}}$
66 65 ralrimiva ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to \forall {t}\in {N}\phantom{\rule{.4em}{0ex}}\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\in {\mathrm{Base}}_{{P}}$
67 1 29 5 16 66 34 coe1fzgsumd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {\mathrm{coe}}_{1}\left(\underset{{t}\in {N}}{{\sum }_{{P}}}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)\right)\left({K}\right)=\underset{{t}\in {N}}{{\sum }_{{R}}}{\mathrm{coe}}_{1}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)\left({K}\right)$
68 simpl1r ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {R}\in \mathrm{Ring}$
69 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
70 1 30 69 29 coe1mul ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}{U}{t}\in {\mathrm{Base}}_{{P}}\wedge {t}{W}{J}\in {\mathrm{Base}}_{{P}}\right)\to {\mathrm{coe}}_{1}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)=\left({k}\in {ℕ}_{0}⟼\underset{{l}=0}{\overset{{k}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({k}-{l}\right)\right)\right)$
71 68 60 63 70 syl3anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {\mathrm{coe}}_{1}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)=\left({k}\in {ℕ}_{0}⟼\underset{{l}=0}{\overset{{k}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({k}-{l}\right)\right)\right)$
72 oveq2 ${⊢}{k}={K}\to \left(0\dots {k}\right)=\left(0\dots {K}\right)$
73 fvoveq1 ${⊢}{k}={K}\to {\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({k}-{l}\right)={\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)$
74 73 oveq2d ${⊢}{k}={K}\to {\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({k}-{l}\right)={\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)$
75 72 74 mpteq12dv ${⊢}{k}={K}\to \left({l}\in \left(0\dots {k}\right)⟼{\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({k}-{l}\right)\right)=\left({l}\in \left(0\dots {K}\right)⟼{\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)\right)$
76 75 oveq2d ${⊢}{k}={K}\to \underset{{l}=0}{\overset{{k}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({k}-{l}\right)\right)=\underset{{l}=0}{\overset{{K}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)\right)$
77 76 adantl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\wedge {k}={K}\right)\to \underset{{l}=0}{\overset{{k}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({k}-{l}\right)\right)=\underset{{l}=0}{\overset{{K}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)\right)$
78 16 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {K}\in {ℕ}_{0}$
79 ovexd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to \underset{{l}=0}{\overset{{K}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)\right)\in \mathrm{V}$
80 71 77 78 79 fvmptd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {t}\in {N}\right)\to {\mathrm{coe}}_{1}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)\left({K}\right)=\underset{{l}=0}{\overset{{K}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)\right)$
81 80 mpteq2dva ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to \left({t}\in {N}⟼{\mathrm{coe}}_{1}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)\left({K}\right)\right)=\left({t}\in {N}⟼\underset{{l}=0}{\overset{{K}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)\right)\right)$
82 81 oveq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to \underset{{t}\in {N}}{{\sum }_{{R}}}{\mathrm{coe}}_{1}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)\left({K}\right)=\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\underset{{l}=0}{\overset{{K}}{{\sum }_{{R}}}},\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)\right)\right)$
83 67 82 eqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {\mathrm{coe}}_{1}\left(\underset{{t}\in {N}}{{\sum }_{{P}}}\left(\left({I}{U}{t}\right){\cdot }_{{P}}\left({t}{W}{J}\right)\right)\right)\left({K}\right)=\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\underset{{l}=0}{\overset{{K}}{{\sum }_{{R}}}},\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)\right)\right)$
84 20 55 83 3eqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\wedge {K}\in {ℕ}_{0}\right)\right)\to {I}\left(\left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}\right){J}=\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\underset{{l}=0}{\overset{{K}}{{\sum }_{{R}}}},\left({\mathrm{coe}}_{1}\left({I}{U}{t}\right)\left({l}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{J}\right)\left({K}-{l}\right)\right)\right)$