# Metamath Proof Explorer

## Theorem m2cpminvid2lem

Description: Lemma for m2cpminvid2 . (Contributed by AV, 12-Nov-2019) (Revised by AV, 14-Dec-2019)

Ref Expression
Hypotheses m2cpminvid2lem.s ${⊢}{S}={N}\mathrm{ConstPolyMat}{R}$
m2cpminvid2lem.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
Assertion m2cpminvid2lem ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)$

### Proof

Step Hyp Ref Expression
1 m2cpminvid2lem.s ${⊢}{S}={N}\mathrm{ConstPolyMat}{R}$
2 m2cpminvid2lem.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
3 eqid ${⊢}{N}\mathrm{Mat}{P}={N}\mathrm{Mat}{P}$
4 eqid ${⊢}{\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}$
5 1 2 3 4 cpmatelimp ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({M}\in {S}\to \left({M}\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}\wedge \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)\right)$
6 5 3impia ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\to \left({M}\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}\wedge \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)$
7 6 simprd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}$
8 7 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}$
9 fvoveq1 ${⊢}{i}={x}\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)={\mathrm{coe}}_{1}\left({x}{M}{j}\right)$
10 9 fveq1d ${⊢}{i}={x}\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={\mathrm{coe}}_{1}\left({x}{M}{j}\right)\left({k}\right)$
11 10 eqeq1d ${⊢}{i}={x}\to \left({\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}↔{\mathrm{coe}}_{1}\left({x}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)$
12 11 ralbidv ${⊢}{i}={x}\to \left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)$
13 oveq2 ${⊢}{j}={y}\to {x}{M}{j}={x}{M}{y}$
14 13 fveq2d ${⊢}{j}={y}\to {\mathrm{coe}}_{1}\left({x}{M}{j}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)$
15 14 fveq1d ${⊢}{j}={y}\to {\mathrm{coe}}_{1}\left({x}{M}{j}\right)\left({k}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({k}\right)$
16 15 eqeq1d ${⊢}{j}={y}\to \left({\mathrm{coe}}_{1}\left({x}{M}{j}\right)\left({k}\right)={0}_{{R}}↔{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({k}\right)={0}_{{R}}\right)$
17 16 ralbidv ${⊢}{j}={y}\to \left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{j}\right)\left({k}\right)={0}_{{R}}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({k}\right)={0}_{{R}}\right)$
18 12 17 rspc2v ${⊢}\left({x}\in {N}\wedge {y}\in {N}\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({k}\right)={0}_{{R}}\right)$
19 18 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({k}\right)={0}_{{R}}\right)$
20 fveqeq2 ${⊢}{k}={n}\to \left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({k}\right)={0}_{{R}}↔{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}\right)$
21 20 cbvralvw ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({k}\right)={0}_{{R}}↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}$
22 simpl2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {R}\in \mathrm{Ring}$
23 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
24 simprl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {x}\in {N}$
25 simprr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {y}\in {N}$
26 1 2 3 4 cpmatpmat ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\to {M}\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}$
27 26 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {M}\in {\mathrm{Base}}_{\left({N}\mathrm{Mat}{P}\right)}$
28 3 23 4 24 25 27 matecld ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {x}{M}{y}\in {\mathrm{Base}}_{{P}}$
29 0nn0 ${⊢}0\in {ℕ}_{0}$
30 eqid ${⊢}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)$
31 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
32 30 23 2 31 coe1fvalcl ${⊢}\left({x}{M}{y}\in {\mathrm{Base}}_{{P}}\wedge 0\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\in {\mathrm{Base}}_{{R}}$
33 28 29 32 sylancl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\in {\mathrm{Base}}_{{R}}$
34 22 33 jca ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\in {\mathrm{Base}}_{{R}}\right)$
35 34 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to \left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\in {\mathrm{Base}}_{{R}}\right)$
36 eqid ${⊢}\mathrm{algSc}\left({P}\right)=\mathrm{algSc}\left({P}\right)$
37 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
38 2 36 31 37 coe1scl ${⊢}\left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\in {\mathrm{Base}}_{{R}}\right)\to {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)=\left({l}\in {ℕ}_{0}⟼if\left({l}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)\right)$
39 35 38 syl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)=\left({l}\in {ℕ}_{0}⟼if\left({l}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)\right)$
40 39 fveq1d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)=\left({l}\in {ℕ}_{0}⟼if\left({l}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)\right)\left({n}\right)$
41 eqidd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to \left({l}\in {ℕ}_{0}⟼if\left({l}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)\right)=\left({l}\in {ℕ}_{0}⟼if\left({l}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)\right)$
42 eqeq1 ${⊢}{l}={n}\to \left({l}=0↔{n}=0\right)$
43 42 ifbid ${⊢}{l}={n}\to if\left({l}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)=if\left({n}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)$
44 43 adantl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\wedge {l}={n}\right)\to if\left({l}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)=if\left({n}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)$
45 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
46 45 adantl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to {n}\in {ℕ}_{0}$
47 fvex ${⊢}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\in \mathrm{V}$
48 fvex ${⊢}{0}_{{R}}\in \mathrm{V}$
49 47 48 ifex ${⊢}if\left({n}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)\in \mathrm{V}$
50 49 a1i ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to if\left({n}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)\in \mathrm{V}$
51 41 44 46 50 fvmptd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to \left({l}\in {ℕ}_{0}⟼if\left({l}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)\right)\left({n}\right)=if\left({n}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)$
52 nnne0 ${⊢}{n}\in ℕ\to {n}\ne 0$
53 52 neneqd ${⊢}{n}\in ℕ\to ¬{n}=0$
54 53 adantl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to ¬{n}=0$
55 54 iffalsed ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to if\left({n}=0,{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right),{0}_{{R}}\right)={0}_{{R}}$
56 40 51 55 3eqtrd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={0}_{{R}}$
57 eqcom ${⊢}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}↔{0}_{{R}}={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)$
58 57 biimpi ${⊢}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}\to {0}_{{R}}={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)$
59 56 58 sylan9eq ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\wedge {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}\right)\to {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)$
60 59 ex ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {n}\in ℕ\right)\to \left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}\to {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)\right)$
61 60 ralimdva ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)\right)$
62 61 imp ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)$
63 34 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}\right)\to \left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\in {\mathrm{Base}}_{{R}}\right)$
64 2 36 31 ply1sclid ${⊢}\left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\in {\mathrm{Base}}_{{R}}\right)\to {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)={\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)$
65 64 eqcomd ${⊢}\left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\in {\mathrm{Base}}_{{R}}\right)\to {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)$
66 63 65 syl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}\right)\to {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)$
67 62 66 jca ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}\right)\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)\wedge {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)$
68 67 ex ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={0}_{{R}}\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)\wedge {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)$
69 21 68 syl5bi ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({k}\right)={0}_{{R}}\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)\wedge {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)$
70 19 69 syld ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)\wedge {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)$
71 8 70 mpd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)\wedge {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)$
72 c0ex ${⊢}0\in \mathrm{V}$
73 fveq2 ${⊢}{n}=0\to {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)$
74 fveq2 ${⊢}{n}=0\to {\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)$
75 73 74 eqeq12d ${⊢}{n}=0\to \left({\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)↔{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)$
76 75 ralunsn ${⊢}0\in \mathrm{V}\to \left(\forall {n}\in \left(ℕ\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)↔\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)\wedge {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)$
77 72 76 mp1i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left(\forall {n}\in \left(ℕ\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)↔\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)\wedge {\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left(0\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)$
78 71 77 mpbird ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \forall {n}\in \left(ℕ\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)$
79 df-n0 ${⊢}{ℕ}_{0}=ℕ\cup \left\{0\right\}$
80 79 raleqi ${⊢}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)↔\forall {n}\in \left(ℕ\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)$
81 78 80 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {S}\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({x}{M}{y}\right)\left({n}\right)$