# Metamath Proof Explorer

## Theorem mp2pm2mp

Description: A polynomial over matrices transformed into a polynomial matrix transformed back into the polynomial over matrices. (Contributed by AV, 12-Oct-2019)

Ref Expression
Hypotheses mp2pm2mp.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mp2pm2mp.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
mp2pm2mp.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
mp2pm2mp.m
mp2pm2mp.e ${⊢}{E}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
mp2pm2mp.y ${⊢}{Y}={\mathrm{var}}_{1}\left({R}\right)$
mp2pm2mp.i
mp2pm2mplem2.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
mp2pm2mp.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
Assertion mp2pm2mp ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {T}\left({I}\left({O}\right)\right)={O}$

### Proof

Step Hyp Ref Expression
1 mp2pm2mp.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mp2pm2mp.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
3 mp2pm2mp.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
4 mp2pm2mp.m
5 mp2pm2mp.e ${⊢}{E}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
6 mp2pm2mp.y ${⊢}{Y}={\mathrm{var}}_{1}\left({R}\right)$
7 mp2pm2mp.i
8 mp2pm2mplem2.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
9 mp2pm2mp.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
10 eqid ${⊢}{N}\mathrm{Mat}{P}={N}\mathrm{Mat}{P}$
11 eqid ${⊢}{\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}$
12 1 2 3 8 4 5 6 7 10 11 mply1topmatcl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {I}\left({O}\right)\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}$
13 eqid ${⊢}{\cdot }_{{Q}}={\cdot }_{{Q}}$
14 eqid ${⊢}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}={\cdot }_{{\mathrm{mulGrp}}_{{Q}}}$
15 eqid ${⊢}{\mathrm{var}}_{1}\left({A}\right)={\mathrm{var}}_{1}\left({A}\right)$
16 8 10 11 13 14 15 1 2 9 pm2mpfval ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {I}\left({O}\right)\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}\right)\to {T}\left({I}\left({O}\right)\right)=\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
17 12 16 syld3an3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {T}\left({I}\left({O}\right)\right)=\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
18 1 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
19 18 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {A}\in \mathrm{Ring}$
20 eqid ${⊢}{0}_{{Q}}={0}_{{Q}}$
21 2 ply1ring ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{Ring}$
22 ringcmn ${⊢}{Q}\in \mathrm{Ring}\to {Q}\in \mathrm{CMnd}$
23 18 21 22 3syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{CMnd}$
24 23 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {Q}\in \mathrm{CMnd}$
25 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
26 25 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {ℕ}_{0}\in \mathrm{V}$
27 19 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {n}\in {ℕ}_{0}\right)\to {A}\in \mathrm{Ring}$
28 simpl2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {n}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
29 12 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {n}\in {ℕ}_{0}\right)\to {I}\left({O}\right)\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}$
30 simpr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {n}\in {ℕ}_{0}\right)\to {n}\in {ℕ}_{0}$
31 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
32 8 10 11 1 31 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\left({O}\right)\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}\wedge {n}\in {ℕ}_{0}\right)\to {I}\left({O}\right)\mathrm{decompPMat}{n}\in {\mathrm{Base}}_{{A}}$
33 28 29 30 32 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {n}\in {ℕ}_{0}\right)\to {I}\left({O}\right)\mathrm{decompPMat}{n}\in {\mathrm{Base}}_{{A}}$
34 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
35 31 2 15 13 34 14 3 ply1tmcl ${⊢}\left({A}\in \mathrm{Ring}\wedge {I}\left({O}\right)\mathrm{decompPMat}{n}\in {\mathrm{Base}}_{{A}}\wedge {n}\in {ℕ}_{0}\right)\to \left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\in {L}$
36 27 33 30 35 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\in {L}$
37 36 fmpttd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({n}\in {ℕ}_{0}⟼\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right):{ℕ}_{0}⟶{L}$
38 fveq2 ${⊢}{k}={n}\to {\mathrm{coe}}_{1}\left({p}\right)\left({k}\right)={\mathrm{coe}}_{1}\left({p}\right)\left({n}\right)$
39 38 oveqd ${⊢}{k}={n}\to {i}{\mathrm{coe}}_{1}\left({p}\right)\left({k}\right){j}={i}{\mathrm{coe}}_{1}\left({p}\right)\left({n}\right){j}$
40 oveq1 ${⊢}{k}={n}\to {k}{E}{Y}={n}{E}{Y}$
41 39 40 oveq12d
42 41 cbvmptv
43 42 a1i
44 43 oveq2d
45 44 mpoeq3ia
46 45 mpteq2i
47 7 46 eqtri
48 1 2 3 4 5 6 47 8 13 14 15 mp2pm2mplem5 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {finSupp}_{{0}_{{Q}}}\left(\left({n}\in {ℕ}_{0}⟼\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
49 3 20 24 26 37 48 gsumcl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {L}$
50 simp3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {O}\in {L}$
51 19 49 50 3jca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({A}\in \mathrm{Ring}\wedge \underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {L}\wedge {O}\in {L}\right)$
52 1 2 3 4 5 6 7 8 mp2pm2mplem4 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {n}\in {ℕ}_{0}\right)\to {I}\left({O}\right)\mathrm{decompPMat}{n}={\mathrm{coe}}_{1}\left({O}\right)\left({n}\right)$
53 52 oveq1d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)$
54 53 adantlr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)$
55 54 mpteq2dva ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}⟼\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)=\left({n}\in {ℕ}_{0}⟼{\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
56 55 oveq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\to \underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)=\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left({\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
57 56 fveq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)={\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left({\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
58 57 fveq1d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right)={\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left({\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right)$
59 19 50 jca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({A}\in \mathrm{Ring}\wedge {O}\in {L}\right)$
60 59 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\to \left({A}\in \mathrm{Ring}\wedge {O}\in {L}\right)$
61 eqid ${⊢}{\mathrm{coe}}_{1}\left({O}\right)={\mathrm{coe}}_{1}\left({O}\right)$
62 2 15 3 13 34 14 61 ply1coe ${⊢}\left({A}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {O}=\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left({\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
63 60 62 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\to {O}=\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left({\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)$
64 63 eqcomd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\to \underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left({\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)={O}$
65 64 fveq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left({\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)={\mathrm{coe}}_{1}\left({O}\right)$
66 65 fveq1d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left({\mathrm{coe}}_{1}\left({O}\right)\left({n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right)={\mathrm{coe}}_{1}\left({O}\right)\left({l}\right)$
67 58 66 eqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {l}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right)={\mathrm{coe}}_{1}\left({O}\right)\left({l}\right)$
68 67 ralrimiva ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \forall {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right)={\mathrm{coe}}_{1}\left({O}\right)\left({l}\right)$
69 eqid ${⊢}{\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)={\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)$
70 2 3 69 61 eqcoe1ply1eq ${⊢}\left({A}\in \mathrm{Ring}\wedge \underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\in {L}\wedge {O}\in {L}\right)\to \left(\forall {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)\right)\left({l}\right)={\mathrm{coe}}_{1}\left({O}\right)\left({l}\right)\to \underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)={O}\right)$
71 51 68 70 sylc ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \underset{{n}\in {ℕ}_{0}}{{\sum }_{{Q}}}\left(\left({I}\left({O}\right)\mathrm{decompPMat}{n}\right){\cdot }_{{Q}}\left({n}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}{\mathrm{var}}_{1}\left({A}\right)\right)\right)={O}$
72 17 71 eqtrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {T}\left({I}\left({O}\right)\right)={O}$