Theorem mhpmulcl

Description: A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024) Remove sethood hypothesis. (Revised by SN, 18-May-2025)

	Ref	Expression
Hypotheses	mhpmulcl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpmulcl.y	$$⊢Y=I\mathrm{mPoly}R$$
	mhpmulcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	mhpmulcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mhpmulcl.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	mhpmulcl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	mhpmulcl.p	$$⊢\phi \to P\in H\left(M\right)$$
	mhpmulcl.q	$$⊢\phi \to Q\in H\left(N\right)$$
Assertion	mhpmulcl	$$⊢\phi \to P\underset{\dot{}}{·}Q\in H\left(M+N\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhpmulcl.h	$$⊢H=I\mathrm{mHomP}R$$
2		mhpmulcl.y	$$⊢Y=I\mathrm{mPoly}R$$
3		mhpmulcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
4		mhpmulcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		mhpmulcl.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
6		mhpmulcl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		mhpmulcl.p	$$⊢\phi \to P\in H\left(M\right)$$
8		mhpmulcl.q	$$⊢\phi \to Q\in H\left(N\right)$$
9		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
10		eqid	$$⊢{\cdot }_R={\cdot }_R$$
11		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
12		reldmmhp	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mHomP}$$
13	12 1 7	elfvov1	$$⊢\phi \to I\in \mathrm{V}$$
14	1 2 9 13 4 5 7	mhpmpl	$$⊢\phi \to P\in {\mathrm{Base}}_Y$$
15	1 2 9 13 4 6 8	mhpmpl	$$⊢\phi \to Q\in {\mathrm{Base}}_Y$$
16	2 9 10 3 11 14 15	mplmul	$$⊢\phi \to P\underset{\dot{}}{·}Q=\left(d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}d\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(d{-}_{f}e\right)\right)\right)$$
17	16	adantr	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to P\underset{\dot{}}{·}Q=\left(d\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}d\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(d{-}_{f}e\right)\right)\right)$$
18		breq2	$$⊢d=x\to \left(c{\le }_{f}d\leftrightarrow c{\le }_{f}x\right)$$
19	18	rabbidv	$$⊢d=x\to \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}d\right\}=\left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}$$
20		fvoveq1	$$⊢d=x\to Q\left(d{-}_{f}e\right)=Q\left(x{-}_{f}e\right)$$
21	20	oveq2d	$$⊢d=x\to P\left(e\right){\cdot }_{R}Q\left(d{-}_{f}e\right)=P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)$$
22	19 21	mpteq12dv	$$⊢d=x\to \left(e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}d\right\}⟼P\left(e\right){\cdot }_{R}Q\left(d{-}_{f}e\right)\right)=\left(e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}⟼P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)$$
23	22	oveq2d	$$⊢d=x\to \underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}d\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(d{-}_{f}e\right)\right)=\underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)$$
24	23	adantl	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d=x\right)\to \underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}d\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(d{-}_{f}e\right)\right)=\underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)$$
25		simpr	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
26		ovexd	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)\in \mathrm{V}$$
27	17 24 25 26	fvmptd	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(P\underset{\dot{}}{·}Q\right)\left(x\right)=\underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)$$
28	27	neeq1d	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(\left(P\underset{\dot{}}{·}Q\right)\left(x\right)\ne 0_R\leftrightarrow \underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)\ne 0_R\right)$$
29		simp-4l	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to \phi$$
30		oveq2	$$⊢c=e\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c={\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e$$
31	30	eqeq1d	$$⊢c=e\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=M\leftrightarrow {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e=M\right)$$
32	31	necon3bbid	$$⊢c=e\to \left(\neg {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=M\leftrightarrow {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)$$
33		simplr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}$$
34		elrabi	$$⊢e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\to e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
35	33 34	syl	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
36		simpr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M$$
37	32 35 36	elrabd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|\neg {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=M\right\}$$
38		notrab	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=M\right\}=\left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|\neg {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=M\right\}$$
39	37 38	eleqtrrdi	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to e\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=M\right\}\right)$$
40		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
41	2 40 9 11 14	mplelf	$$⊢\phi \to P:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
42		eqid	$$⊢0_R=0_R$$
43	1 42 11 13 4 5 7	mhpdeg	$$⊢\phi \to P\mathrm{supp}{0}_R\subseteq \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=M\right\}$$
44		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
45	44	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
46	45	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
47		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
48	41 43 46 47	suppssr	$$⊢\left(\phi \wedge e\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=M\right\}\right)\right)\to P\left(e\right)=0_R$$
49	29 39 48	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to P\left(e\right)=0_R$$
50	49	oveq1d	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)=0_R{\cdot }_{R}Q\left(x{-}_{f}e\right)$$
51	4	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to R\in \mathrm{Ring}$$
52	15	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to Q\in {\mathrm{Base}}_Y$$
53	2 40 9 11 52	mplelf	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to Q:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
54		simp-4r	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
55		eqid	$$⊢\left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}=\left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}$$
56	11 55	psrbagconcl	$$⊢\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to x{-}_{f}e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}$$
57	54 33 56	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to x{-}_{f}e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}$$
58		elrabi	$$⊢x{-}_{f}e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\to x{-}_{f}e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
59	57 58	syl	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to x{-}_{f}e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
60	53 59	ffvelcdmd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to Q\left(x{-}_{f}e\right)\in {\mathrm{Base}}_R$$
61	40 10 42	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge Q\left(x{-}_{f}e\right)\in {\mathrm{Base}}_R\right)\to 0_R{\cdot }_{R}Q\left(x{-}_{f}e\right)=0_R$$
62	51 60 61	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to 0_R{\cdot }_{R}Q\left(x{-}_{f}e\right)=0_R$$
63	50 62	eqtrd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\right)\to P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)=0_R$$
64		simp-4l	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to \phi$$
65		oveq2	$$⊢c=x{-}_{f}e\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c={\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)$$
66	65	eqeq1d	$$⊢c=x{-}_{f}e\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=N\leftrightarrow {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)=N\right)$$
67	66	necon3bbid	$$⊢c=x{-}_{f}e\to \left(\neg {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=N\leftrightarrow {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)$$
68		simp-4r	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
69		simplr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}$$
70	68 69 56	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to x{-}_{f}e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}$$
71	70 58	syl	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to x{-}_{f}e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
72		simpr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N$$
73	67 71 72	elrabd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to x{-}_{f}e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|\neg {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=N\right\}$$
74		notrab	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=N\right\}=\left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|\neg {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=N\right\}$$
75	73 74	eleqtrrdi	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to x{-}_{f}e\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=N\right\}\right)$$
76	2 40 9 11 15	mplelf	$$⊢\phi \to Q:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
77	1 42 11 13 4 6 8	mhpdeg	$$⊢\phi \to Q\mathrm{supp}{0}_R\subseteq \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=N\right\}$$
78	76 77 46 47	suppssr	$$⊢\left(\phi \wedge x{-}_{f}e\in \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\setminus \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c=N\right\}\right)\right)\to Q\left(x{-}_{f}e\right)=0_R$$
79	64 75 78	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to Q\left(x{-}_{f}e\right)=0_R$$
80	79	oveq2d	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)=P\left(e\right){\cdot }_R{0}_R$$
81	4	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to R\in \mathrm{Ring}$$
82	14	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to P\in {\mathrm{Base}}_Y$$
83	2 40 9 11 82	mplelf	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to P:\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
84	34	adantl	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
85	84	adantr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
86	83 85	ffvelcdmd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to P\left(e\right)\in {\mathrm{Base}}_R$$
87	40 10 42	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge P\left(e\right)\in {\mathrm{Base}}_R\right)\to P\left(e\right){\cdot }_R{0}_R=0_R$$
88	81 86 87	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to P\left(e\right){\cdot }_R{0}_R=0_R$$
89	80 88	eqtrd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\to P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)=0_R$$
90		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
91		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
92	91	submbas	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to {\mathbb{N}}_0={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
93	90 92	ax-mp	$$⊢{\mathbb{N}}_0={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
94		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
95	91 94	subm0	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to 0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
96	90 95	ax-mp	$$⊢0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
97		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
98		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
99	91 98	ressplusg	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to +={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
100	97 99	ax-mp	$$⊢+={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
101		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
102		ringcmn	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
103	101 102	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
104	91	submcmn	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}\wedge {\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{CMnd}$$
105	103 90 104	mp2an	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{CMnd}$$
106	105	a1i	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{CMnd}$$
107	13	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to I\in \mathrm{V}$$
108	11	psrbagf	$$⊢e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to e:I⟶{\mathbb{N}}_0$$
109	84 108	syl	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to e:I⟶{\mathbb{N}}_0$$
110		simpllr	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
111	11	psrbagf	$$⊢x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to x:I⟶{\mathbb{N}}_0$$
112	110 111	syl	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to x:I⟶{\mathbb{N}}_0$$
113	112	ffnd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to xFnI$$
114	109	ffnd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to eFnI$$
115		inidm	$$⊢I\cap I=I$$
116		eqidd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to x\left(i\right)=x\left(i\right)$$
117		eqidd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to e\left(i\right)=e\left(i\right)$$
118	113 114 107 107 115 116 117	offval	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to x{-}_{f}e=\left(i\in I⟼x\left(i\right)-e\left(i\right)\right)$$
119		simpl	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to \left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)$$
120		simplr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}$$
121		breq1	$$⊢c=e\to \left(c{\le }_{f}x\leftrightarrow e{\le }_{f}x\right)$$
122	121	elrab	$$⊢e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\leftrightarrow \left(e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge e{\le }_{f}x\right)$$
123	122	simprbi	$$⊢e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\to e{\le }_{f}x$$
124	120 123	syl	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to e{\le }_{f}x$$
125		simpr	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to i\in I$$
126	114 113 107 107 115 117 116	ofrval	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge e{\le }_{f}x\wedge i\in I\right)\to e\left(i\right)\le x\left(i\right)$$
127	119 124 125 126	syl3anc	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to e\left(i\right)\le x\left(i\right)$$
128	109	ffvelcdmda	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to e\left(i\right)\in {\mathbb{N}}_0$$
129	112	ffvelcdmda	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to x\left(i\right)\in {\mathbb{N}}_0$$
130		nn0sub	$$⊢\left(e\left(i\right)\in {\mathbb{N}}_0\wedge x\left(i\right)\in {\mathbb{N}}_0\right)\to \left(e\left(i\right)\le x\left(i\right)\leftrightarrow x\left(i\right)-e\left(i\right)\in {\mathbb{N}}_0\right)$$
131	128 129 130	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to \left(e\left(i\right)\le x\left(i\right)\leftrightarrow x\left(i\right)-e\left(i\right)\in {\mathbb{N}}_0\right)$$
132	127 131	mpbid	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge i\in I\right)\to x\left(i\right)-e\left(i\right)\in {\mathbb{N}}_0$$
133	118 132	fmpt3d	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left(x{-}_{f}e\right):I⟶{\mathbb{N}}_0$$
134	109	ffund	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \mathrm{Fun}e$$
135		c0ex	$$⊢0\in \mathrm{V}$$
136	107 135	jctir	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left(I\in \mathrm{V}\wedge 0\in \mathrm{V}\right)$$
137		fsuppeq	$$⊢\left(I\in \mathrm{V}\wedge 0\in \mathrm{V}\right)\to \left(e:I⟶{\mathbb{N}}_0\to e\mathrm{supp}0=e^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right)$$
138	136 109 137	sylc	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to e\mathrm{supp}0=e^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]$$
139		dfn2	$$⊢\mathbb{N}={\mathbb{N}}_0\setminus \left\{0\right\}$$
140	139	imaeq2i	$$⊢e^{-1}\left[\mathbb{N}\right]=e^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]$$
141	138 140	eqtr4di	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to e\mathrm{supp}0=e^{-1}\left[\mathbb{N}\right]$$
142	11	psrbag	$$⊢I\in \mathrm{V}\to \left(e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\leftrightarrow \left(e:I⟶{\mathbb{N}}_0\wedge e^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
143	107 142	syl	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left(e\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\leftrightarrow \left(e:I⟶{\mathbb{N}}_0\wedge e^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
144	84 143	mpbid	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left(e:I⟶{\mathbb{N}}_0\wedge e^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
145	144	simprd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to e^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
146	141 145	eqeltrd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to e\mathrm{supp}0\in \mathrm{Fin}$$
147	84	elexd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to e\in \mathrm{V}$$
148		isfsupp	$$⊢\left(e\in \mathrm{V}\wedge 0\in \mathrm{V}\right)\to \left({finSupp}_0\left(e\right)\leftrightarrow \left(\mathrm{Fun}e\wedge e\mathrm{supp}0\in \mathrm{Fin}\right)\right)$$
149	147 135 148	sylancl	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left({finSupp}_0\left(e\right)\leftrightarrow \left(\mathrm{Fun}e\wedge e\mathrm{supp}0\in \mathrm{Fin}\right)\right)$$
150	134 146 149	mpbir2and	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to {finSupp}_0\left(e\right)$$
151	113 114 107 107	offun	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \mathrm{Fun}\left(x{-}_{f}e\right)$$
152	11	psrbagfsupp	$$⊢x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to {finSupp}_0\left(x\right)$$
153	110 152	syl	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to {finSupp}_0\left(x\right)$$
154	153 150	fsuppunfi	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to {supp}_0\left(x\right)\cup {supp}_0\left(e\right)\in \mathrm{Fin}$$
155		0nn0	$$⊢0\in {\mathbb{N}}_0$$
156	155	a1i	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to 0\in {\mathbb{N}}_0$$
157		0m0e0	$$⊢0-0=0$$
158	157	a1i	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to 0-0=0$$
159	107 156 112 109 158	suppofssd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left(x{-}_{f}e\right)\mathrm{supp}0\subseteq {supp}_0\left(x\right)\cup {supp}_0\left(e\right)$$
160	154 159	ssfid	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left(x{-}_{f}e\right)\mathrm{supp}0\in \mathrm{Fin}$$
161		ovexd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to x{-}_{f}e\in \mathrm{V}$$
162		isfsupp	$$⊢\left(x{-}_{f}e\in \mathrm{V}\wedge 0\in \mathrm{V}\right)\to \left({finSupp}_0\left(\left(x{-}_{f}e\right)\right)\leftrightarrow \left(\mathrm{Fun}\left(x{-}_{f}e\right)\wedge \left(x{-}_{f}e\right)\mathrm{supp}0\in \mathrm{Fin}\right)\right)$$
163	161 135 162	sylancl	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left({finSupp}_0\left(\left(x{-}_{f}e\right)\right)\leftrightarrow \left(\mathrm{Fun}\left(x{-}_{f}e\right)\wedge \left(x{-}_{f}e\right)\mathrm{supp}0\in \mathrm{Fin}\right)\right)$$
164	151 160 163	mpbir2and	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to {finSupp}_0\left(\left(x{-}_{f}e\right)\right)$$
165	93 96 100 106 107 109 133 150 164	gsumadd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(e{+}_f\left(x{-}_{f}e\right)\right)=\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},e\right)+\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},\left(x{-}_{f}e\right)\right)$$
166	109	ffvelcdmda	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge b\in I\right)\to e\left(b\right)\in {\mathbb{N}}_0$$
167	166	nn0cnd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge b\in I\right)\to e\left(b\right)\in ℂ$$
168	112	ffvelcdmda	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge b\in I\right)\to x\left(b\right)\in {\mathbb{N}}_0$$
169	168	nn0cnd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge b\in I\right)\to x\left(b\right)\in ℂ$$
170	167 169	pncan3d	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge b\in I\right)\to e\left(b\right)+x\left(b\right)-e\left(b\right)=x\left(b\right)$$
171	170	mpteq2dva	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left(b\in I⟼e\left(b\right)+x\left(b\right)-e\left(b\right)\right)=\left(b\in I⟼x\left(b\right)\right)$$
172		fvexd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge b\in I\right)\to e\left(b\right)\in \mathrm{V}$$
173		ovexd	$$⊢\left(\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\wedge b\in I\right)\to x\left(b\right)-e\left(b\right)\in \mathrm{V}$$
174	109	feqmptd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to e=\left(b\in I⟼e\left(b\right)\right)$$
175	112	feqmptd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to x=\left(b\in I⟼x\left(b\right)\right)$$
176	107 168 166 175 174	offval2	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to x{-}_{f}e=\left(b\in I⟼x\left(b\right)-e\left(b\right)\right)$$
177	107 172 173 174 176	offval2	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to e{+}_f\left(x{-}_{f}e\right)=\left(b\in I⟼e\left(b\right)+x\left(b\right)-e\left(b\right)\right)$$
178	171 177 175	3eqtr4d	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to e{+}_f\left(x{-}_{f}e\right)=x$$
179	178	oveq2d	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(e{+}_f\left(x{-}_{f}e\right)\right)={\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x$$
180	165 179	eqtr3d	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},e\right)+\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},\left(x{-}_{f}e\right)\right)={\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x$$
181		simplr	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N$$
182	180 181	eqnetrd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},e\right)+\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},\left(x{-}_{f}e\right)\right)\ne M+N$$
183		oveq12	$$⊢\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e=M\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)=N\right)\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},e\right)+\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},\left(x{-}_{f}e\right)\right)=M+N$$
184	183	a1i	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left(\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e=M\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)=N\right)\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},e\right)+\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},\left(x{-}_{f}e\right)\right)=M+N\right)$$
185	184	necon3ad	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left(\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},e\right)+\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0},\left(x{-}_{f}e\right)\right)\ne M+N\to \neg \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e=M\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)=N\right)\right)$$
186	182 185	mpd	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \neg \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e=M\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)=N\right)$$
187		neorian	$$⊢\left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\vee {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)\leftrightarrow \neg \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e=M\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)=N\right)$$
188	186 187	sylibr	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e\ne M\vee {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}\left(x{-}_{f}e\right)\ne N\right)$$
189	63 89 188	mpjaodan	$$⊢\left(\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\wedge e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\right)\to P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)=0_R$$
190	189	mpteq2dva	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\to \left(e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}⟼P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)=\left(e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}⟼0_R\right)$$
191	190	oveq2d	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\to \underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)=\underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}{0}_R$$
192		ringmnd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$
193	4 192	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
194	193	ad2antrr	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\to R\in \mathrm{Mnd}$$
195	45	rabex	$$⊢\left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\in \mathrm{V}$$
196	42	gsumz	$$⊢\left(R\in \mathrm{Mnd}\wedge \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}\in \mathrm{V}\right)\to \underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}{0}_R=0_R$$
197	194 195 196	sylancl	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\to \underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}{0}_R=0_R$$
198	191 197	eqtrd	$$⊢\left(\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\right)\to \underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)=0_R$$
199	198	ex	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x\ne M+N\to \underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)=0_R\right)$$
200	199	necon1d	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(\underset{e\in \left\{c\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|c{\le }_{f}x\right\}}{{\sum }_R}\left(P\left(e\right){\cdot }_{R}Q\left(x{-}_{f}e\right)\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x=M+N\right)$$
201	28 200	sylbid	$$⊢\left(\phi \wedge x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(\left(P\underset{\dot{}}{·}Q\right)\left(x\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x=M+N\right)$$
202	201	ralrimiva	$$⊢\phi \to \forall x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(\left(P\underset{\dot{}}{·}Q\right)\left(x\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x=M+N\right)$$
203	5 6	nn0addcld	$$⊢\phi \to M+N\in {\mathbb{N}}_0$$
204	2	mplring	$$⊢\left(I\in \mathrm{V}\wedge R\in \mathrm{Ring}\right)\to Y\in \mathrm{Ring}$$
205	13 4 204	syl2anc	$$⊢\phi \to Y\in \mathrm{Ring}$$
206	9 3	ringcl	$$⊢\left(Y\in \mathrm{Ring}\wedge P\in {\mathrm{Base}}_Y\wedge Q\in {\mathrm{Base}}_Y\right)\to P\underset{\dot{}}{·}Q\in {\mathrm{Base}}_Y$$
207	205 14 15 206	syl3anc	$$⊢\phi \to P\underset{\dot{}}{·}Q\in {\mathrm{Base}}_Y$$
208	1 2 9 42 11 13 4 203 207	ismhp3	$$⊢\phi \to \left(P\underset{\dot{}}{·}Q\in H\left(M+N\right)\leftrightarrow \forall x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(\left(P\underset{\dot{}}{·}Q\right)\left(x\right)\ne 0_R\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}x=M+N\right)\right)$$
209	202 208	mpbird	$$⊢\phi \to P\underset{\dot{}}{·}Q\in H\left(M+N\right)$$