Metamath Proof Explorer

Theorem mp2pm2mplem4

Description: Lemma 4 for mp2pm2mp . (Contributed by AV, 12-Oct-2019) (Revised by AV, 5-Dec-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)$
Assertion mp2pm2mplem4 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to {I}\left({O}\right)\mathrm{decompPMat}{K}={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)$

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 1 2 3 4 5 6 7 8 mp2pm2mplem3
10 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
11 eqid ${⊢}{0}_{{P}}={0}_{{P}}$
12 8 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
13 12 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {P}\in \mathrm{Ring}$
14 ringcmn ${⊢}{P}\in \mathrm{Ring}\to {P}\in \mathrm{CMnd}$
15 13 14 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {P}\in \mathrm{CMnd}$
16 15 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to {P}\in \mathrm{CMnd}$
17 16 3ad2ant1 ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {P}\in \mathrm{CMnd}$
18 simpl2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
19 18 ad2antrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to {R}\in \mathrm{Ring}$
20 19 3ad2ant1 ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {R}\in \mathrm{Ring}$
21 20 adantr ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
22 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
23 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
24 simpl2 ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {i}\in {N}$
25 simpl3 ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {j}\in {N}$
26 simpl3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to {O}\in {L}$
27 26 ad2antrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to {O}\in {L}$
28 27 3ad2ant1 ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {O}\in {L}$
29 eqid ${⊢}{\mathrm{coe}}_{1}\left({O}\right)={\mathrm{coe}}_{1}\left({O}\right)$
30 29 3 2 23 coe1fvalcl ${⊢}\left({O}\in {L}\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\in {\mathrm{Base}}_{{A}}$
31 28 30 sylan ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\in {\mathrm{Base}}_{{A}}$
32 1 22 23 24 25 31 matecld ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}\in {\mathrm{Base}}_{{R}}$
33 simpr ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
34 eqid ${⊢}{\mathrm{mulGrp}}_{{P}}={\mathrm{mulGrp}}_{{P}}$
35 22 8 6 4 34 5 10 ply1tmcl
36 21 32 33 35 syl3anc
37 36 ralrimiva
38 simp1lr ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {s}\in {ℕ}_{0}$
39 oveq ${⊢}{\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({x}\right){j}={i}{0}_{{A}}{j}$
40 39 oveq1d
41 3simpa ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
42 41 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
43 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
44 1 43 mat0op ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {0}_{{A}}=\left({a}\in {N},{b}\in {N}⟼{0}_{{R}}\right)$
45 42 44 syl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {0}_{{A}}=\left({a}\in {N},{b}\in {N}⟼{0}_{{R}}\right)$
46 eqidd ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \left({a}={i}\wedge {b}={j}\right)\right)\to {0}_{{R}}={0}_{{R}}$
47 simprl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\in {N}$
48 simprr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {j}\in {N}$
49 fvexd ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {0}_{{R}}\in \mathrm{V}$
50 45 46 47 48 49 ovmpod ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}{0}_{{A}}{j}={0}_{{R}}$
51 50 adantr ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {x}\in {ℕ}_{0}\right)\to {i}{0}_{{A}}{j}={0}_{{R}}$
52 51 oveq1d
53 18 ad3antrrr ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {x}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
54 8 ply1sca ${⊢}{R}\in \mathrm{Ring}\to {R}=\mathrm{Scalar}\left({P}\right)$
55 53 54 syl ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {x}\in {ℕ}_{0}\right)\to {R}=\mathrm{Scalar}\left({P}\right)$
56 55 fveq2d ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {x}\in {ℕ}_{0}\right)\to {0}_{{R}}={0}_{\mathrm{Scalar}\left({P}\right)}$
57 56 oveq1d
58 8 ply1lmod ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{LMod}$
59 58 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {P}\in \mathrm{LMod}$
60 59 ad4antr ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {x}\in {ℕ}_{0}\right)\to {P}\in \mathrm{LMod}$
61 simpr ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {x}\in {ℕ}_{0}\right)\to {x}\in {ℕ}_{0}$
62 8 6 34 5 10 ply1moncl ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {ℕ}_{0}\right)\to {x}{E}{Y}\in {\mathrm{Base}}_{{P}}$
63 53 61 62 syl2anc ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {x}\in {ℕ}_{0}\right)\to {x}{E}{Y}\in {\mathrm{Base}}_{{P}}$
64 eqid ${⊢}\mathrm{Scalar}\left({P}\right)=\mathrm{Scalar}\left({P}\right)$
65 eqid ${⊢}{0}_{\mathrm{Scalar}\left({P}\right)}={0}_{\mathrm{Scalar}\left({P}\right)}$
66 10 64 4 65 11 lmod0vs
67 60 63 66 syl2anc
68 52 57 67 3eqtrd
70 40 69 sylan9eqr
71 70 exp31
72 71 a2d
73 72 ralimdva
74 73 impancom
75 74 3impib
76 breq2 ${⊢}{k}={x}\to \left({s}<{k}↔{s}<{x}\right)$
77 fveq2 ${⊢}{k}={x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)={\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)$
78 77 oveqd ${⊢}{k}={x}\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}={i}{\mathrm{coe}}_{1}\left({O}\right)\left({x}\right){j}$
79 oveq1 ${⊢}{k}={x}\to {k}{E}{Y}={x}{E}{Y}$
80 78 79 oveq12d
81 80 eqeq1d
82 76 81 imbi12d
83 82 cbvralvw
84 75 83 sylibr
85 10 11 17 37 38 84 gsummptnn0fz
86 85 fveq2d
87 86 fveq1d
88 simpllr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to {K}\in {ℕ}_{0}$
89 88 3ad2ant1 ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {K}\in {ℕ}_{0}$
90 36 expcom
91 elfznn0 ${⊢}{k}\in \left(0\dots {s}\right)\to {k}\in {ℕ}_{0}$
92 90 91 syl11
93 92 ralrimiv
94 fzfid ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left(0\dots {s}\right)\in \mathrm{Fin}$
95 8 10 20 89 93 94 coe1fzgsumd
96 87 95 eqtrd
97 96 mpoeq3dva
98 18 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {R}\in \mathrm{Ring}$
99 98 adantr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to {R}\in \mathrm{Ring}$
100 simpl2 ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to {i}\in {N}$
101 simpl3 ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to {j}\in {N}$
102 26 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {O}\in {L}$
103 102 91 30 syl2an ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\in {\mathrm{Base}}_{{A}}$
104 1 22 23 100 101 103 matecld ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}\in {\mathrm{Base}}_{{R}}$
105 91 adantl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to {k}\in {ℕ}_{0}$
106 43 22 8 6 4 34 5 coe1tm
107 99 104 105 106 syl3anc
108 eqeq1 ${⊢}{l}={K}\to \left({l}={k}↔{K}={k}\right)$
109 108 ifbid ${⊢}{l}={K}\to if\left({l}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)=if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)$
110 109 adantl ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\wedge {l}={K}\right)\to if\left({l}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)=if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)$
111 simpl1r ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to {K}\in {ℕ}_{0}$
112 ovex ${⊢}{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}\in \mathrm{V}$
113 fvex ${⊢}{0}_{{R}}\in \mathrm{V}$
114 112 113 ifex ${⊢}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\in \mathrm{V}$
115 114 a1i ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\in \mathrm{V}$
116 107 110 111 115 fvmptd
117 116 mpteq2dva
118 117 oveq2d
119 118 mpoeq3dva
121 breq2 ${⊢}{x}={K}\to \left({s}<{x}↔{s}<{K}\right)$
122 fveqeq2 ${⊢}{x}={K}\to \left({\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}↔{\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)$
123 121 122 imbi12d ${⊢}{x}={K}\to \left(\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)↔\left({s}<{K}\to {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\right)$
124 123 rspcva ${⊢}\left({K}\in {ℕ}_{0}\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to \left({s}<{K}\to {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)$
125 1 43 mat0op ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {0}_{{A}}=\left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)$
126 125 eqcomd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)={0}_{{A}}$
127 126 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)={0}_{{A}}$
128 127 ad3antlr ${⊢}\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\to \left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)={0}_{{A}}$
129 elfz2nn0 ${⊢}{k}\in \left(0\dots {s}\right)↔\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\wedge {k}\le {s}\right)$
130 nn0re ${⊢}{k}\in {ℕ}_{0}\to {k}\in ℝ$
131 130 ad2antrr ${⊢}\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\to {k}\in ℝ$
132 nn0re ${⊢}{s}\in {ℕ}_{0}\to {s}\in ℝ$
133 132 ad2antlr ${⊢}\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\to {s}\in ℝ$
134 nn0re ${⊢}{K}\in {ℕ}_{0}\to {K}\in ℝ$
135 134 adantl ${⊢}\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\to {K}\in ℝ$
136 lelttr ${⊢}\left({k}\in ℝ\wedge {s}\in ℝ\wedge {K}\in ℝ\right)\to \left(\left({k}\le {s}\wedge {s}<{K}\right)\to {k}<{K}\right)$
137 131 133 135 136 syl3anc ${⊢}\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left(\left({k}\le {s}\wedge {s}<{K}\right)\to {k}<{K}\right)$
138 animorr ${⊢}\left(\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}<{K}\right)\to \left({K}<{k}\vee {k}<{K}\right)$
139 df-ne ${⊢}{K}\ne {k}↔¬{K}={k}$
140 130 adantr ${⊢}\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\to {k}\in ℝ$
141 lttri2 ${⊢}\left({K}\in ℝ\wedge {k}\in ℝ\right)\to \left({K}\ne {k}↔\left({K}<{k}\vee {k}<{K}\right)\right)$
142 134 140 141 syl2anr ${⊢}\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left({K}\ne {k}↔\left({K}<{k}\vee {k}<{K}\right)\right)$
143 142 adantr ${⊢}\left(\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}<{K}\right)\to \left({K}\ne {k}↔\left({K}<{k}\vee {k}<{K}\right)\right)$
144 139 143 bitr3id ${⊢}\left(\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}<{K}\right)\to \left(¬{K}={k}↔\left({K}<{k}\vee {k}<{K}\right)\right)$
145 138 144 mpbird ${⊢}\left(\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {k}<{K}\right)\to ¬{K}={k}$
146 145 ex ${⊢}\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left({k}<{K}\to ¬{K}={k}\right)$
147 137 146 syld ${⊢}\left(\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left(\left({k}\le {s}\wedge {s}<{K}\right)\to ¬{K}={k}\right)$
148 147 exp4b ${⊢}\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\to \left({K}\in {ℕ}_{0}\to \left({k}\le {s}\to \left({s}<{K}\to ¬{K}={k}\right)\right)\right)$
149 148 com24 ${⊢}\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\to \left({s}<{K}\to \left({k}\le {s}\to \left({K}\in {ℕ}_{0}\to ¬{K}={k}\right)\right)\right)$
150 149 expimpd ${⊢}{k}\in {ℕ}_{0}\to \left(\left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\to \left({k}\le {s}\to \left({K}\in {ℕ}_{0}\to ¬{K}={k}\right)\right)\right)$
151 150 com23 ${⊢}{k}\in {ℕ}_{0}\to \left({k}\le {s}\to \left(\left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\to \left({K}\in {ℕ}_{0}\to ¬{K}={k}\right)\right)\right)$
152 151 imp ${⊢}\left({k}\in {ℕ}_{0}\wedge {k}\le {s}\right)\to \left(\left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\to \left({K}\in {ℕ}_{0}\to ¬{K}={k}\right)\right)$
153 152 3adant2 ${⊢}\left({k}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\wedge {k}\le {s}\right)\to \left(\left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\to \left({K}\in {ℕ}_{0}\to ¬{K}={k}\right)\right)$
154 129 153 sylbi ${⊢}{k}\in \left(0\dots {s}\right)\to \left(\left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\to \left({K}\in {ℕ}_{0}\to ¬{K}={k}\right)\right)$
155 154 com13 ${⊢}{K}\in {ℕ}_{0}\to \left(\left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\to \left({k}\in \left(0\dots {s}\right)\to ¬{K}={k}\right)\right)$
156 155 adantr ${⊢}\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\to \left(\left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\to \left({k}\in \left(0\dots {s}\right)\to ¬{K}={k}\right)\right)$
157 156 imp ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\to \left({k}\in \left(0\dots {s}\right)\to ¬{K}={k}\right)$
158 157 adantr ${⊢}\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\to \left({k}\in \left(0\dots {s}\right)\to ¬{K}={k}\right)$
159 158 3ad2ant1 ${⊢}\left(\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left({k}\in \left(0\dots {s}\right)\to ¬{K}={k}\right)$
160 159 imp ${⊢}\left(\left(\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to ¬{K}={k}$
161 160 iffalsed ${⊢}\left(\left(\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)={0}_{{R}}$
162 161 mpteq2dva ${⊢}\left(\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left({k}\in \left(0\dots {s}\right)⟼if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)=\left({k}\in \left(0\dots {s}\right)⟼{0}_{{R}}\right)$
163 162 oveq2d ${⊢}\left(\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)=\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}{0}_{{R}}$
164 ringmnd ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Mnd}$
165 164 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {R}\in \mathrm{Mnd}$
166 ovex ${⊢}\left(0\dots {s}\right)\in \mathrm{V}$
167 43 gsumz ${⊢}\left({R}\in \mathrm{Mnd}\wedge \left(0\dots {s}\right)\in \mathrm{V}\right)\to \underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}{0}_{{R}}={0}_{{R}}$
168 165 166 167 sylancl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}{0}_{{R}}={0}_{{R}}$
169 168 ad3antlr ${⊢}\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\to \underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}{0}_{{R}}={0}_{{R}}$
170 169 3ad2ant1 ${⊢}\left(\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}{0}_{{R}}={0}_{{R}}$
171 163 170 eqtrd ${⊢}\left(\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)={0}_{{R}}$
172 171 mpoeq3dva ${⊢}\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)=\left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)$
173 simpr ${⊢}\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}$
174 128 172 173 3eqtr4d ${⊢}\left(\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)$
175 174 ex ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge \left({s}\in {ℕ}_{0}\wedge {s}<{K}\right)\right)\to \left({\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)$
176 175 expr ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge {s}\in {ℕ}_{0}\right)\to \left({s}<{K}\to \left({\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)\right)$
177 176 a2d ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\right)\wedge {s}\in {ℕ}_{0}\right)\to \left(\left({s}<{K}\to {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\to \left({s}<{K}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)\right)$
178 177 exp31 ${⊢}{K}\in {ℕ}_{0}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({s}\in {ℕ}_{0}\to \left(\left({s}<{K}\to {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\to \left({s}<{K}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)\right)\right)\right)$
179 178 com14 ${⊢}\left({s}<{K}\to {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)={0}_{{A}}\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({s}\in {ℕ}_{0}\to \left({K}\in {ℕ}_{0}\to \left({s}<{K}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)\right)\right)\right)$
180 124 179 syl ${⊢}\left({K}\in {ℕ}_{0}\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({s}\in {ℕ}_{0}\to \left({K}\in {ℕ}_{0}\to \left({s}<{K}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)\right)\right)\right)$
181 180 ex ${⊢}{K}\in {ℕ}_{0}\to \left(\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({s}\in {ℕ}_{0}\to \left({K}\in {ℕ}_{0}\to \left({s}<{K}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)\right)\right)\right)\right)$
182 181 com25 ${⊢}{K}\in {ℕ}_{0}\to \left({K}\in {ℕ}_{0}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({s}\in {ℕ}_{0}\to \left(\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\to \left({s}<{K}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)\right)\right)\right)\right)$
183 182 pm2.43i ${⊢}{K}\in {ℕ}_{0}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \left({s}\in {ℕ}_{0}\to \left(\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\to \left({s}<{K}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)\right)\right)\right)$
184 183 impcom ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left({s}\in {ℕ}_{0}\to \left(\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\to \left({s}<{K}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)\right)\right)$
185 184 imp31 ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to \left({s}<{K}\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)$
186 185 com12 ${⊢}{s}<{K}\to \left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)$
187 165 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to {R}\in \mathrm{Mnd}$
188 187 adantl ${⊢}\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\to {R}\in \mathrm{Mnd}$
189 188 3ad2ant1 ${⊢}\left(\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {R}\in \mathrm{Mnd}$
190 ovexd ${⊢}\left(\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left(0\dots {s}\right)\in \mathrm{V}$
191 lenlt ${⊢}\left({K}\in ℝ\wedge {s}\in ℝ\right)\to \left({K}\le {s}↔¬{s}<{K}\right)$
192 134 132 191 syl2an ${⊢}\left({K}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\to \left({K}\le {s}↔¬{s}<{K}\right)$
193 simpll ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\le {s}\right)\to {K}\in {ℕ}_{0}$
194 simplr ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\le {s}\right)\to {s}\in {ℕ}_{0}$
195 simpr ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\le {s}\right)\to {K}\le {s}$
196 elfz2nn0 ${⊢}{K}\in \left(0\dots {s}\right)↔\left({K}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\wedge {K}\le {s}\right)$
197 193 194 195 196 syl3anbrc ${⊢}\left(\left({K}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\wedge {K}\le {s}\right)\to {K}\in \left(0\dots {s}\right)$
198 197 ex ${⊢}\left({K}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\to \left({K}\le {s}\to {K}\in \left(0\dots {s}\right)\right)$
199 192 198 sylbird ${⊢}\left({K}\in {ℕ}_{0}\wedge {s}\in {ℕ}_{0}\right)\to \left(¬{s}<{K}\to {K}\in \left(0\dots {s}\right)\right)$
200 199 ad4ant23 ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to \left(¬{s}<{K}\to {K}\in \left(0\dots {s}\right)\right)$
201 200 impcom ${⊢}\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\to {K}\in \left(0\dots {s}\right)$
202 201 3ad2ant1 ${⊢}\left(\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {K}\in \left(0\dots {s}\right)$
203 eqcom ${⊢}{K}={k}↔{k}={K}$
204 ifbi ${⊢}\left({K}={k}↔{k}={K}\right)\to if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)=if\left({k}={K},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)$
205 203 204 ax-mp ${⊢}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)=if\left({k}={K},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)$
206 205 mpteq2i ${⊢}\left({k}\in \left(0\dots {s}\right)⟼if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)=\left({k}\in \left(0\dots {s}\right)⟼if\left({k}={K},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)$
207 simpl2 ${⊢}\left(\left(\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {i}\in {N}$
208 simpl3 ${⊢}\left(\left(\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {j}\in {N}$
209 27 adantl ${⊢}\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\to {O}\in {L}$
210 209 3ad2ant1 ${⊢}\left(\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {O}\in {L}$
211 210 30 sylan ${⊢}\left(\left(\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\in {\mathrm{Base}}_{{A}}$
212 1 22 23 207 208 211 matecld ${⊢}\left(\left(\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}\in {\mathrm{Base}}_{{R}}$
213 91 212 sylan2 ${⊢}\left(\left(\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in \left(0\dots {s}\right)\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}\in {\mathrm{Base}}_{{R}}$
214 213 ralrimiva ${⊢}\left(\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \forall {k}\in \left(0\dots {s}\right)\phantom{\rule{.4em}{0ex}}{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}\in {\mathrm{Base}}_{{R}}$
215 43 189 190 202 206 214 gsummpt1n0
216 215 mpoeq3dva
217 csbov
218 csbfv
219 218 a1i
220 219 oveqd
221 217 220 syl5eq
223 222 mpoeq3dv
224 oveq12 ${⊢}\left({i}={a}\wedge {j}={b}\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({K}\right){j}={a}{\mathrm{coe}}_{1}\left({O}\right)\left({K}\right){b}$
225 224 adantl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\wedge \left({i}={a}\wedge {j}={b}\right)\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({K}\right){j}={a}{\mathrm{coe}}_{1}\left({O}\right)\left({K}\right){b}$
226 simprl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {a}\in {N}$
227 simprr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {b}\in {N}$
228 ovexd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {a}{\mathrm{coe}}_{1}\left({O}\right)\left({K}\right){b}\in \mathrm{V}$
229 223 225 226 227 228 ovmpod
230 229 ralrimivva
231 simpl1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to {N}\in \mathrm{Fin}$
232 218 oveqi
233 217 232 eqtri
234 simp2 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}\in {N}$
235 simp3 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {j}\in {N}$
236 29 3 2 23 coe1fvalcl ${⊢}\left({O}\in {L}\wedge {K}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\in {\mathrm{Base}}_{{A}}$
237 236 3ad2antl3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\in {\mathrm{Base}}_{{A}}$
238 237 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\in {\mathrm{Base}}_{{A}}$
239 1 22 23 234 235 238 matecld ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({K}\right){j}\in {\mathrm{Base}}_{{R}}$
240 233 239 eqeltrid
241 1 22 23 231 18 240 matbas2d
242 1 23 eqmat
243 241 237 242 syl2anc
244 230 243 mpbird
247 216 246 eqtrd ${⊢}\left(¬{s}<{K}\wedge \left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\right)\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)$
248 247 ex ${⊢}¬{s}<{K}\to \left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)\right)$
249 186 248 pm2.61i ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge \forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)\to \left({i}\in {N},{j}\in {N}⟼\underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}if\left({K}={k},{i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j},{0}_{{R}}\right)\right)={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)$
250 97 120 249 3eqtrd
251 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
252 29 3 2 251 coe1sfi ${⊢}{O}\in {L}\to {finSupp}_{{0}_{{A}}}\left({\mathrm{coe}}_{1}\left({O}\right)\right)$
253 26 252 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to {finSupp}_{{0}_{{A}}}\left({\mathrm{coe}}_{1}\left({O}\right)\right)$
254 29 3 2 251 23 coe1fsupp ${⊢}{O}\in {L}\to {\mathrm{coe}}_{1}\left({O}\right)\in \left\{{x}\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)|{finSupp}_{{0}_{{A}}}\left({x}\right)\right\}$
255 elrabi ${⊢}{\mathrm{coe}}_{1}\left({O}\right)\in \left\{{x}\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)|{finSupp}_{{0}_{{A}}}\left({x}\right)\right\}\to {\mathrm{coe}}_{1}\left({O}\right)\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)$
256 26 254 255 3syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)$
257 fvex ${⊢}{0}_{{A}}\in \mathrm{V}$
258 fsuppmapnn0ub ${⊢}\left({\mathrm{coe}}_{1}\left({O}\right)\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)\wedge {0}_{{A}}\in \mathrm{V}\right)\to \left({finSupp}_{{0}_{{A}}}\left({\mathrm{coe}}_{1}\left({O}\right)\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)$
259 256 257 258 sylancl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to \left({finSupp}_{{0}_{{A}}}\left({\mathrm{coe}}_{1}\left({O}\right)\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)$
260 253 259 mpd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)$
261 250 260 r19.29a
262 9 261 eqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {K}\in {ℕ}_{0}\right)\to {I}\left({O}\right)\mathrm{decompPMat}{K}={\mathrm{coe}}_{1}\left({O}\right)\left({K}\right)$