# Metamath Proof Explorer

## Theorem decpmatmul

Description: The matrix consisting of the coefficients in the polynomial entries of the product of two polynomial matrices is a sum of products of the matrices consisting of the coefficients in the polynomial entries of the polynomial matrices for the same power. (Contributed by AV, 21-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}}$
decpmatmul.a ${⊢}{A}={N}\mathrm{Mat}{R}$
Assertion decpmatmul ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}=\underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}}\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\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 decpmatmul.a ${⊢}{A}={N}\mathrm{Mat}{R}$
5 eqidd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left({x}\in {N},{y}\in {N}⟼\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\right)=\left({x}\in {N},{y}\in {N}⟼\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\right)$
6 oveq1 ${⊢}{x}={i}\to {x}\left({U}\mathrm{decompPMat}{k}\right){t}={i}\left({U}\mathrm{decompPMat}{k}\right){t}$
7 oveq2 ${⊢}{y}={j}\to {t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}={t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}$
8 6 7 oveqan12d ${⊢}\left({x}={i}\wedge {y}={j}\right)\to \left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)=\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)$
9 8 mpteq2dv ${⊢}\left({x}={i}\wedge {y}={j}\right)\to \left({t}\in {N}⟼\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)=\left({t}\in {N}⟼\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)$
10 9 oveq2d ${⊢}\left({x}={i}\wedge {y}={j}\right)\to \underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)=\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)$
11 10 mpteq2dv ${⊢}\left({x}={i}\wedge {y}={j}\right)\to \left({k}\in \left(0\dots {K}\right)⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)=\left({k}\in \left(0\dots {K}\right)⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)\right)$
12 11 oveq2d ${⊢}\left({x}={i}\wedge {y}={j}\right)\to \underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)=\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)\right)$
13 12 adantl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({x}={i}\wedge {y}={j}\right)\right)\to \underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)=\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)\right)$
14 simprl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\in {N}$
15 simprr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {j}\in {N}$
16 ovexd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)\right)\in \mathrm{V}$
17 5 13 14 15 16 ovmpod ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\left({x}\in {N},{y}\in {N}⟼\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\right){j}=\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)\right)$
18 2 3 matrcl ${⊢}{U}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{V}\right)$
19 18 simpld ${⊢}{U}\in {B}\to {N}\in \mathrm{Fin}$
20 19 adantr ${⊢}\left({U}\in {B}\wedge {W}\in {B}\right)\to {N}\in \mathrm{Fin}$
21 20 anim2i ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {N}\in \mathrm{Fin}\right)$
22 21 ancomd ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
23 22 3adant3 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
24 eqid ${⊢}{R}\mathrm{maMul}⟨{N},{N},{N}⟩={R}\mathrm{maMul}⟨{N},{N},{N}⟩$
25 4 24 matmulr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
26 23 25 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
27 26 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
28 27 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
29 28 eqcomd ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {\cdot }_{{A}}={R}\mathrm{maMul}⟨{N},{N},{N}⟩$
30 29 oveqd ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)=\left({U}\mathrm{decompPMat}{k}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right)\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)$
31 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
32 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
33 simp1 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
34 33 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {R}\in \mathrm{Ring}$
35 34 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {R}\in \mathrm{Ring}$
36 23 simpld ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to {N}\in \mathrm{Fin}$
37 36 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {N}\in \mathrm{Fin}$
38 37 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {N}\in \mathrm{Fin}$
39 simpl2l ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {U}\in {B}$
40 39 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {U}\in {B}$
41 elfznn0 ${⊢}{k}\in \left(0\dots {K}\right)\to {k}\in {ℕ}_{0}$
42 41 adantl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {k}\in {ℕ}_{0}$
43 35 40 42 3jca ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {U}\in {B}\wedge {k}\in {ℕ}_{0}\right)$
44 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
45 1 2 3 4 44 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {U}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {U}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
46 43 45 syl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {U}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
47 4 31 44 matbas2i ${⊢}{U}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}\to {U}\mathrm{decompPMat}{k}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
48 46 47 syl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {U}\mathrm{decompPMat}{k}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
49 simpl2r ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {W}\in {B}$
50 49 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {W}\in {B}$
51 fznn0sub ${⊢}{k}\in \left(0\dots {K}\right)\to {K}-{k}\in {ℕ}_{0}$
52 51 adantl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {K}-{k}\in {ℕ}_{0}$
53 35 50 52 3jca ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {W}\in {B}\wedge {K}-{k}\in {ℕ}_{0}\right)$
54 1 2 3 4 44 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {W}\in {B}\wedge {K}-{k}\in {ℕ}_{0}\right)\to {W}\mathrm{decompPMat}\left({K}-{k}\right)\in {\mathrm{Base}}_{{A}}$
55 53 54 syl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {W}\mathrm{decompPMat}\left({K}-{k}\right)\in {\mathrm{Base}}_{{A}}$
56 4 31 44 matbas2i ${⊢}{W}\mathrm{decompPMat}\left({K}-{k}\right)\in {\mathrm{Base}}_{{A}}\to {W}\mathrm{decompPMat}\left({K}-{k}\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
57 55 56 syl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {W}\mathrm{decompPMat}\left({K}-{k}\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
58 24 31 32 35 38 38 38 48 57 mamuval ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({U}\mathrm{decompPMat}{k}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right)\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)=\left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)$
59 30 58 eqtrd ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)=\left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)$
60 59 mpteq2dva ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left({k}\in \left(0\dots {K}\right)⟼\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)=\left({k}\in \left(0\dots {K}\right)⟼\left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\right)$
61 60 oveq2d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}}\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)=\underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}}\left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)$
62 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
63 ovexd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left(0\dots {K}\right)\in \mathrm{V}$
64 ringcmn ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{CMnd}$
65 33 64 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to {R}\in \mathrm{CMnd}$
66 65 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {R}\in \mathrm{CMnd}$
67 66 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {R}\in \mathrm{CMnd}$
68 67 3ad2ant1 ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {R}\in \mathrm{CMnd}$
69 38 3ad2ant1 ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {N}\in \mathrm{Fin}$
70 35 3ad2ant1 ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {R}\in \mathrm{Ring}$
71 70 adantr ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\wedge {t}\in {N}\right)\to {R}\in \mathrm{Ring}$
72 simpl2 ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\wedge {t}\in {N}\right)\to {x}\in {N}$
73 simpr ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\wedge {t}\in {N}\right)\to {t}\in {N}$
74 43 3ad2ant1 ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to \left({R}\in \mathrm{Ring}\wedge {U}\in {B}\wedge {k}\in {ℕ}_{0}\right)$
75 74 adantr ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\wedge {t}\in {N}\right)\to \left({R}\in \mathrm{Ring}\wedge {U}\in {B}\wedge {k}\in {ℕ}_{0}\right)$
76 75 45 syl ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\wedge {t}\in {N}\right)\to {U}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
77 4 31 44 72 73 76 matecld ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\wedge {t}\in {N}\right)\to {x}\left({U}\mathrm{decompPMat}{k}\right){t}\in {\mathrm{Base}}_{{R}}$
78 simpl3 ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\wedge {t}\in {N}\right)\to {y}\in {N}$
79 55 3ad2ant1 ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {W}\mathrm{decompPMat}\left({K}-{k}\right)\in {\mathrm{Base}}_{{A}}$
80 79 adantr ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\wedge {t}\in {N}\right)\to {W}\mathrm{decompPMat}\left({K}-{k}\right)\in {\mathrm{Base}}_{{A}}$
81 4 31 44 73 78 80 matecld ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\wedge {t}\in {N}\right)\to {t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\in {\mathrm{Base}}_{{R}}$
82 31 32 ringcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\left({U}\mathrm{decompPMat}{k}\right){t}\in {\mathrm{Base}}_{{R}}\wedge {t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\in {\mathrm{Base}}_{{R}}\right)\to \left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\in {\mathrm{Base}}_{{R}}$
83 71 77 81 82 syl3anc ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\wedge {t}\in {N}\right)\to \left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\in {\mathrm{Base}}_{{R}}$
84 83 ralrimiva ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to \forall {t}\in {N}\phantom{\rule{.4em}{0ex}}\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\in {\mathrm{Base}}_{{R}}$
85 31 68 69 84 gsummptcl ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {x}\in {N}\wedge {y}\in {N}\right)\to \underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\in {\mathrm{Base}}_{{R}}$
86 4 31 44 38 35 85 matbas2d ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\in {\mathrm{Base}}_{{A}}$
87 eqid ${⊢}\left({k}\in \left(0\dots {K}\right)⟼\left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\right)=\left({k}\in \left(0\dots {K}\right)⟼\left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\right)$
88 fzfid ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left(0\dots {K}\right)\in \mathrm{Fin}$
89 simpl ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{V}\right)\to {N}\in \mathrm{Fin}$
90 89 89 jca ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{V}\right)\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
91 18 90 syl ${⊢}{U}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
92 91 adantr ${⊢}\left({U}\in {B}\wedge {W}\in {B}\right)\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
93 92 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
94 93 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
95 94 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
96 mpoexga ${⊢}\left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)\to \left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\in \mathrm{V}$
97 95 96 syl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\in \mathrm{V}$
98 fvexd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {0}_{{A}}\in \mathrm{V}$
99 87 88 97 98 fsuppmptdm ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in \left(0\dots {K}\right)⟼\left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\right)\right)$
100 4 44 62 37 63 34 86 99 matgsum ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}}\left({x}\in {N},{y}\in {N}⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)=\left({x}\in {N},{y}\in {N}⟼\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\right)$
101 61 100 eqtrd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}}\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)=\left({x}\in {N},{y}\in {N}⟼\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\right)$
102 101 oveqd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\left(\underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}},\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)\right){j}={i}\left({x}\in {N},{y}\in {N}⟼\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({x}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){y}\right)\right)\right)\right){j}$
103 simpl2 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left({U}\in {B}\wedge {W}\in {B}\right)$
104 simpl3 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {K}\in {ℕ}_{0}$
105 1 2 3 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{{k}=0}{\overset{{K}}{{\sum }_{{R}}}},\left({\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\right)\right)$
106 37 34 103 14 15 104 105 syl213anc ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\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}=\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}},\left({\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\right)\right)$
107 simpll1 ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {R}\in \mathrm{Ring}$
108 simplrl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {i}\in {N}$
109 simprl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {t}\in {N}$
110 3 eleq2i ${⊢}{U}\in {B}↔{U}\in {\mathrm{Base}}_{{C}}$
111 110 biimpi ${⊢}{U}\in {B}\to {U}\in {\mathrm{Base}}_{{C}}$
112 111 adantr ${⊢}\left({U}\in {B}\wedge {W}\in {B}\right)\to {U}\in {\mathrm{Base}}_{{C}}$
113 112 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to {U}\in {\mathrm{Base}}_{{C}}$
114 113 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {U}\in {\mathrm{Base}}_{{C}}$
115 114 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {U}\in {\mathrm{Base}}_{{C}}$
116 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
117 2 116 matecl ${⊢}\left({i}\in {N}\wedge {t}\in {N}\wedge {U}\in {\mathrm{Base}}_{{C}}\right)\to {i}{U}{t}\in {\mathrm{Base}}_{{P}}$
118 108 109 115 117 syl3anc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {i}{U}{t}\in {\mathrm{Base}}_{{P}}$
119 41 ad2antll ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {k}\in {ℕ}_{0}$
120 eqid ${⊢}{\mathrm{coe}}_{1}\left({i}{U}{t}\right)={\mathrm{coe}}_{1}\left({i}{U}{t}\right)$
121 120 116 1 31 coe1fvalcl ${⊢}\left({i}{U}{t}\in {\mathrm{Base}}_{{P}}\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right)\in {\mathrm{Base}}_{{R}}$
122 118 119 121 syl2anc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right)\in {\mathrm{Base}}_{{R}}$
123 simplrr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {j}\in {N}$
124 49 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {W}\in {B}$
125 2 116 3 109 123 124 matecld ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {t}{W}{j}\in {\mathrm{Base}}_{{P}}$
126 51 ad2antll ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {K}-{k}\in {ℕ}_{0}$
127 eqid ${⊢}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)={\mathrm{coe}}_{1}\left({t}{W}{j}\right)$
128 127 116 1 31 coe1fvalcl ${⊢}\left({t}{W}{j}\in {\mathrm{Base}}_{{P}}\wedge {K}-{k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\in {\mathrm{Base}}_{{R}}$
129 125 126 128 syl2anc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\in {\mathrm{Base}}_{{R}}$
130 31 32 ringcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right)\in {\mathrm{Base}}_{{R}}\wedge {\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\in {\mathrm{Base}}_{{R}}\right)\to {\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\in {\mathrm{Base}}_{{R}}$
131 107 122 129 130 syl3anc ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({t}\in {N}\wedge {k}\in \left(0\dots {K}\right)\right)\right)\to {\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\in {\mathrm{Base}}_{{R}}$
132 31 66 37 88 131 gsumcom3fi ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \underset{{t}\in {N}}{{\sum }_{{R}}}\left(\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}},\left({\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\right)\right)=\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left({\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\right)\right)$
133 14 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {i}\in {N}$
134 133 anim1i ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {t}\in {N}\right)\to \left({i}\in {N}\wedge {t}\in {N}\right)$
135 1 2 3 decpmate ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {U}\in {B}\wedge {k}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {t}\in {N}\right)\right)\to {i}\left({U}\mathrm{decompPMat}{k}\right){t}={\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right)$
136 43 134 135 syl2an2r ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {t}\in {N}\right)\to {i}\left({U}\mathrm{decompPMat}{k}\right){t}={\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right)$
137 simplrr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {j}\in {N}$
138 137 anim1ci ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {t}\in {N}\right)\to \left({t}\in {N}\wedge {j}\in {N}\right)$
139 1 2 3 decpmate ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {W}\in {B}\wedge {K}-{k}\in {ℕ}_{0}\right)\wedge \left({t}\in {N}\wedge {j}\in {N}\right)\right)\to {t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}={\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)$
140 53 138 139 syl2an2r ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {t}\in {N}\right)\to {t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}={\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)$
141 136 140 oveq12d ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {t}\in {N}\right)\to \left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)={\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)$
142 141 eqcomd ${⊢}\left(\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\wedge {t}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)=\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)$
143 142 mpteq2dva ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({t}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\right)=\left({t}\in {N}⟼\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)$
144 143 oveq2d ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \underset{{t}\in {N}}{{\sum }_{{R}}}\left({\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\right)=\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)$
145 144 mpteq2dva ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left({k}\in \left(0\dots {K}\right)⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left({\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\right)\right)=\left({k}\in \left(0\dots {K}\right)⟼\underset{{t}\in {N}}{{\sum }_{{R}}}\left(\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)\right)$
146 145 oveq2d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left({\mathrm{coe}}_{1}\left({i}{U}{t}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({t}{W}{j}\right)\left({K}-{k}\right)\right)\right)=\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)\right)$
147 106 132 146 3eqtrd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\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}=\underset{{k}=0}{\overset{{K}}{{\sum }_{{R}}}}\left(\underset{{t}\in {N}}{{\sum }_{{R}}},\left(\left({i}\left({U}\mathrm{decompPMat}{k}\right){t}\right){\cdot }_{{R}}\left({t}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right){j}\right)\right)\right)$
148 17 102 147 3eqtr4rd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\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}={i}\left(\underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}},\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)\right){j}$
149 148 ralrimivva ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}\left(\left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}\right){j}={i}\left(\underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}},\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)\right){j}$
150 1 2 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Ring}$
151 22 150 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to {C}\in \mathrm{Ring}$
152 simprl ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to {U}\in {B}$
153 simprr ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to {W}\in {B}$
154 eqid ${⊢}{\cdot }_{{C}}={\cdot }_{{C}}$
155 3 154 ringcl ${⊢}\left({C}\in \mathrm{Ring}\wedge {U}\in {B}\wedge {W}\in {B}\right)\to {U}{\cdot }_{{C}}{W}\in {B}$
156 151 152 153 155 syl3anc ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\right)\to {U}{\cdot }_{{C}}{W}\in {B}$
157 156 3adant3 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to {U}{\cdot }_{{C}}{W}\in {B}$
158 1 2 3 4 44 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {U}{\cdot }_{{C}}{W}\in {B}\wedge {K}\in {ℕ}_{0}\right)\to \left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}\in {\mathrm{Base}}_{{A}}$
159 157 158 syld3an2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}\in {\mathrm{Base}}_{{A}}$
160 4 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
161 23 160 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to {A}\in \mathrm{Ring}$
162 ringcmn ${⊢}{A}\in \mathrm{Ring}\to {A}\in \mathrm{CMnd}$
163 161 162 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to {A}\in \mathrm{CMnd}$
164 fzfid ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left(0\dots {K}\right)\in \mathrm{Fin}$
165 161 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {A}\in \mathrm{Ring}$
166 33 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {R}\in \mathrm{Ring}$
167 simpl2l ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {U}\in {B}$
168 41 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {k}\in {ℕ}_{0}$
169 166 167 168 3jca ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {U}\in {B}\wedge {k}\in {ℕ}_{0}\right)$
170 169 45 syl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {U}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
171 simpl2r ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {W}\in {B}$
172 51 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {K}-{k}\in {ℕ}_{0}$
173 166 171 172 3jca ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {W}\in {B}\wedge {K}-{k}\in {ℕ}_{0}\right)$
174 173 54 syl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to {W}\mathrm{decompPMat}\left({K}-{k}\right)\in {\mathrm{Base}}_{{A}}$
175 eqid ${⊢}{\cdot }_{{A}}={\cdot }_{{A}}$
176 44 175 ringcl ${⊢}\left({A}\in \mathrm{Ring}\wedge {U}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}\wedge {W}\mathrm{decompPMat}\left({K}-{k}\right)\in {\mathrm{Base}}_{{A}}\right)\to \left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\in {\mathrm{Base}}_{{A}}$
177 165 170 174 176 syl3anc ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {K}\right)\right)\to \left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\in {\mathrm{Base}}_{{A}}$
178 177 ralrimiva ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to \forall {k}\in \left(0\dots {K}\right)\phantom{\rule{.4em}{0ex}}\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\in {\mathrm{Base}}_{{A}}$
179 44 163 164 178 gsummptcl ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to \underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}}\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)\in {\mathrm{Base}}_{{A}}$
180 4 44 eqmat ${⊢}\left(\left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}\in {\mathrm{Base}}_{{A}}\wedge \underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}}\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)\in {\mathrm{Base}}_{{A}}\right)\to \left(\left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}=\underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}}\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}\left(\left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}\right){j}={i}\left(\underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}},\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)\right){j}\right)$
181 159 179 180 syl2anc ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left(\left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}=\underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}}\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}\left(\left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}\right){j}={i}\left(\underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}},\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)\right){j}\right)$
182 149 181 mpbird ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({U}\in {B}\wedge {W}\in {B}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left({U}{\cdot }_{{C}}{W}\right)\mathrm{decompPMat}{K}=\underset{{k}=0}{\overset{{K}}{{\sum }_{{A}}}}\left(\left({U}\mathrm{decompPMat}{k}\right){\cdot }_{{A}}\left({W}\mathrm{decompPMat}\left({K}-{k}\right)\right)\right)$