# Metamath Proof Explorer

## Theorem cpmatmcllem

Description: Lemma for cpmatmcl . (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses cpmatsrngpmat.s ${⊢}{S}={N}\mathrm{ConstPolyMat}{R}$
cpmatsrngpmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
cpmatsrngpmat.c ${⊢}{C}={N}\mathrm{Mat}{P}$
Assertion cpmatmcllem ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}$

### Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s ${⊢}{S}={N}\mathrm{ConstPolyMat}{R}$
2 cpmatsrngpmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
3 cpmatsrngpmat.c ${⊢}{C}={N}\mathrm{Mat}{P}$
4 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
5 1 2 3 4 cpmatelimp ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({x}\in {S}\to \left({x}\in {\mathrm{Base}}_{{C}}\wedge \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\right)\right)$
6 1 2 3 4 cpmatelimp ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({y}\in {S}\to \left({y}\in {\mathrm{Base}}_{{C}}\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)$
7 6 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({y}\in {S}\to \left({y}\in {\mathrm{Base}}_{{C}}\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)$
8 ralcom ${⊢}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}↔\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}$
9 r19.26-2 ${⊢}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)↔\left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)$
10 ralcom ${⊢}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)↔\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)$
11 9 10 bitr3i ${⊢}\left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)↔\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)$
12 nfv ${⊢}Ⅎ{c}\phantom{\rule{.4em}{0ex}}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)$
13 nfra1 ${⊢}Ⅎ{c}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)$
14 12 13 nfan ${⊢}Ⅎ{c}\phantom{\rule{.4em}{0ex}}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)$
15 simp-4r ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to {R}\in \mathrm{Ring}$
16 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
17 simplrl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to {i}\in {N}$
18 simpr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to {k}\in {N}$
19 simplrl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
20 19 adantr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
21 3 16 4 17 18 20 matecld ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to {i}{x}{k}\in {\mathrm{Base}}_{{P}}$
22 simplrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to {j}\in {N}$
23 simplrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {y}\in {\mathrm{Base}}_{{C}}$
24 23 adantr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to {y}\in {\mathrm{Base}}_{{C}}$
25 3 16 4 18 22 24 matecld ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to {k}{y}{j}\in {\mathrm{Base}}_{{P}}$
26 15 21 25 jca32 ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to \left({R}\in \mathrm{Ring}\wedge \left({i}{x}{k}\in {\mathrm{Base}}_{{P}}\wedge {k}{y}{j}\in {\mathrm{Base}}_{{P}}\right)\right)$
27 26 adantlr ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\wedge {k}\in {N}\right)\to \left({R}\in \mathrm{Ring}\wedge \left({i}{x}{k}\in {\mathrm{Base}}_{{P}}\wedge {k}{y}{j}\in {\mathrm{Base}}_{{P}}\right)\right)$
28 oveq2 ${⊢}{l}={k}\to {i}{x}{l}={i}{x}{k}$
29 28 fveq2d ${⊢}{l}={k}\to {\mathrm{coe}}_{1}\left({i}{x}{l}\right)={\mathrm{coe}}_{1}\left({i}{x}{k}\right)$
30 29 fveq1d ${⊢}{l}={k}\to {\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)$
31 30 eqeq1d ${⊢}{l}={k}\to \left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}↔{\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\right)$
32 fvoveq1 ${⊢}{l}={k}\to {\mathrm{coe}}_{1}\left({l}{y}{j}\right)={\mathrm{coe}}_{1}\left({k}{y}{j}\right)$
33 32 fveq1d ${⊢}{l}={k}\to {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)$
34 33 eqeq1d ${⊢}{l}={k}\to \left({\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}↔{\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)$
35 31 34 anbi12d ${⊢}{l}={k}\to \left(\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)↔\left({\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)$
36 35 rspcva ${⊢}\left({k}\in {N}\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\to \left({\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)$
37 36 a1i ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {c}\in ℕ\right)\to \left(\left({k}\in {N}\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\to \left({\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)$
38 37 exp4b ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left({c}\in ℕ\to \left({k}\in {N}\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\to \left({\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\right)\right)$
39 38 com23 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left({k}\in {N}\to \left({c}\in ℕ\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\to \left({\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\right)\right)$
40 39 imp31 ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\wedge {c}\in ℕ\right)\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\to \left({\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)$
41 40 ralimdva ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to \left(\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)$
42 41 impancom ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\to \left({k}\in {N}\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)$
43 42 imp ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\wedge {k}\in {N}\right)\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)$
44 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
45 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
46 2 16 44 45 cply1mul ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({i}{x}{k}\in {\mathrm{Base}}_{{P}}\wedge {k}{y}{j}\in {\mathrm{Base}}_{{P}}\right)\right)\to \left(\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{k}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({k}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)={0}_{{R}}\right)$
47 27 43 46 sylc ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\wedge {k}\in {N}\right)\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)={0}_{{R}}$
48 47 r19.21bi ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\wedge {k}\in {N}\right)\wedge {c}\in ℕ\right)\to {\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)={0}_{{R}}$
49 48 an32s ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\wedge {c}\in ℕ\right)\wedge {k}\in {N}\right)\to {\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)={0}_{{R}}$
50 49 mpteq2dva ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\wedge {c}\in ℕ\right)\to \left({k}\in {N}⟼{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)\right)=\left({k}\in {N}⟼{0}_{{R}}\right)$
51 50 oveq2d ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\wedge {c}\in ℕ\right)\to \underset{{k}\in {N}}{{\sum }_{{R}}}{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)=\underset{{k}\in {N}}{{\sum }_{{R}}}{0}_{{R}}$
52 ringmnd ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Mnd}$
53 52 anim2i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Mnd}\right)$
54 53 ancomd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({R}\in \mathrm{Mnd}\wedge {N}\in \mathrm{Fin}\right)$
55 44 gsumz ${⊢}\left({R}\in \mathrm{Mnd}\wedge {N}\in \mathrm{Fin}\right)\to \underset{{k}\in {N}}{{\sum }_{{R}}}{0}_{{R}}={0}_{{R}}$
56 54 55 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \underset{{k}\in {N}}{{\sum }_{{R}}}{0}_{{R}}={0}_{{R}}$
57 56 ad4antr ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\wedge {c}\in ℕ\right)\to \underset{{k}\in {N}}{{\sum }_{{R}}}{0}_{{R}}={0}_{{R}}$
58 51 57 eqtrd ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\wedge {c}\in ℕ\right)\to \underset{{k}\in {N}}{{\sum }_{{R}}}{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)={0}_{{R}}$
59 58 ex ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\to \left({c}\in ℕ\to \underset{{k}\in {N}}{{\sum }_{{R}}}{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)={0}_{{R}}\right)$
60 14 59 ralrimi ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\underset{{k}\in {N}}{{\sum }_{{R}}}{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)={0}_{{R}}$
61 simp-4r ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {c}\in ℕ\right)\to {R}\in \mathrm{Ring}$
62 nnnn0 ${⊢}{c}\in ℕ\to {c}\in {ℕ}_{0}$
63 62 adantl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {c}\in ℕ\right)\to {c}\in {ℕ}_{0}$
64 2 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
65 64 ad4antlr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to {P}\in \mathrm{Ring}$
66 16 45 ringcl ${⊢}\left({P}\in \mathrm{Ring}\wedge {i}{x}{k}\in {\mathrm{Base}}_{{P}}\wedge {k}{y}{j}\in {\mathrm{Base}}_{{P}}\right)\to \left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\in {\mathrm{Base}}_{{P}}$
67 65 21 25 66 syl3anc ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {k}\in {N}\right)\to \left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\in {\mathrm{Base}}_{{P}}$
68 67 ralrimiva ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \forall {k}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\in {\mathrm{Base}}_{{P}}$
69 68 adantr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {c}\in ℕ\right)\to \forall {k}\in {N}\phantom{\rule{.4em}{0ex}}\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\in {\mathrm{Base}}_{{P}}$
70 simp-4l ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {c}\in ℕ\right)\to {N}\in \mathrm{Fin}$
71 2 16 61 63 69 70 coe1fzgsumd ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {c}\in ℕ\right)\to {\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)=\underset{{k}\in {N}}{{\sum }_{{R}}}{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)$
72 71 eqeq1d ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge {c}\in ℕ\right)\to \left({\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}↔\underset{{k}\in {N}}{{\sum }_{{R}}}{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)={0}_{{R}}\right)$
73 72 ralbidva ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left(\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}↔\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\underset{{k}\in {N}}{{\sum }_{{R}}}{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)={0}_{{R}}\right)$
74 73 adantr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\to \left(\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}↔\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\underset{{k}\in {N}}{{\sum }_{{R}}}{\mathrm{coe}}_{1}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\left({c}\right)={0}_{{R}}\right)$
75 60 74 mpbird ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\wedge \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\right)\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}$
76 75 ex ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left(\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\left({\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge {\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
77 11 76 syl5bi ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left(\left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
78 77 expd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)$
79 78 expr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {i}\in {N}\right)\to \left({j}\in {N}\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)\right)$
80 79 com23 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {i}\in {N}\right)\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \left({j}\in {N}\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)\right)$
81 80 imp31 ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {i}\in {N}\right)\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\right)\wedge {j}\in {N}\right)\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\to \forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
82 81 ralimdva ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {i}\in {N}\right)\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\right)\to \left(\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\to \forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
83 8 82 syl5bi ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {i}\in {N}\right)\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\right)\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\to \forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
84 83 ex ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {i}\in {N}\right)\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\to \forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)$
85 84 com23 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge {i}\in {N}\right)\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)$
86 85 impancom ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\to \left({i}\in {N}\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)$
87 86 imp ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\wedge {i}\in {N}\right)\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
88 87 ralimdva ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
89 88 ex ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\right)\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)$
90 89 expr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({y}\in {\mathrm{Base}}_{{C}}\to \left(\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)\right)$
91 90 impd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left(\left({y}\in {\mathrm{Base}}_{{C}}\wedge \forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({l}{y}{j}\right)\left({c}\right)={0}_{{R}}\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)$
92 7 91 syld ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left({y}\in {S}\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)$
93 92 com23 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {\mathrm{Base}}_{{C}}\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \left({y}\in {S}\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)$
94 93 ex ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({x}\in {\mathrm{Base}}_{{C}}\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\to \left({y}\in {S}\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)\right)$
95 94 impd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left(\left({x}\in {\mathrm{Base}}_{{C}}\wedge \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {l}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{x}{l}\right)\left({c}\right)={0}_{{R}}\right)\to \left({y}\in {S}\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)$
96 5 95 syld ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({x}\in {S}\to \left({y}\in {S}\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)\right)$
97 96 imp32 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}$