Theorem mplcoe5

Description: Decompose a monomial into a finite product of powers of variables. Instead of assuming that R is a commutative ring (as in mplcoe2 ), it is sufficient that R is a ring and all the variables of the multivariate polynomial commute. (Contributed by AV, 7-Oct-2019)

	Ref	Expression
Hypotheses	mplcoe1.p	$$⊢P=I\mathrm{mPoly}R$$
	mplcoe1.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplcoe1.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mplcoe1.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mplcoe1.i	$$⊢\phi \to I\in W$$
	mplcoe2.g	$$⊢G={\mathrm{mulGrp}}_P$$
	mplcoe2.m	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	mplcoe2.v	$$⊢V=I\mathrm{mVar}R$$
	mplcoe5.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mplcoe5.y	$$⊢\phi \to Y\in D$$
	mplcoe5.c	$$⊢\phi \to \forall x\in I\forall y\in IV\left(y\right){+}_{G}V\left(x\right)=V\left(x\right){+}_{G}V\left(y\right)$$
Assertion	mplcoe5	$$⊢\phi \to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in I}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplcoe1.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplcoe1.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mplcoe1.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mplcoe1.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		mplcoe1.i	$$⊢\phi \to I\in W$$
6		mplcoe2.g	$$⊢G={\mathrm{mulGrp}}_P$$
7		mplcoe2.m	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
8		mplcoe2.v	$$⊢V=I\mathrm{mVar}R$$
9		mplcoe5.r	$$⊢\phi \to R\in \mathrm{Ring}$$
10		mplcoe5.y	$$⊢\phi \to Y\in D$$
11		mplcoe5.c	$$⊢\phi \to \forall x\in I\forall y\in IV\left(y\right){+}_{G}V\left(x\right)=V\left(x\right){+}_{G}V\left(y\right)$$
12	2	psrbag	$$⊢I\in W\to \left(Y\in D\leftrightarrow \left(Y:I⟶{\mathbb{N}}_0\wedge Y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
13	5 12	syl	$$⊢\phi \to \left(Y\in D\leftrightarrow \left(Y:I⟶{\mathbb{N}}_0\wedge Y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
14	10 13	mpbid	$$⊢\phi \to \left(Y:I⟶{\mathbb{N}}_0\wedge Y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
15	14	simpld	$$⊢\phi \to Y:I⟶{\mathbb{N}}_0$$
16	15	feqmptd	$$⊢\phi \to Y=\left(i\in I⟼Y\left(i\right)\right)$$
17		iftrue	$$⊢i\in Y^{-1}\left[\mathbb{N}\right]\to if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)=Y\left(i\right)$$
18	17	adantl	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge i\in Y^{-1}\left[\mathbb{N}\right]\right)\to if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)=Y\left(i\right)$$
19		eldif	$$⊢i\in \left(I\setminus Y^{-1}\left[\mathbb{N}\right]\right)\leftrightarrow \left(i\in I\wedge \neg i\in Y^{-1}\left[\mathbb{N}\right]\right)$$
20		ifid	$$⊢if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),Y\left(i\right)\right)=Y\left(i\right)$$
21		frnnn0supp	$$⊢\left(I\in W\wedge Y:I⟶{\mathbb{N}}_0\right)\to Y\mathrm{supp}0=Y^{-1}\left[\mathbb{N}\right]$$
22	5 15 21	syl2anc	$$⊢\phi \to Y\mathrm{supp}0=Y^{-1}\left[\mathbb{N}\right]$$
23		eqimss	$$⊢Y\mathrm{supp}0=Y^{-1}\left[\mathbb{N}\right]\to Y\mathrm{supp}0\subseteq Y^{-1}\left[\mathbb{N}\right]$$
24	22 23	syl	$$⊢\phi \to Y\mathrm{supp}0\subseteq Y^{-1}\left[\mathbb{N}\right]$$
25		c0ex	$$⊢0\in \mathrm{V}$$
26	25	a1i	$$⊢\phi \to 0\in \mathrm{V}$$
27	15 24 5 26	suppssr	$$⊢\left(\phi \wedge i\in \left(I\setminus Y^{-1}\left[\mathbb{N}\right]\right)\right)\to Y\left(i\right)=0$$
28	27	ifeq2d	$$⊢\left(\phi \wedge i\in \left(I\setminus Y^{-1}\left[\mathbb{N}\right]\right)\right)\to if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),Y\left(i\right)\right)=if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)$$
29	20 28	syl5reqr	$$⊢\left(\phi \wedge i\in \left(I\setminus Y^{-1}\left[\mathbb{N}\right]\right)\right)\to if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)=Y\left(i\right)$$
30	19 29	sylan2br	$$⊢\left(\phi \wedge \left(i\in I\wedge \neg i\in Y^{-1}\left[\mathbb{N}\right]\right)\right)\to if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)=Y\left(i\right)$$
31	30	anassrs	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge \neg i\in Y^{-1}\left[\mathbb{N}\right]\right)\to if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)=Y\left(i\right)$$
32	18 31	pm2.61dan	$$⊢\left(\phi \wedge i\in I\right)\to if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)=Y\left(i\right)$$
33	32	mpteq2dva	$$⊢\phi \to \left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right)=\left(i\in I⟼Y\left(i\right)\right)$$
34	16 33	eqtr4d	$$⊢\phi \to Y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right)$$
35	34	eqeq2d	$$⊢\phi \to \left(y=Y\leftrightarrow y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right)\right)$$
36	35	ifbid	$$⊢\phi \to if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
37	36	mpteq2dv	$$⊢\phi \to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
38		cnvimass	$$⊢Y^{-1}\left[\mathbb{N}\right]\subseteq \mathrm{dom}Y$$
39	38 15	fssdm	$$⊢\phi \to Y^{-1}\left[\mathbb{N}\right]\subseteq I$$
40	14	simprd	$$⊢\phi \to Y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
41		sseq1	$$⊢w=\varnothing \to \left(w\subseteq I\leftrightarrow \varnothing \subseteq I\right)$$
42		noel	$$⊢\neg i\in \varnothing$$
43		eleq2	$$⊢w=\varnothing \to \left(i\in w\leftrightarrow i\in \varnothing \right)$$
44	42 43	mtbiri	$$⊢w=\varnothing \to \neg i\in w$$
45	44	iffalsed	$$⊢w=\varnothing \to if\left(i\in w,Y\left(i\right),0\right)=0$$
46	45	mpteq2dv	$$⊢w=\varnothing \to \left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right)=\left(i\in I⟼0\right)$$
47		fconstmpt	$$⊢I\times \left\{0\right\}=\left(i\in I⟼0\right)$$
48	46 47	syl6eqr	$$⊢w=\varnothing \to \left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right)=I\times \left\{0\right\}$$
49	48	eqeq2d	$$⊢w=\varnothing \to \left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right)\leftrightarrow y=I\times \left\{0\right\}\right)$$
50	49	ifbid	$$⊢w=\varnothing \to if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
51	50	mpteq2dv	$$⊢w=\varnothing \to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
52		mpteq1	$$⊢w=\varnothing \to \left(k\in w⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\left(k\in \varnothing ⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
53		mpt0	$$⊢\left(k\in \varnothing ⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\varnothing$$
54	52 53	syl6eq	$$⊢w=\varnothing \to \left(k\in w⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\varnothing$$
55	54	oveq2d	$$⊢w=\varnothing \to \underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)={\sum }_G\varnothing$$
56		eqid	$$⊢1_P=1_P$$
57	6 56	ringidval	$$⊢1_P=0_G$$
58	57	gsum0	$$⊢{\sum }_G\varnothing =1_P$$
59	55 58	syl6eq	$$⊢w=\varnothing \to \underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=1_P$$
60	51 59	eqeq12d	$$⊢w=\varnothing \to \left(\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\leftrightarrow \left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=1_P\right)$$
61	41 60	imbi12d	$$⊢w=\varnothing \to \left(\left(w\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\leftrightarrow \left(\varnothing \subseteq I\to \left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=1_P\right)\right)$$
62	61	imbi2d	$$⊢w=\varnothing \to \left(\left(\phi \to \left(w\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(\varnothing \subseteq I\to \left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=1_P\right)\right)\right)$$
63		sseq1	$$⊢w=x\to \left(w\subseteq I\leftrightarrow x\subseteq I\right)$$
64		eleq2	$$⊢w=x\to \left(i\in w\leftrightarrow i\in x\right)$$
65	64	ifbid	$$⊢w=x\to if\left(i\in w,Y\left(i\right),0\right)=if\left(i\in x,Y\left(i\right),0\right)$$
66	65	mpteq2dv	$$⊢w=x\to \left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right)=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)$$
67	66	eqeq2d	$$⊢w=x\to \left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right)\leftrightarrow y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)\right)$$
68	67	ifbid	$$⊢w=x\to if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
69	68	mpteq2dv	$$⊢w=x\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
70		mpteq1	$$⊢w=x\to \left(k\in w⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\left(k\in x⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
71	70	oveq2d	$$⊢w=x\to \underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
72	69 71	eqeq12d	$$⊢w=x\to \left(\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\leftrightarrow \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)$$
73	63 72	imbi12d	$$⊢w=x\to \left(\left(w\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\leftrightarrow \left(x\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)$$
74	73	imbi2d	$$⊢w=x\to \left(\left(\phi \to \left(w\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(x\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)\right)$$
75		sseq1	$$⊢w=x\cup \left\{z\right\}\to \left(w\subseteq I\leftrightarrow x\cup \left\{z\right\}\subseteq I\right)$$
76		eleq2	$$⊢w=x\cup \left\{z\right\}\to \left(i\in w\leftrightarrow i\in \left(x\cup \left\{z\right\}\right)\right)$$
77	76	ifbid	$$⊢w=x\cup \left\{z\right\}\to if\left(i\in w,Y\left(i\right),0\right)=if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)$$
78	77	mpteq2dv	$$⊢w=x\cup \left\{z\right\}\to \left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right)=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right)$$
79	78	eqeq2d	$$⊢w=x\cup \left\{z\right\}\to \left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right)\leftrightarrow y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right)\right)$$
80	79	ifbid	$$⊢w=x\cup \left\{z\right\}\to if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
81	80	mpteq2dv	$$⊢w=x\cup \left\{z\right\}\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
82		mpteq1	$$⊢w=x\cup \left\{z\right\}\to \left(k\in w⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\left(k\in \left(x\cup \left\{z\right\}\right)⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
83	82	oveq2d	$$⊢w=x\cup \left\{z\right\}\to \underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
84	81 83	eqeq12d	$$⊢w=x\cup \left\{z\right\}\to \left(\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\leftrightarrow \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)$$
85	75 84	imbi12d	$$⊢w=x\cup \left\{z\right\}\to \left(\left(w\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\leftrightarrow \left(x\cup \left\{z\right\}\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)$$
86	85	imbi2d	$$⊢w=x\cup \left\{z\right\}\to \left(\left(\phi \to \left(w\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(x\cup \left\{z\right\}\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)\right)$$
87		sseq1	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to \left(w\subseteq I\leftrightarrow Y^{-1}\left[\mathbb{N}\right]\subseteq I\right)$$
88		eleq2	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to \left(i\in w\leftrightarrow i\in Y^{-1}\left[\mathbb{N}\right]\right)$$
89	88	ifbid	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to if\left(i\in w,Y\left(i\right),0\right)=if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)$$
90	89	mpteq2dv	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to \left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right)=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right)$$
91	90	eqeq2d	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to \left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right)\leftrightarrow y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right)\right)$$
92	91	ifbid	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
93	92	mpteq2dv	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
94		mpteq1	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to \left(k\in w⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\left(k\in Y^{-1}\left[\mathbb{N}\right]⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
95	94	oveq2d	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to \underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\underset{k\in Y^{-1}\left[\mathbb{N}\right]}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
96	93 95	eqeq12d	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to \left(\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\leftrightarrow \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in Y^{-1}\left[\mathbb{N}\right]}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)$$
97	87 96	imbi12d	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to \left(\left(w\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\leftrightarrow \left(Y^{-1}\left[\mathbb{N}\right]\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in Y^{-1}\left[\mathbb{N}\right]}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)$$
98	97	imbi2d	$$⊢w=Y^{-1}\left[\mathbb{N}\right]\to \left(\left(\phi \to \left(w\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in w,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in w}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(Y^{-1}\left[\mathbb{N}\right]\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in Y^{-1}\left[\mathbb{N}\right]}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)\right)$$
99	1 2 3 4 56 5 9	mpl1	$$⊢\phi \to 1_P=\left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
100	99	eqcomd	$$⊢\phi \to \left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=1_P$$
101	100	a1d	$$⊢\phi \to \left(\varnothing \subseteq I\to \left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=1_P\right)$$
102		ssun1	$$⊢x\subseteq x\cup \left\{z\right\}$$
103		sstr2	$$⊢x\subseteq x\cup \left\{z\right\}\to \left(x\cup \left\{z\right\}\subseteq I\to x\subseteq I\right)$$
104	102 103	ax-mp	$$⊢x\cup \left\{z\right\}\subseteq I\to x\subseteq I$$
105	104	imim1i	$$⊢\left(x\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\to \left(x\cup \left\{z\right\}\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)$$
106		oveq1	$$⊢\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_P\left(Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)\right)=\left(\underset{k\in x}{{\sum }_G},\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right){\cdot }_P\left(Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)\right)$$
107		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
108	5	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to I\in W$$
109	9	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to R\in \mathrm{Ring}$$
110	15	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to Y:I⟶{\mathbb{N}}_0$$
111	110	ffvelrnda	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\to Y\left(i\right)\in {\mathbb{N}}_0$$
112		0nn0	$$⊢0\in {\mathbb{N}}_0$$
113		ifcl	$$⊢\left(Y\left(i\right)\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\right)\to if\left(i\in x,Y\left(i\right),0\right)\in {\mathbb{N}}_0$$
114	111 112 113	sylancl	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\to if\left(i\in x,Y\left(i\right),0\right)\in {\mathbb{N}}_0$$
115	114	fmpttd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right):I⟶{\mathbb{N}}_0$$
116		frnnn0supp	$$⊢\left(I\in W\wedge \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right):I⟶{\mathbb{N}}_0\right)\to \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)\mathrm{supp}0={\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)}^{-1}\left[\mathbb{N}\right]$$
117	108 115 116	syl2anc	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)\mathrm{supp}0={\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)}^{-1}\left[\mathbb{N}\right]$$
118		simprll	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to x\in \mathrm{Fin}$$
119		eldifn	$$⊢i\in \left(I\setminus x\right)\to \neg i\in x$$
120	119	adantl	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in \left(I\setminus x\right)\right)\to \neg i\in x$$
121	120	iffalsed	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in \left(I\setminus x\right)\right)\to if\left(i\in x,Y\left(i\right),0\right)=0$$
122	121 108	suppss2	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)\mathrm{supp}0\subseteq x$$
123	118 122	ssfid	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)\mathrm{supp}0\in \mathrm{Fin}$$
124	117 123	eqeltrrd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to {\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
125	2	psrbag	$$⊢I\in W\to \left(\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)\in D\leftrightarrow \left(\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right):I⟶{\mathbb{N}}_0\wedge {\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
126	108 125	syl	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)\in D\leftrightarrow \left(\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right):I⟶{\mathbb{N}}_0\wedge {\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\right)$$
127	115 124 126	mpbir2and	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)\in D$$
128		eqid	$$⊢{\cdot }_P={\cdot }_P$$
129		ssun2	$$⊢\left\{z\right\}\subseteq x\cup \left\{z\right\}$$
130		simprr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to x\cup \left\{z\right\}\subseteq I$$
131	129 130	sstrid	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left\{z\right\}\subseteq I$$
132		vex	$$⊢z\in \mathrm{V}$$
133	132	snss	$$⊢z\in I\leftrightarrow \left\{z\right\}\subseteq I$$
134	131 133	sylibr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to z\in I$$
135	110 134	ffvelrnd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to Y\left(z\right)\in {\mathbb{N}}_0$$
136	2	snifpsrbag	$$⊢\left(I\in W\wedge Y\left(z\right)\in {\mathbb{N}}_0\right)\to \left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right)\in D$$
137	108 135 136	syl2anc	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right)\in D$$
138	1 107 3 4 2 108 109 127 128 137	mplmonmul	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_P\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right){+}_f\left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
139	1 2 3 4 108 6 7 8 109 134 135	mplcoe3	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)$$
140	139	oveq2d	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_P\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_P\left(Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)\right)$$
141	135	adantr	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\to Y\left(z\right)\in {\mathbb{N}}_0$$
142		ifcl	$$⊢\left(Y\left(z\right)\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\right)\to if\left(i=z,Y\left(z\right),0\right)\in {\mathbb{N}}_0$$
143	141 112 142	sylancl	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\to if\left(i=z,Y\left(z\right),0\right)\in {\mathbb{N}}_0$$
144		eqidd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right)$$
145		eqidd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right)=\left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right)$$
146	108 114 143 144 145	offval2	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right){+}_f\left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right)=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)+if\left(i=z,Y\left(z\right),0\right)\right)$$
147	111	adantr	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to Y\left(i\right)\in {\mathbb{N}}_0$$
148	147	nn0cnd	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to Y\left(i\right)\in ℂ$$
149	148	addid2d	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to 0+Y\left(i\right)=Y\left(i\right)$$
150		elsni	$$⊢i\in \left\{z\right\}\to i=z$$
151	150	adantl	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to i=z$$
152		simprlr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \neg z\in x$$
153	152	ad2antrr	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to \neg z\in x$$
154	151 153	eqneltrd	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to \neg i\in x$$
155	154	iffalsed	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to if\left(i\in x,Y\left(i\right),0\right)=0$$
156	151	iftrued	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to if\left(i=z,Y\left(z\right),0\right)=Y\left(z\right)$$
157	151	fveq2d	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to Y\left(i\right)=Y\left(z\right)$$
158	156 157	eqtr4d	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to if\left(i=z,Y\left(z\right),0\right)=Y\left(i\right)$$
159	155 158	oveq12d	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to if\left(i\in x,Y\left(i\right),0\right)+if\left(i=z,Y\left(z\right),0\right)=0+Y\left(i\right)$$
160		simpr	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to i\in \left\{z\right\}$$
161	129 160	sseldi	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to i\in \left(x\cup \left\{z\right\}\right)$$
162	161	iftrued	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)=Y\left(i\right)$$
163	149 159 162	3eqtr4d	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge i\in \left\{z\right\}\right)\to if\left(i\in x,Y\left(i\right),0\right)+if\left(i=z,Y\left(z\right),0\right)=if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)$$
164	114	adantr	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge \neg i\in \left\{z\right\}\right)\to if\left(i\in x,Y\left(i\right),0\right)\in {\mathbb{N}}_0$$
165	164	nn0cnd	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge \neg i\in \left\{z\right\}\right)\to if\left(i\in x,Y\left(i\right),0\right)\in ℂ$$
166	165	addid1d	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge \neg i\in \left\{z\right\}\right)\to if\left(i\in x,Y\left(i\right),0\right)+0=if\left(i\in x,Y\left(i\right),0\right)$$
167		simpr	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge \neg i\in \left\{z\right\}\right)\to \neg i\in \left\{z\right\}$$
168		velsn	$$⊢i\in \left\{z\right\}\leftrightarrow i=z$$
169	167 168	sylnib	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge \neg i\in \left\{z\right\}\right)\to \neg i=z$$
170	169	iffalsed	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge \neg i\in \left\{z\right\}\right)\to if\left(i=z,Y\left(z\right),0\right)=0$$
171	170	oveq2d	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge \neg i\in \left\{z\right\}\right)\to if\left(i\in x,Y\left(i\right),0\right)+if\left(i=z,Y\left(z\right),0\right)=if\left(i\in x,Y\left(i\right),0\right)+0$$
172		biorf	$$⊢\neg i\in \left\{z\right\}\to \left(i\in x\leftrightarrow \left(i\in \left\{z\right\}\vee i\in x\right)\right)$$
173		elun	$$⊢i\in \left(x\cup \left\{z\right\}\right)\leftrightarrow \left(i\in x\vee i\in \left\{z\right\}\right)$$
174		orcom	$$⊢\left(i\in x\vee i\in \left\{z\right\}\right)\leftrightarrow \left(i\in \left\{z\right\}\vee i\in x\right)$$
175	173 174	bitri	$$⊢i\in \left(x\cup \left\{z\right\}\right)\leftrightarrow \left(i\in \left\{z\right\}\vee i\in x\right)$$
176	172 175	syl6rbbr	$$⊢\neg i\in \left\{z\right\}\to \left(i\in \left(x\cup \left\{z\right\}\right)\leftrightarrow i\in x\right)$$
177	176	adantl	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge \neg i\in \left\{z\right\}\right)\to \left(i\in \left(x\cup \left\{z\right\}\right)\leftrightarrow i\in x\right)$$
178	177	ifbid	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge \neg i\in \left\{z\right\}\right)\to if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)=if\left(i\in x,Y\left(i\right),0\right)$$
179	166 171 178	3eqtr4d	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\wedge \neg i\in \left\{z\right\}\right)\to if\left(i\in x,Y\left(i\right),0\right)+if\left(i=z,Y\left(z\right),0\right)=if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)$$
180	163 179	pm2.61dan	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge i\in I\right)\to if\left(i\in x,Y\left(i\right),0\right)+if\left(i=z,Y\left(z\right),0\right)=if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)$$
181	180	mpteq2dva	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)+if\left(i=z,Y\left(z\right),0\right)\right)=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right)$$
182	146 181	eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right){+}_f\left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right)=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right)$$
183	182	eqeq2d	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right){+}_f\left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right)\leftrightarrow y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right)\right)$$
184	183	ifbid	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right){+}_f\left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
185	184	mpteq2dv	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right){+}_f\left(i\in I⟼if\left(i=z,Y\left(z\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
186	138 140 185	3eqtr3rd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_P\left(Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)\right)$$
187	6 107	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_G$$
188	6 128	mgpplusg	$$⊢{\cdot }_P={+}_G$$
189		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
190		eqid	$$⊢\left(k\in \left(x\cup \left\{z\right\}\right)⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\left(k\in \left(x\cup \left\{z\right\}\right)⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
191	1	mplring	$$⊢\left(I\in W\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{Ring}$$
192	5 9 191	syl2anc	$$⊢\phi \to P\in \mathrm{Ring}$$
193	6	ringmgp	$$⊢P\in \mathrm{Ring}\to G\in \mathrm{Mnd}$$
194	192 193	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
195	194	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to G\in \mathrm{Mnd}$$
196	10	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to Y\in D$$
197		fveq2	$$⊢x=a\to V\left(x\right)=V\left(a\right)$$
198	197	oveq2d	$$⊢x=a\to V\left(y\right){+}_{G}V\left(x\right)=V\left(y\right){+}_{G}V\left(a\right)$$
199	197	oveq1d	$$⊢x=a\to V\left(x\right){+}_{G}V\left(y\right)=V\left(a\right){+}_{G}V\left(y\right)$$
200	198 199	eqeq12d	$$⊢x=a\to \left(V\left(y\right){+}_{G}V\left(x\right)=V\left(x\right){+}_{G}V\left(y\right)\leftrightarrow V\left(y\right){+}_{G}V\left(a\right)=V\left(a\right){+}_{G}V\left(y\right)\right)$$
201		fveq2	$$⊢y=b\to V\left(y\right)=V\left(b\right)$$
202	201	oveq1d	$$⊢y=b\to V\left(y\right){+}_{G}V\left(a\right)=V\left(b\right){+}_{G}V\left(a\right)$$
203	201	oveq2d	$$⊢y=b\to V\left(a\right){+}_{G}V\left(y\right)=V\left(a\right){+}_{G}V\left(b\right)$$
204	202 203	eqeq12d	$$⊢y=b\to \left(V\left(y\right){+}_{G}V\left(a\right)=V\left(a\right){+}_{G}V\left(y\right)\leftrightarrow V\left(b\right){+}_{G}V\left(a\right)=V\left(a\right){+}_{G}V\left(b\right)\right)$$
205	200 204	cbvral2vw	$$⊢\forall x\in I\forall y\in IV\left(y\right){+}_{G}V\left(x\right)=V\left(x\right){+}_{G}V\left(y\right)\leftrightarrow \forall a\in I\forall b\in IV\left(b\right){+}_{G}V\left(a\right)=V\left(a\right){+}_{G}V\left(b\right)$$
206	11 205	sylib	$$⊢\phi \to \forall a\in I\forall b\in IV\left(b\right){+}_{G}V\left(a\right)=V\left(a\right){+}_{G}V\left(b\right)$$
207	206	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \forall a\in I\forall b\in IV\left(b\right){+}_{G}V\left(a\right)=V\left(a\right){+}_{G}V\left(b\right)$$
208	1 2 3 4 108 6 7 8 109 196 207 130	mplcoe5lem	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \mathrm{ran}\left(k\in \left(x\cup \left\{z\right\}\right)⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\subseteq \mathrm{Cntz}\left(G\right)\left(\mathrm{ran}\left(k\in \left(x\cup \left\{z\right\}\right)⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)$$
209	102 130	sstrid	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to x\subseteq I$$
210	209	sselda	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge k\in x\right)\to k\in I$$
211	194	adantr	$$⊢\left(\phi \wedge k\in I\right)\to G\in \mathrm{Mnd}$$
212	15	ffvelrnda	$$⊢\left(\phi \wedge k\in I\right)\to Y\left(k\right)\in {\mathbb{N}}_0$$
213	5	adantr	$$⊢\left(\phi \wedge k\in I\right)\to I\in W$$
214	9	adantr	$$⊢\left(\phi \wedge k\in I\right)\to R\in \mathrm{Ring}$$
215		simpr	$$⊢\left(\phi \wedge k\in I\right)\to k\in I$$
216	1 8 107 213 214 215	mvrcl	$$⊢\left(\phi \wedge k\in I\right)\to V\left(k\right)\in {\mathrm{Base}}_P$$
217	187 7	mulgnn0cl	$$⊢\left(G\in \mathrm{Mnd}\wedge Y\left(k\right)\in {\mathbb{N}}_0\wedge V\left(k\right)\in {\mathrm{Base}}_P\right)\to Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\in {\mathrm{Base}}_P$$
218	211 212 216 217	syl3anc	$$⊢\left(\phi \wedge k\in I\right)\to Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\in {\mathrm{Base}}_P$$
219	218	adantlr	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge k\in I\right)\to Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\in {\mathrm{Base}}_P$$
220	210 219	syldan	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge k\in x\right)\to Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\in {\mathrm{Base}}_P$$
221	1 8 107 108 109 134	mvrcl	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to V\left(z\right)\in {\mathrm{Base}}_P$$
222	187 7	mulgnn0cl	$$⊢\left(G\in \mathrm{Mnd}\wedge Y\left(z\right)\in {\mathbb{N}}_0\wedge V\left(z\right)\in {\mathrm{Base}}_P\right)\to Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)\in {\mathrm{Base}}_P$$
223	195 135 221 222	syl3anc	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)\in {\mathrm{Base}}_P$$
224		fveq2	$$⊢k=z\to Y\left(k\right)=Y\left(z\right)$$
225		fveq2	$$⊢k=z\to V\left(k\right)=V\left(z\right)$$
226	224 225	oveq12d	$$⊢k=z\to Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)=Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)$$
227	226	adantl	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\wedge k=z\right)\to Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)=Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)$$
228	187 188 189 190 195 118 208 220 134 152 223 227	gsumzunsnd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)=\left(\underset{k\in x}{{\sum }_G},\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right){\cdot }_P\left(Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)\right)$$
229	186 228	eqeq12d	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\leftrightarrow \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_P\left(Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)\right)=\left(\underset{k\in x}{{\sum }_G},\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right){\cdot }_P\left(Y\left(z\right)\underset{\dot{}}{\times }V\left(z\right)\right)\right)$$
230	106 229	syl5ibr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq I\right)\right)\to \left(\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)$$
231	230	expr	$$⊢\left(\phi \wedge \left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\right)\to \left(x\cup \left\{z\right\}\subseteq I\to \left(\left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)$$
232	231	a2d	$$⊢\left(\phi \wedge \left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\right)\to \left(\left(x\cup \left\{z\right\}\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\to \left(x\cup \left\{z\right\}\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)$$
233	105 232	syl5	$$⊢\left(\phi \wedge \left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\right)\to \left(\left(x\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\to \left(x\cup \left\{z\right\}\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)$$
234	233	expcom	$$⊢\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\to \left(\phi \to \left(\left(x\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\to \left(x\cup \left\{z\right\}\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)\right)$$
235	234	a2d	$$⊢\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\to \left(\left(\phi \to \left(x\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in x,Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)\to \left(\phi \to \left(x\cup \left\{z\right\}\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in \left(x\cup \left\{z\right\}\right),Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)\right)$$
236	62 74 86 98 101 235	findcard2s	$$⊢Y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\to \left(\phi \to \left(Y^{-1}\left[\mathbb{N}\right]\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in Y^{-1}\left[\mathbb{N}\right]}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)\right)$$
237	40 236	mpcom	$$⊢\phi \to \left(Y^{-1}\left[\mathbb{N}\right]\subseteq I\to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in Y^{-1}\left[\mathbb{N}\right]}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)$$
238	39 237	mpd	$$⊢\phi \to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in Y^{-1}\left[\mathbb{N}\right]}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
239	39	resmptd	$$⊢\phi \to {\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\upharpoonright }_{Y^{-1}\left[\mathbb{N}\right]}=\left(k\in Y^{-1}\left[\mathbb{N}\right]⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
240	239	oveq2d	$$⊢\phi \to {\sum }_G\left({\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\upharpoonright }_{Y^{-1}\left[\mathbb{N}\right]}\right)=\underset{k\in Y^{-1}\left[\mathbb{N}\right]}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
241	218	fmpttd	$$⊢\phi \to \left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right):I⟶{\mathrm{Base}}_P$$
242		ssidd	$$⊢\phi \to I\subseteq I$$
243	1 2 3 4 5 6 7 8 9 10 11 242	mplcoe5lem	$$⊢\phi \to \mathrm{ran}\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\subseteq \mathrm{Cntz}\left(G\right)\left(\mathrm{ran}\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)$$
244	15 24 5 26	suppssr	$$⊢\left(\phi \wedge k\in \left(I\setminus Y^{-1}\left[\mathbb{N}\right]\right)\right)\to Y\left(k\right)=0$$
245	244	oveq1d	$$⊢\left(\phi \wedge k\in \left(I\setminus Y^{-1}\left[\mathbb{N}\right]\right)\right)\to Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)=0\underset{\dot{}}{\times }V\left(k\right)$$
246		eldifi	$$⊢k\in \left(I\setminus Y^{-1}\left[\mathbb{N}\right]\right)\to k\in I$$
247	246 216	sylan2	$$⊢\left(\phi \wedge k\in \left(I\setminus Y^{-1}\left[\mathbb{N}\right]\right)\right)\to V\left(k\right)\in {\mathrm{Base}}_P$$
248	187 57 7	mulg0	$$⊢V\left(k\right)\in {\mathrm{Base}}_P\to 0\underset{\dot{}}{\times }V\left(k\right)=1_P$$
249	247 248	syl	$$⊢\left(\phi \wedge k\in \left(I\setminus Y^{-1}\left[\mathbb{N}\right]\right)\right)\to 0\underset{\dot{}}{\times }V\left(k\right)=1_P$$
250	245 249	eqtrd	$$⊢\left(\phi \wedge k\in \left(I\setminus Y^{-1}\left[\mathbb{N}\right]\right)\right)\to Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)=1_P$$
251	250 5	suppss2	$$⊢\phi \to \left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\mathrm{supp}{1}_P\subseteq Y^{-1}\left[\mathbb{N}\right]$$
252	5	mptexd	$$⊢\phi \to \left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\in \mathrm{V}$$
253		funmpt	$$⊢\mathrm{Fun}\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
254	253	a1i	$$⊢\phi \to \mathrm{Fun}\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
255		fvexd	$$⊢\phi \to 1_P\in \mathrm{V}$$
256		suppssfifsupp	$$⊢\left(\left(\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\wedge 1_P\in \mathrm{V}\right)\wedge \left(Y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge \left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\mathrm{supp}{1}_P\subseteq Y^{-1}\left[\mathbb{N}\right]\right)\right)\to {finSupp}_{1_P}\left(\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)$$
257	252 254 255 40 251 256	syl32anc	$$⊢\phi \to {finSupp}_{1_P}\left(\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\right)$$
258	187 57 189 194 5 241 243 251 257	gsumzres	$$⊢\phi \to {\sum }_G\left({\left(k\in I⟼Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)\upharpoonright }_{Y^{-1}\left[\mathbb{N}\right]}\right)=\underset{k\in I}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
259	238 240 258	3eqtr2d	$$⊢\phi \to \left(y\in D⟼if\left(y=\left(i\in I⟼if\left(i\in Y^{-1}\left[\mathbb{N}\right],Y\left(i\right),0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in I}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$
260	37 259	eqtrd	$$⊢\phi \to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{k\in I}{{\sum }_G}\left(Y\left(k\right)\underset{\dot{}}{\times }V\left(k\right)\right)$$