# Metamath Proof Explorer

## Theorem pm2mpmhmlem2

Description: Lemma 2 for pm2mpmhm . (Contributed by AV, 22-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpmhm.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pm2mpmhm.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pm2mpmhm.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pm2mpmhm.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
pm2mpmhm.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
pm2mpmhm.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
Assertion pm2mpmhmlem2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{T}\left({x}{\cdot }_{{C}}{y}\right)={T}\left({x}\right){\cdot }_{{Q}}{T}\left({y}\right)$

### Proof

Step Hyp Ref Expression
1 pm2mpmhm.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pm2mpmhm.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pm2mpmhm.a ${⊢}{A}={N}\mathrm{Mat}{R}$
4 pm2mpmhm.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
5 pm2mpmhm.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
6 pm2mpmhm.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
7 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}$
8 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}$
9 1 2 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Ring}$
10 9 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 {C}\in \mathrm{Ring}$
11 simpl ${⊢}\left({x}\in {B}\wedge {y}\in {B}\right)\to {x}\in {B}$
12 11 adantl ${⊢}\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}\in {B}$
13 simpr ${⊢}\left({x}\in {B}\wedge {y}\in {B}\right)\to {y}\in {B}$
14 13 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {y}\in {B}$
15 eqid ${⊢}{\cdot }_{{C}}={\cdot }_{{C}}$
16 6 15 ringcl ${⊢}\left({C}\in \mathrm{Ring}\wedge {x}\in {B}\wedge {y}\in {B}\right)\to {x}{\cdot }_{{C}}{y}\in {B}$
17 10 12 14 16 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 {x}{\cdot }_{{C}}{y}\in {B}$
18 eqid ${⊢}{\cdot }_{{Q}}={\cdot }_{{Q}}$
19 eqid ${⊢}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}={\cdot }_{{\mathrm{mulGrp}}_{{Q}}}$
20 eqid ${⊢}{\mathrm{var}}_{1}\left({A}\right)={\mathrm{var}}_{1}\left({A}\right)$
21 1 2 6 18 19 20 3 4 5 pm2mpfval ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}{\cdot }_{{C}}{y}\in {B}\right)\to {T}\left({x}{\cdot }_{{C}}{y}\right)=\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\left({x}{\cdot }_{{C}}{y}\right)\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
22 7 8 17 21 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 {T}\left({x}{\cdot }_{{C}}{y}\right)=\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\left({x}{\cdot }_{{C}}{y}\right)\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
23 1 2 6 3 decpmatmul ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({x}{\cdot }_{{C}}{y}\right)\mathrm{decompPMat}{k}=\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)$
24 23 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 {k}\in {ℕ}_{0}\right)\to \left({x}{\cdot }_{{C}}{y}\right)\mathrm{decompPMat}{k}=\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)$
25 24 oveq1d ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \left(\left({x}{\cdot }_{{C}}{y}\right)\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)=\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)$
26 25 mpteq2dva ${⊢}\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({k}\in {ℕ}_{0}⟼\left(\left({x}{\cdot }_{{C}}{y}\right)\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(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
27 26 oveq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\left({x}{\cdot }_{{C}}{y}\right)\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 }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
28 eqid ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{Q}}$
29 3 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
30 29 ad2antrr ${⊢}\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 {A}\in \mathrm{Ring}$
31 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
32 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
33 ringcmn ${⊢}{A}\in \mathrm{Ring}\to {A}\in \mathrm{CMnd}$
34 29 33 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{CMnd}$
35 34 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 {k}\in {ℕ}_{0}\right)\to {A}\in \mathrm{CMnd}$
36 fzfid ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \left(0\dots {k}\right)\in \mathrm{Fin}$
37 30 ad2antrr ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {A}\in \mathrm{Ring}$
38 simp-5r ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {R}\in \mathrm{Ring}$
39 12 ad3antrrr ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {x}\in {B}$
40 elfznn0 ${⊢}{z}\in \left(0\dots {k}\right)\to {z}\in {ℕ}_{0}$
41 40 adantl ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {z}\in {ℕ}_{0}$
42 1 2 6 3 31 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {B}\wedge {z}\in {ℕ}_{0}\right)\to {x}\mathrm{decompPMat}{z}\in {\mathrm{Base}}_{{A}}$
43 38 39 41 42 syl3anc ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {x}\mathrm{decompPMat}{z}\in {\mathrm{Base}}_{{A}}$
44 14 ad3antrrr ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {y}\in {B}$
45 fznn0sub ${⊢}{z}\in \left(0\dots {k}\right)\to {k}-{z}\in {ℕ}_{0}$
46 45 adantl ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {k}-{z}\in {ℕ}_{0}$
47 1 2 6 3 31 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {y}\in {B}\wedge {k}-{z}\in {ℕ}_{0}\right)\to {y}\mathrm{decompPMat}\left({k}-{z}\right)\in {\mathrm{Base}}_{{A}}$
48 38 44 46 47 syl3anc ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {y}\mathrm{decompPMat}\left({k}-{z}\right)\in {\mathrm{Base}}_{{A}}$
49 eqid ${⊢}{\cdot }_{{A}}={\cdot }_{{A}}$
50 31 49 ringcl ${⊢}\left({A}\in \mathrm{Ring}\wedge {x}\mathrm{decompPMat}{z}\in {\mathrm{Base}}_{{A}}\wedge {y}\mathrm{decompPMat}\left({k}-{z}\right)\in {\mathrm{Base}}_{{A}}\right)\to \left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\in {\mathrm{Base}}_{{A}}$
51 37 43 48 50 syl3anc ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to \left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\in {\mathrm{Base}}_{{A}}$
52 51 ralrimiva ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \forall {z}\in \left(0\dots {k}\right)\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\in {\mathrm{Base}}_{{A}}$
53 31 35 36 52 gsummptcl ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\in {\mathrm{Base}}_{{A}}$
54 53 ralrimiva ${⊢}\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 \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\in {\mathrm{Base}}_{{A}}$
55 1 2 6 3 49 32 decpmatmulsumfsupp ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right)\right)$
56 55 adantr ${⊢}\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 {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right)\right)$
57 simpr ${⊢}\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 {n}\in {ℕ}_{0}$
58 4 28 20 19 30 31 18 32 54 56 57 gsummoncoe1
59 csbov2g
60 id ${⊢}{n}\in {ℕ}_{0}\to {n}\in {ℕ}_{0}$
61 oveq2 ${⊢}{k}={n}\to \left(0\dots {k}\right)=\left(0\dots {n}\right)$
62 oveq1 ${⊢}{k}={n}\to {k}-{z}={n}-{z}$
63 62 oveq2d ${⊢}{k}={n}\to {y}\mathrm{decompPMat}\left({k}-{z}\right)={y}\mathrm{decompPMat}\left({n}-{z}\right)$
64 63 oveq2d ${⊢}{k}={n}\to \left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)=\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{z}\right)\right)$
65 61 64 mpteq12dv ${⊢}{k}={n}\to \left({z}\in \left(0\dots {k}\right)⟼\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)=\left({z}\in \left(0\dots {n}\right)⟼\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{z}\right)\right)\right)$
66 65 adantl ${⊢}\left({n}\in {ℕ}_{0}\wedge {k}={n}\right)\to \left({z}\in \left(0\dots {k}\right)⟼\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)=\left({z}\in \left(0\dots {n}\right)⟼\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{z}\right)\right)\right)$
67 60 66 csbied
68 67 oveq2d
69 59 68 eqtrd
71 eqidd ${⊢}\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({r}\in {ℕ}_{0}⟼\underset{{l}=0}{\overset{{r}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)\right)\right)=\left({r}\in {ℕ}_{0}⟼\underset{{l}=0}{\overset{{r}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)\right)\right)$
72 oveq2 ${⊢}{r}={n}\to \left(0\dots {r}\right)=\left(0\dots {n}\right)$
73 fvoveq1 ${⊢}{r}={n}\to {\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)={\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)$
74 73 oveq2d ${⊢}{r}={n}\to {\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)={\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)$
75 72 74 mpteq12dv ${⊢}{r}={n}\to \left({l}\in \left(0\dots {r}\right)⟼{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)\right)=\left({l}\in \left(0\dots {n}\right)⟼{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)\right)$
76 75 oveq2d ${⊢}{r}={n}\to \underset{{l}=0}{\overset{{r}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)\right)=\underset{{l}=0}{\overset{{n}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)\right)$
77 76 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 {r}={n}\right)\to \underset{{l}=0}{\overset{{r}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)\right)=\underset{{l}=0}{\overset{{n}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)\right)$
78 ovexd ${⊢}\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{{l}=0}{\overset{{n}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)\right)\in \mathrm{V}$
79 71 77 57 78 fvmptd ${⊢}\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({r}\in {ℕ}_{0}⟼\underset{{l}=0}{\overset{{r}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)\right)\right)\left({n}\right)=\underset{{l}=0}{\overset{{n}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)\right)$
80 eqid ${⊢}{0}_{{Q}}={0}_{{Q}}$
81 4 ply1ring ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{Ring}$
82 29 81 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{Ring}$
83 ringcmn ${⊢}{Q}\in \mathrm{Ring}\to {Q}\in \mathrm{CMnd}$
84 82 83 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{CMnd}$
85 84 ad2antrr ${⊢}\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 {Q}\in \mathrm{CMnd}$
86 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
87 86 a1i ${⊢}\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 {ℕ}_{0}\in \mathrm{V}$
88 11 anim2i ${⊢}\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(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {B}\right)$
89 df-3an ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}\in {B}\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {B}\right)$
90 88 89 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({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}\in {B}\right)$
91 90 adantr ${⊢}\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({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}\in {B}\right)$
92 1 2 6 18 19 20 3 4 28 pm2mpghmlem1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\in {\mathrm{Base}}_{{Q}}$
93 91 92 sylan ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\in {\mathrm{Base}}_{{Q}}$
94 93 fmpttd ${⊢}\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({k}\in {ℕ}_{0}⟼\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{Q}}$
95 1 2 6 18 19 20 3 4 pm2mpghmlem2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}\in {B}\right)\to {finSupp}_{{0}_{{Q}}}\left(\left({k}\in {ℕ}_{0}⟼\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
96 91 95 syl ${⊢}\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 {finSupp}_{{0}_{{Q}}}\left(\left({k}\in {ℕ}_{0}⟼\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
97 28 80 85 87 94 96 gsumcl ${⊢}\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}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}$
98 13 anim2i ${⊢}\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(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {y}\in {B}\right)$
99 df-3an ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {B}\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {y}\in {B}\right)$
100 98 99 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({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {B}\right)$
101 100 adantr ${⊢}\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({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {B}\right)$
102 1 2 6 18 19 20 3 4 28 pm2mpghmlem1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\in {\mathrm{Base}}_{{Q}}$
103 101 102 sylan ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\in {\mathrm{Base}}_{{Q}}$
104 103 fmpttd ${⊢}\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({k}\in {ℕ}_{0}⟼\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{Q}}$
105 7 8 14 3jca ${⊢}\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({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {B}\right)$
106 105 adantr ${⊢}\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({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {B}\right)$
107 1 2 6 18 19 20 3 4 pm2mpghmlem2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {B}\right)\to {finSupp}_{{0}_{{Q}}}\left(\left({k}\in {ℕ}_{0}⟼\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
108 106 107 syl ${⊢}\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 {finSupp}_{{0}_{{Q}}}\left(\left({k}\in {ℕ}_{0}⟼\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
109 28 80 85 87 104 108 gsumcl ${⊢}\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}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}$
110 eqid ${⊢}{\cdot }_{{Q}}={\cdot }_{{Q}}$
111 4 110 49 28 coe1mul ${⊢}\left({A}\in \mathrm{Ring}\wedge \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}\wedge \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}\right)\to {\mathrm{coe}}_{1}\left(\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)=\left({r}\in {ℕ}_{0}⟼\underset{{l}=0}{\overset{{r}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)\right)\right)$
112 111 fveq1d ${⊢}\left({A}\in \mathrm{Ring}\wedge \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}\wedge \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}\right)\to {\mathrm{coe}}_{1}\left(\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)\left({n}\right)=\left({r}\in {ℕ}_{0}⟼\underset{{l}=0}{\overset{{r}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)\right)\right)\left({n}\right)$
113 30 97 109 112 syl3anc ${⊢}\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 {\mathrm{coe}}_{1}\left(\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)\left({n}\right)=\left({r}\in {ℕ}_{0}⟼\underset{{l}=0}{\overset{{r}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({r}-{l}\right)\right)\right)\left({n}\right)$
114 oveq2 ${⊢}{z}={l}\to {x}\mathrm{decompPMat}{z}={x}\mathrm{decompPMat}{l}$
115 oveq2 ${⊢}{z}={l}\to {n}-{z}={n}-{l}$
116 115 oveq2d ${⊢}{z}={l}\to {y}\mathrm{decompPMat}\left({n}-{z}\right)={y}\mathrm{decompPMat}\left({n}-{l}\right)$
117 114 116 oveq12d ${⊢}{z}={l}\to \left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{z}\right)\right)=\left({x}\mathrm{decompPMat}{l}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{l}\right)\right)$
118 117 cbvmptv ${⊢}\left({z}\in \left(0\dots {n}\right)⟼\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{z}\right)\right)\right)=\left({l}\in \left(0\dots {n}\right)⟼\left({x}\mathrm{decompPMat}{l}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{l}\right)\right)\right)$
119 29 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 {l}\in \left(0\dots {n}\right)\right)\to {A}\in \mathrm{Ring}$
120 simp-5r ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
121 12 ad3antrrr ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {x}\in {B}$
122 simpr ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
123 1 2 6 3 31 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {x}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
124 120 121 122 123 syl3anc ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {x}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
125 124 ralrimiva ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\to \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{x}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
126 8 12 jca ${⊢}\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({R}\in \mathrm{Ring}\wedge {x}\in {B}\right)$
127 126 ad2antrr ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {x}\in {B}\right)$
128 1 2 6 3 32 decpmatfsupp ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {B}\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{x}\mathrm{decompPMat}{k}\right)\right)$
129 127 128 syl ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{x}\mathrm{decompPMat}{k}\right)\right)$
130 elfznn0 ${⊢}{l}\in \left(0\dots {n}\right)\to {l}\in {ℕ}_{0}$
131 130 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 {l}\in \left(0\dots {n}\right)\right)\to {l}\in {ℕ}_{0}$
132 4 28 20 19 119 31 18 32 125 129 131 gsummoncoe1
133 csbov2g
134 csbvarg
135 134 oveq2d
136 133 135 eqtrd
138 132 137 eqtr2d ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\to {x}\mathrm{decompPMat}{l}={\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right)$
139 14 ad3antrrr ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {y}\in {B}$
140 1 2 6 3 31 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {y}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {y}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
141 120 139 122 140 syl3anc ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {y}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
142 141 ralrimiva ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\to \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{y}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
143 8 14 jca ${⊢}\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({R}\in \mathrm{Ring}\wedge {y}\in {B}\right)$
144 143 ad2antrr ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {y}\in {B}\right)$
145 1 2 6 3 32 decpmatfsupp ${⊢}\left({R}\in \mathrm{Ring}\wedge {y}\in {B}\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{y}\mathrm{decompPMat}{k}\right)\right)$
146 144 145 syl ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{y}\mathrm{decompPMat}{k}\right)\right)$
147 fznn0sub ${⊢}{l}\in \left(0\dots {n}\right)\to {n}-{l}\in {ℕ}_{0}$
148 147 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 {l}\in \left(0\dots {n}\right)\right)\to {n}-{l}\in {ℕ}_{0}$
149 4 28 20 19 119 31 18 32 142 146 148 gsummoncoe1
150 ovex ${⊢}{n}-{l}\in \mathrm{V}$
151 csbov2g
152 150 151 mp1i
153 csbvarg
154 150 153 mp1i
155 154 oveq2d
156 149 152 155 3eqtrrd ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\to {y}\mathrm{decompPMat}\left({n}-{l}\right)={\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)$
157 138 156 oveq12d ${⊢}\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 {l}\in \left(0\dots {n}\right)\right)\to \left({x}\mathrm{decompPMat}{l}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{l}\right)\right)={\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)$
158 157 mpteq2dva ${⊢}\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({l}\in \left(0\dots {n}\right)⟼\left({x}\mathrm{decompPMat}{l}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{l}\right)\right)\right)=\left({l}\in \left(0\dots {n}\right)⟼{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)\right)$
159 118 158 syl5eq ${⊢}\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({z}\in \left(0\dots {n}\right)⟼\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{z}\right)\right)\right)=\left({l}\in \left(0\dots {n}\right)⟼{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)\right)$
160 159 oveq2d ${⊢}\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{{z}=0}{\overset{{n}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{z}\right)\right)\right)=\underset{{l}=0}{\overset{{n}}{{\sum }_{{A}}}}\left({\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right){\cdot }_{{A}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}-{l}\right)\right)$
161 79 113 160 3eqtr4rd ${⊢}\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{{z}=0}{\overset{{n}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({n}-{z}\right)\right)\right)={\mathrm{coe}}_{1}\left(\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)\left({n}\right)$
162 58 70 161 3eqtrd ${⊢}\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 {\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left(\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)\left({n}\right)$
163 162 ralrimiva ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left(\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)\left({n}\right)$
164 29 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}$
165 84 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{CMnd}$
166 86 a1i ${⊢}\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}\in \mathrm{V}$
167 4 ply1lmod ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{LMod}$
168 29 167 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{LMod}$
169 168 ad2antrr ${⊢}\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 {k}\in {ℕ}_{0}\right)\to {Q}\in \mathrm{LMod}$
170 34 ad2antrr ${⊢}\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 {k}\in {ℕ}_{0}\right)\to {A}\in \mathrm{CMnd}$
171 fzfid ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \left(0\dots {k}\right)\in \mathrm{Fin}$
172 29 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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {A}\in \mathrm{Ring}$
173 simp-4r ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {R}\in \mathrm{Ring}$
174 simplrl ${⊢}\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 {k}\in {ℕ}_{0}\right)\to {x}\in {B}$
175 174 adantr ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {x}\in {B}$
176 40 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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {z}\in {ℕ}_{0}$
177 173 175 176 42 syl3anc ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {x}\mathrm{decompPMat}{z}\in {\mathrm{Base}}_{{A}}$
178 simplrr ${⊢}\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 {k}\in {ℕ}_{0}\right)\to {y}\in {B}$
179 178 adantr ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {y}\in {B}$
180 45 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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {k}-{z}\in {ℕ}_{0}$
181 173 179 180 47 syl3anc ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to {y}\mathrm{decompPMat}\left({k}-{z}\right)\in {\mathrm{Base}}_{{A}}$
182 172 177 181 50 syl3anc ${⊢}\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 {k}\in {ℕ}_{0}\right)\wedge {z}\in \left(0\dots {k}\right)\right)\to \left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\in {\mathrm{Base}}_{{A}}$
183 182 ralrimiva ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \forall {z}\in \left(0\dots {k}\right)\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\in {\mathrm{Base}}_{{A}}$
184 31 170 171 183 gsummptcl ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\in {\mathrm{Base}}_{{A}}$
185 29 ad2antrr ${⊢}\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 {k}\in {ℕ}_{0}\right)\to {A}\in \mathrm{Ring}$
186 4 ply1sca ${⊢}{A}\in \mathrm{Ring}\to {A}=\mathrm{Scalar}\left({Q}\right)$
187 185 186 syl ${⊢}\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 {k}\in {ℕ}_{0}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
188 187 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 {k}\in {ℕ}_{0}\right)\to \mathrm{Scalar}\left({Q}\right)={A}$
189 188 fveq2d ${⊢}\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 {k}\in {ℕ}_{0}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}={\mathrm{Base}}_{{A}}$
190 184 189 eleqtrrd ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}$
191 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
192 4 20 191 19 28 ply1moncl ${⊢}\left({A}\in \mathrm{Ring}\wedge {k}\in {ℕ}_{0}\right)\to {k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\in {\mathrm{Base}}_{{Q}}$
193 185 192 sylancom ${⊢}\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 {k}\in {ℕ}_{0}\right)\to {k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\in {\mathrm{Base}}_{{Q}}$
194 eqid ${⊢}\mathrm{Scalar}\left({Q}\right)=\mathrm{Scalar}\left({Q}\right)$
195 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}$
196 28 194 18 195 lmodvscl ${⊢}\left({Q}\in \mathrm{LMod}\wedge \underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}}\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}\wedge {k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\in {\mathrm{Base}}_{{Q}}\right)\to \left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\in {\mathrm{Base}}_{{Q}}$
197 169 190 193 196 syl3anc ${⊢}\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 {k}\in {ℕ}_{0}\right)\to \left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\in {\mathrm{Base}}_{{Q}}$
198 197 fmpttd ${⊢}\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({k}\in {ℕ}_{0}⟼\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{Q}}$
199 1 2 6 18 19 20 3 4 28 5 pm2mpmhmlem1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {finSupp}_{{0}_{{Q}}}\left(\left({k}\in {ℕ}_{0}⟼\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
200 28 80 165 166 198 199 gsumcl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}$
201 82 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{Ring}$
202 90 92 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 {k}\in {ℕ}_{0}\right)\to \left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\in {\mathrm{Base}}_{{Q}}$
203 202 fmpttd ${⊢}\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({k}\in {ℕ}_{0}⟼\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{Q}}$
204 90 95 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 {finSupp}_{{0}_{{Q}}}\left(\left({k}\in {ℕ}_{0}⟼\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
205 28 80 165 166 203 204 gsumcl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}$
206 100 102 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 {k}\in {ℕ}_{0}\right)\to \left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\in {\mathrm{Base}}_{{Q}}$
207 206 fmpttd ${⊢}\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({k}\in {ℕ}_{0}⟼\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{Q}}$
208 7 8 14 107 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 {finSupp}_{{0}_{{Q}}}\left(\left({k}\in {ℕ}_{0}⟼\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
209 28 80 165 166 207 208 gsumcl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}$
210 28 110 ringcl ${⊢}\left({Q}\in \mathrm{Ring}\wedge \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}\wedge \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}\right)\to \left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\in {\mathrm{Base}}_{{Q}}$
211 201 205 209 210 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 \left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\in {\mathrm{Base}}_{{Q}}$
212 eqid ${⊢}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)={\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
213 eqid ${⊢}{\mathrm{coe}}_{1}\left(\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)={\mathrm{coe}}_{1}\left(\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)$
214 4 28 212 213 ply1coe1eq ${⊢}\left({A}\in \mathrm{Ring}\wedge \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {\mathrm{Base}}_{{Q}}\wedge \left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\in {\mathrm{Base}}_{{Q}}\right)\to \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left(\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)\left({n}\right)↔\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)=\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)$
215 164 200 211 214 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 \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left(\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)\left({n}\right)↔\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)=\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\right)$
216 163 215 mpbid ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left(\underset{{z}=0}{\overset{{k}}{{\sum }_{{A}}}},\left(\left({x}\mathrm{decompPMat}{z}\right){\cdot }_{{A}}\left({y}\mathrm{decompPMat}\left({k}-{z}\right)\right)\right)\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)=\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
217 22 27 216 3eqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {T}\left({x}{\cdot }_{{C}}{y}\right)=\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
218 1 2 6 18 19 20 3 4 5 pm2mpfval ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}\in {B}\right)\to {T}\left({x}\right)=\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
219 7 8 12 218 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 {T}\left({x}\right)=\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
220 1 2 6 18 19 20 3 4 5 pm2mpfval ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {B}\right)\to {T}\left({y}\right)=\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
221 7 8 14 220 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 {T}\left({y}\right)=\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
222 219 221 oveq12d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {T}\left({x}\right){\cdot }_{{Q}}{T}\left({y}\right)=\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({x}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right){\cdot }_{{Q}}\left(\underset{{k}\in {ℕ}_{0}}{{\sum }_{{Q}}},\left(\left({y}\mathrm{decompPMat}{k}\right){\cdot }_{{Q}}\left({k}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
223 217 222 eqtr4d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {T}\left({x}{\cdot }_{{C}}{y}\right)={T}\left({x}\right){\cdot }_{{Q}}{T}\left({y}\right)$
224 223 ralrimivva ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{T}\left({x}{\cdot }_{{C}}{y}\right)={T}\left({x}\right){\cdot }_{{Q}}{T}\left({y}\right)$