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)

	Ref	Expression
Hypotheses	mhpmulcl.h	$$⊢H=I\mathrm{mHomP}R$$
	mhpmulcl.y	$$⊢Y=I\mathrm{mPoly}R$$
	mhpmulcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	mhpmulcl.i	$$⊢\phi \to I\in V$$
	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.i	$$⊢\phi \to I\in V$$
5		mhpmulcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		mhpmulcl.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
7		mhpmulcl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
8		mhpmulcl.p	$$⊢\phi \to P\in H\left(M\right)$$
9		mhpmulcl.q	$$⊢\phi \to Q\in H\left(N\right)$$
10		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
11		eqid	$$⊢{\cdot }_R={\cdot }_R$$
12		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\}$$
13	1 2 10 4 5 6 8	mhpmpl	$$⊢\phi \to P\in {\mathrm{Base}}_Y$$
14	1 2 10 4 5 7 9	mhpmpl	$$⊢\phi \to Q\in {\mathrm{Base}}_Y$$
15	2 10 11 3 12 13 14	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)$$
16	15	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)$$
17		breq2	$$⊢d=x\to \left(c{\le }_{f}d\leftrightarrow c{\le }_{f}x\right)$$
18	17	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\}$$
19		fvoveq1	$$⊢d=x\to Q\left(d{-}_{f}e\right)=Q\left(x{-}_{f}e\right)$$
20	19	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)$$
21	18 20	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)$$
22	21	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)$$
23	22	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)$$
24		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\}$$
25		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}$$
26	16 23 24 25	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)$$
27	26	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)$$
28		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$$
29		oveq2	$$⊢c=e\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}c={\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}e$$
30	29	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)$$
31	30	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)$$
32		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\}$$
33		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\}$$
34	32 33	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\}$$
35		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$$
36	31 34 35	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\}$$
37		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\}$$
38	36 37	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)$$
39		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
40	2 39 10 12 13	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$$
41		eqid	$$⊢0_R=0_R$$
42	1 41 12 4 5 6 8	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\}$$
43		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
44	43	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
45	44	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}$$
46		fvexd	$$⊢\phi \to 0_R\in \mathrm{V}$$
47	40 42 45 46	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$$
48	28 38 47	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$$
49	48	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)$$
50	5	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}$$
51	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}e\ne M\right)\to Q\in {\mathrm{Base}}_Y$$
52	2 39 10 12 51	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$$
53		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\}$$
54		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\}$$
55	12 54	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\}$$
56	53 32 55	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\}$$
57		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\}$$
58	56 57	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\}$$
59	52 58	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$$
60	39 11 41	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$$
61	50 59 60	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$$
62	49 61	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$$
63		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$$
64		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)$$
65	64	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)$$
66	65	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)$$
67		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\}$$
68		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\}$$
69	67 68 55	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\}$$
70	69 57	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\}$$
71		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$$
72	66 70 71	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\}$$
73		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\}$$
74	72 73	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)$$
75	2 39 10 12 14	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$$
76	1 41 12 4 5 7 9	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\}$$
77	75 76 45 46	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$$
78	63 74 77	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$$
79	78	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$$
80	5	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}$$
81	13	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$$
82	2 39 10 12 81	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$$
83	33	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\}$$
84	83	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\}$$
85	82 84	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$$
86	39 11 41	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$$
87	80 85 86	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$$
88	79 87	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$$
89		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
90		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
91	90	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)}$$
92	89 91	ax-mp	$$⊢{\mathbb{N}}_0={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
93		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
94	90 93	subm0	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to 0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
95	89 94	ax-mp	$$⊢0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
96		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
97		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
98	90 97	ressplusg	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to +={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
99	96 98	ax-mp	$$⊢+={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
100		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
101		ringcmn	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
102	100 101	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
103	90	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}$$
104	102 89 103	mp2an	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{CMnd}$$
105	104	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}$$
106	4	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 V$$
107	12	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$$
108	83 107	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$$
109		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\}$$
110	12	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$$
111	109 110	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$$
112	111	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$$
113	108	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$$
114		inidm	$$⊢I\cap I=I$$
115		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)$$
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 e\left(i\right)=e\left(i\right)$$
117	112 113 106 106 114 115 116	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)$$
118		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)$$
119		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\}$$
120		breq1	$$⊢c=e\to \left(c{\le }_{f}x\leftrightarrow e{\le }_{f}x\right)$$
121	120	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)$$
122	121	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$$
123	119 122	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$$
124		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$$
125	113 112 106 106 114 116 115	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)$$
126	118 123 124 125	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)$$
127	108	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$$
128	111	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$$
129		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)$$
130	127 128 129	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)$$
131	126 130	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$$
132	117 131	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$$
133	108	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$$
134		c0ex	$$⊢0\in \mathrm{V}$$
135	106 134	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 V\wedge 0\in \mathrm{V}\right)$$
136		fsuppeq	$$⊢\left(I\in 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)$$
137	135 108 136	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]$$
138		dfn2	$$⊢\mathbb{N}={\mathbb{N}}_0\setminus \left\{0\right\}$$
139	138	imaeq2i	$$⊢e^{-1}\left[\mathbb{N}\right]=e^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]$$
140	137 139	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]$$
141	12	psrbag	$$⊢I\in 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)$$
142	106 141	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)$$
143	83 142	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)$$
144	143	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}$$
145	140 144	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}$$
146	83	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}$$
147		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)$$
148	146 134 147	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)$$
149	133 145 148	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)$$
150	112 113 106 106	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)$$
151	12	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)$$
152	109 151	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)$$
153	152 149	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}$$
154		0nn0	$$⊢0\in {\mathbb{N}}_0$$
155	154	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$$
156		0m0e0	$$⊢0-0=0$$
157	156	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$$
158	106 155 111 108 157	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)$$
159	153 158	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}$$
160		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}$$
161		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)$$
162	160 134 161	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)$$
163	150 159 162	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)$$
164	92 95 99 105 106 108 132 149 163	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)$$
165	108	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$$
166	165	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 ℂ$$
167	111	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$$
168	167	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 ℂ$$
169	166 168	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)$$
170	169	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)$$
171		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}$$
172		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}$$
173	108	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)$$
174	111	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)$$
175	106 167 165 174 173	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)$$
176	106 171 172 173 175	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)$$
177	170 176 174	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$$
178	177	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$$
179	164 178	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$$
180		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$$
181	179 180	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$$
182		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$$
183	182	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)$$
184	183	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)$$
185	181 184	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)$$
186		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)$$
187	185 186	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)$$
188	62 88 187	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$$
189	188	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)$$
190	189	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$$
191		ringmnd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$
192	5 191	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
193	192	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}$$
194	44	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}$$
195	41	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$$
196	193 194 195	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$$
197	190 196	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$$
198	197	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)$$
199	198	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)$$
200	27 199	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)$$
201	200	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)$$
202	6 7	nn0addcld	$$⊢\phi \to M+N\in {\mathbb{N}}_0$$
203	2	mplring	$$⊢\left(I\in V\wedge R\in \mathrm{Ring}\right)\to Y\in \mathrm{Ring}$$
204	4 5 203	syl2anc	$$⊢\phi \to Y\in \mathrm{Ring}$$
205	10 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$$
206	204 13 14 205	syl3anc	$$⊢\phi \to P\underset{\dot{}}{·}Q\in {\mathrm{Base}}_Y$$
207	1 2 10 41 12 4 5 202 206	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)$$
208	201 207	mpbird	$$⊢\phi \to P\underset{\dot{}}{·}Q\in H\left(M+N\right)$$