Theorem mplcoe1

Description: Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015)

	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$$
	mplcoe1.b	$$⊢B={\mathrm{Base}}_P$$
	mplcoe1.n	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	mplcoe1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mplcoe1.x	$$⊢\phi \to X\in B$$
Assertion	mplcoe1	$$⊢\phi \to X=\underset{k\in D}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\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		mplcoe1.b	$$⊢B={\mathrm{Base}}_P$$
7		mplcoe1.n	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
8		mplcoe1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
9		mplcoe1.x	$$⊢\phi \to X\in B$$
10		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
11	1 10 6 2 9	mplelf	$$⊢\phi \to X:D⟶{\mathrm{Base}}_R$$
12	11	feqmptd	$$⊢\phi \to X=\left(y\in D⟼X\left(y\right)\right)$$
13		iftrue	$$⊢y\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\to if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)=X\left(y\right)$$
14	13	adantl	$$⊢\left(\left(\phi \wedge y\in D\right)\wedge y\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\to if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)=X\left(y\right)$$
15		eldif	$$⊢y\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\leftrightarrow \left(y\in D\wedge \neg y\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)$$
16		ssidd	$$⊢\phi \to X\mathrm{supp}\underset{\dot{}}{0}\subseteq X\mathrm{supp}\underset{\dot{}}{0}$$
17		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
18	2 17	rabex2	$$⊢D\in \mathrm{V}$$
19	18	a1i	$$⊢\phi \to D\in \mathrm{V}$$
20	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
21	20	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
22	11 16 19 21	suppssr	$$⊢\left(\phi \wedge y\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)\to X\left(y\right)=\underset{\dot{}}{0}$$
23	22	ifeq2d	$$⊢\left(\phi \wedge y\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)\to if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),X\left(y\right)\right)=if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)$$
24		ifid	$$⊢if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),X\left(y\right)\right)=X\left(y\right)$$
25	23 24	eqtr3di	$$⊢\left(\phi \wedge y\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)\to if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)=X\left(y\right)$$
26	15 25	sylan2br	$$⊢\left(\phi \wedge \left(y\in D\wedge \neg y\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)\to if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)=X\left(y\right)$$
27	26	anassrs	$$⊢\left(\left(\phi \wedge y\in D\right)\wedge \neg y\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\to if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)=X\left(y\right)$$
28	14 27	pm2.61dan	$$⊢\left(\phi \wedge y\in D\right)\to if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)=X\left(y\right)$$
29	28	mpteq2dva	$$⊢\phi \to \left(y\in D⟼if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼X\left(y\right)\right)$$
30	12 29	eqtr4d	$$⊢\phi \to X=\left(y\in D⟼if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)$$
31		suppssdm	$$⊢X\mathrm{supp}\underset{\dot{}}{0}\subseteq \mathrm{dom}X$$
32	31 11	fssdm	$$⊢\phi \to X\mathrm{supp}\underset{\dot{}}{0}\subseteq D$$
33		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
34		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
35	1 33 34 3 6	mplelbas	$$⊢X\in B\leftrightarrow \left(X\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)$$
36	35	simprbi	$$⊢X\in B\to {finSupp}_{\underset{\dot{}}{0}}\left(X\right)$$
37	9 36	syl	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(X\right)$$
38	37	fsuppimpd	$$⊢\phi \to X\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
39		sseq1	$$⊢w=\varnothing \to \left(w\subseteq D\leftrightarrow \varnothing \subseteq D\right)$$
40		mpteq1	$$⊢w=\varnothing \to \left(k\in w⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(k\in \varnothing ⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
41		mpt0	$$⊢\left(k\in \varnothing ⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\varnothing$$
42	40 41	eqtrdi	$$⊢w=\varnothing \to \left(k\in w⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\varnothing$$
43	42	oveq2d	$$⊢w=\varnothing \to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)={\sum }_P\varnothing$$
44		eqid	$$⊢0_P=0_P$$
45	44	gsum0	$$⊢{\sum }_P\varnothing =0_P$$
46	43 45	eqtrdi	$$⊢w=\varnothing \to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=0_P$$
47		noel	$$⊢\neg y\in \varnothing$$
48		eleq2	$$⊢w=\varnothing \to \left(y\in w\leftrightarrow y\in \varnothing \right)$$
49	47 48	mtbiri	$$⊢w=\varnothing \to \neg y\in w$$
50	49	iffalsed	$$⊢w=\varnothing \to if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
51	50	mpteq2dv	$$⊢w=\varnothing \to \left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼\underset{\dot{}}{0}\right)$$
52	46 51	eqeq12d	$$⊢w=\varnothing \to \left(\underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\leftrightarrow 0_P=\left(y\in D⟼\underset{\dot{}}{0}\right)\right)$$
53	39 52	imbi12d	$$⊢w=\varnothing \to \left(\left(w\subseteq D\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\leftrightarrow \left(\varnothing \subseteq D\to 0_P=\left(y\in D⟼\underset{\dot{}}{0}\right)\right)\right)$$
54	53	imbi2d	$$⊢w=\varnothing \to \left(\left(\phi \to \left(w\subseteq D\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(\varnothing \subseteq D\to 0_P=\left(y\in D⟼\underset{\dot{}}{0}\right)\right)\right)\right)$$
55		sseq1	$$⊢w=x\to \left(w\subseteq D\leftrightarrow x\subseteq D\right)$$
56		mpteq1	$$⊢w=x\to \left(k\in w⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(k\in x⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
57	56	oveq2d	$$⊢w=x\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
58		eleq2	$$⊢w=x\to \left(y\in w\leftrightarrow y\in x\right)$$
59	58	ifbid	$$⊢w=x\to if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)=if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)$$
60	59	mpteq2dv	$$⊢w=x\to \left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)$$
61	57 60	eqeq12d	$$⊢w=x\to \left(\underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\leftrightarrow \underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)$$
62	55 61	imbi12d	$$⊢w=x\to \left(\left(w\subseteq D\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\leftrightarrow \left(x\subseteq D\to \underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
63	62	imbi2d	$$⊢w=x\to \left(\left(\phi \to \left(w\subseteq D\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(x\subseteq D\to \underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
64		sseq1	$$⊢w=x\cup \left\{z\right\}\to \left(w\subseteq D\leftrightarrow x\cup \left\{z\right\}\subseteq D\right)$$
65		mpteq1	$$⊢w=x\cup \left\{z\right\}\to \left(k\in w⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(k\in \left(x\cup \left\{z\right\}\right)⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
66	65	oveq2d	$$⊢w=x\cup \left\{z\right\}\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
67		eleq2	$$⊢w=x\cup \left\{z\right\}\to \left(y\in w\leftrightarrow y\in \left(x\cup \left\{z\right\}\right)\right)$$
68	67	ifbid	$$⊢w=x\cup \left\{z\right\}\to if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)=if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)$$
69	68	mpteq2dv	$$⊢w=x\cup \left\{z\right\}\to \left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)$$
70	66 69	eqeq12d	$$⊢w=x\cup \left\{z\right\}\to \left(\underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\leftrightarrow \underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)$$
71	64 70	imbi12d	$$⊢w=x\cup \left\{z\right\}\to \left(\left(w\subseteq D\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\leftrightarrow \left(x\cup \left\{z\right\}\subseteq D\to \underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
72	71	imbi2d	$$⊢w=x\cup \left\{z\right\}\to \left(\left(\phi \to \left(w\subseteq D\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(x\cup \left\{z\right\}\subseteq D\to \underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
73		sseq1	$$⊢w=X\mathrm{supp}\underset{\dot{}}{0}\to \left(w\subseteq D\leftrightarrow X\mathrm{supp}\underset{\dot{}}{0}\subseteq D\right)$$
74		mpteq1	$$⊢w=X\mathrm{supp}\underset{\dot{}}{0}\to \left(k\in w⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(k\in {supp}_{\underset{\dot{}}{0}}\left(X\right)⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
75	74	oveq2d	$$⊢w=X\mathrm{supp}\underset{\dot{}}{0}\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\underset{k\in X\mathrm{supp}\underset{\dot{}}{0}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
76		eleq2	$$⊢w=X\mathrm{supp}\underset{\dot{}}{0}\to \left(y\in w\leftrightarrow y\in {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)$$
77	76	ifbid	$$⊢w=X\mathrm{supp}\underset{\dot{}}{0}\to if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)=if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)$$
78	77	mpteq2dv	$$⊢w=X\mathrm{supp}\underset{\dot{}}{0}\to \left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)$$
79	75 78	eqeq12d	$$⊢w=X\mathrm{supp}\underset{\dot{}}{0}\to \left(\underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\leftrightarrow \underset{k\in X\mathrm{supp}\underset{\dot{}}{0}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)$$
80	73 79	imbi12d	$$⊢w=X\mathrm{supp}\underset{\dot{}}{0}\to \left(\left(w\subseteq D\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\leftrightarrow \left(X\mathrm{supp}\underset{\dot{}}{0}\subseteq D\to \underset{k\in X\mathrm{supp}\underset{\dot{}}{0}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
81	80	imbi2d	$$⊢w=X\mathrm{supp}\underset{\dot{}}{0}\to \left(\left(\phi \to \left(w\subseteq D\to \underset{k\in w}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in w,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(X\mathrm{supp}\underset{\dot{}}{0}\subseteq D\to \underset{k\in X\mathrm{supp}\underset{\dot{}}{0}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
82		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
83	8 82	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
84	1 2 3 44 5 83	mpl0	$$⊢\phi \to 0_P=D\times \left\{\underset{\dot{}}{0}\right\}$$
85		fconstmpt	$$⊢D\times \left\{\underset{\dot{}}{0}\right\}=\left(y\in D⟼\underset{\dot{}}{0}\right)$$
86	84 85	eqtrdi	$$⊢\phi \to 0_P=\left(y\in D⟼\underset{\dot{}}{0}\right)$$
87	86	a1d	$$⊢\phi \to \left(\varnothing \subseteq D\to 0_P=\left(y\in D⟼\underset{\dot{}}{0}\right)\right)$$
88		ssun1	$$⊢x\subseteq x\cup \left\{z\right\}$$
89		sstr2	$$⊢x\subseteq x\cup \left\{z\right\}\to \left(x\cup \left\{z\right\}\subseteq D\to x\subseteq D\right)$$
90	88 89	ax-mp	$$⊢x\cup \left\{z\right\}\subseteq D\to x\subseteq D$$
91	90	imim1i	$$⊢\left(x\subseteq D\to \underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\to \left(x\cup \left\{z\right\}\subseteq D\to \underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)$$
92		oveq1	$$⊢\underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\to \left(\underset{k\in x}{{\sum }_P},\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\right){+}_P\left(X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right){+}_P\left(X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
93		eqid	$$⊢{+}_P={+}_P$$
94	1 5 8	mplringd	$$⊢\phi \to P\in \mathrm{Ring}$$
95		ringcmn	$$⊢P\in \mathrm{Ring}\to P\in \mathrm{CMnd}$$
96	94 95	syl	$$⊢\phi \to P\in \mathrm{CMnd}$$
97	96	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to P\in \mathrm{CMnd}$$
98		simprll	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to x\in \mathrm{Fin}$$
99		simprr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to x\cup \left\{z\right\}\subseteq D$$
100	99	unssad	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to x\subseteq D$$
101	100	sselda	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge k\in x\right)\to k\in D$$
102	5	adantr	$$⊢\left(\phi \wedge k\in D\right)\to I\in W$$
103	8	adantr	$$⊢\left(\phi \wedge k\in D\right)\to R\in \mathrm{Ring}$$
104	1 102 103	mpllmodd	$$⊢\left(\phi \wedge k\in D\right)\to P\in \mathrm{LMod}$$
105	11	ffvelcdmda	$$⊢\left(\phi \wedge k\in D\right)\to X\left(k\right)\in {\mathrm{Base}}_R$$
106	1 5 8	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
107	106	adantr	$$⊢\left(\phi \wedge k\in D\right)\to R=\mathrm{Scalar}\left(P\right)$$
108	107	fveq2d	$$⊢\left(\phi \wedge k\in D\right)\to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
109	105 108	eleqtrd	$$⊢\left(\phi \wedge k\in D\right)\to X\left(k\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
110		simpr	$$⊢\left(\phi \wedge k\in D\right)\to k\in D$$
111	1 6 3 4 2 102 103 110	mplmon	$$⊢\left(\phi \wedge k\in D\right)\to \left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
112		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
113		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
114	6 112 7 113	lmodvscl	$$⊢\left(P\in \mathrm{LMod}\wedge X\left(k\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge \left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B\right)\to X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
115	104 109 111 114	syl3anc	$$⊢\left(\phi \wedge k\in D\right)\to X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
116	115	adantlr	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge k\in D\right)\to X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
117	101 116	syldan	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge k\in x\right)\to X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
118		vex	$$⊢z\in \mathrm{V}$$
119	118	a1i	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to z\in \mathrm{V}$$
120		simprlr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \neg z\in x$$
121	1 5 8	mpllmodd	$$⊢\phi \to P\in \mathrm{LMod}$$
122	121	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to P\in \mathrm{LMod}$$
123	11	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to X:D⟶{\mathrm{Base}}_R$$
124	99	unssbd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left\{z\right\}\subseteq D$$
125	118	snss	$$⊢z\in D\leftrightarrow \left\{z\right\}\subseteq D$$
126	124 125	sylibr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to z\in D$$
127	123 126	ffvelcdmd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to X\left(z\right)\in {\mathrm{Base}}_R$$
128	106	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to R=\mathrm{Scalar}\left(P\right)$$
129	128	fveq2d	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
130	127 129	eleqtrd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to X\left(z\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
131	5	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to I\in W$$
132	8	adantr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to R\in \mathrm{Ring}$$
133	1 6 3 4 2 131 132 126	mplmon	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
134	6 112 7 113	lmodvscl	$$⊢\left(P\in \mathrm{LMod}\wedge X\left(z\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge \left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B\right)\to X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
135	122 130 133 134	syl3anc	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
136		fveq2	$$⊢k=z\to X\left(k\right)=X\left(z\right)$$
137		equequ2	$$⊢k=z\to \left(y=k\leftrightarrow y=z\right)$$
138	137	ifbid	$$⊢k=z\to if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
139	138	mpteq2dv	$$⊢k=z\to \left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
140	136 139	oveq12d	$$⊢k=z\to X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
141	6 93 97 98 117 119 120 135 140	gsumunsn	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(\underset{k\in x}{{\sum }_P},\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\right){+}_P\left(X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
142		eqid	$$⊢{+}_R={+}_R$$
143	123	ffvelcdmda	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\to X\left(y\right)\in {\mathrm{Base}}_R$$
144	10 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
145	8 144	syl	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
146	145	ad2antrr	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
147	143 146	ifcld	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
148	147	fmpttd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
149		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
150	149 18	elmap	$$⊢\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in \left({{\mathrm{Base}}_R}^D\right)\leftrightarrow \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
151	148 150	sylibr	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in \left({{\mathrm{Base}}_R}^D\right)$$
152	33 10 2 34 131	psrbas	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={{\mathrm{Base}}_R}^D$$
153	151 152	eleqtrrd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
154	18	mptex	$$⊢\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
155		funmpt	$$⊢\mathrm{Fun}\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)$$
156	154 155 20	3pm3.2i	$$⊢\left(\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)$$
157	156	a1i	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)$$
158		eldifn	$$⊢y\in \left(D\setminus x\right)\to \neg y\in x$$
159	158	adantl	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in \left(D\setminus x\right)\right)\to \neg y\in x$$
160	159	iffalsed	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in \left(D\setminus x\right)\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
161	18	a1i	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to D\in \mathrm{V}$$
162	160 161	suppss2	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq x$$
163		suppssfifsupp	$$⊢\left(\left(\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\wedge \left(x\in \mathrm{Fin}\wedge \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq x\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)$$
164	157 98 162 163	syl12anc	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)$$
165	1 33 34 3 6	mplelbas	$$⊢\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in B\leftrightarrow \left(\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge {finSupp}_{\underset{\dot{}}{0}}\left(\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
166	153 164 165	sylanbrc	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in B$$
167	1 6 142 93 166 135	mpladd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right){+}_P\left(X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right){{+}_R}_f\left(X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
168		ovexd	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\to X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
169		eqidd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)$$
170		eqid	$$⊢{\cdot }_R={\cdot }_R$$
171	1 7 10 6 170 2 127 133	mplvsca	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(D\times \left\{X\left(z\right)\right\}\right){{\cdot }_R}_f\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
172	127	adantr	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\to X\left(z\right)\in {\mathrm{Base}}_R$$
173	10 4	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
174	173 144	ifcld	$$⊢R\in \mathrm{Ring}\to if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
175	8 174	syl	$$⊢\phi \to if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
176	175	ad2antrr	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\to if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
177		fconstmpt	$$⊢D\times \left\{X\left(z\right)\right\}=\left(y\in D⟼X\left(z\right)\right)$$
178	177	a1i	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to D\times \left\{X\left(z\right)\right\}=\left(y\in D⟼X\left(z\right)\right)$$
179		eqidd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
180	161 172 176 178 179	offval2	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(D\times \left\{X\left(z\right)\right\}\right){{\cdot }_R}_f\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
181	171 180	eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
182	161 147 168 169 181	offval2	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right){{+}_R}_f\left(X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\left(X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
183	132 82	syl	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to R\in \mathrm{Grp}$$
184	10 142 3	grplid	$$⊢\left(R\in \mathrm{Grp}\wedge X\left(z\right)\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{0}{+}_{R}X\left(z\right)=X\left(z\right)$$
185	183 127 184	syl2anc	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \underset{\dot{}}{0}{+}_{R}X\left(z\right)=X\left(z\right)$$
186	185	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to \underset{\dot{}}{0}{+}_{R}X\left(z\right)=X\left(z\right)$$
187		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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to y\in \left\{z\right\}$$
188		velsn	$$⊢y\in \left\{z\right\}\leftrightarrow y=z$$
189	187 188	sylib	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to y=z$$
190	189	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to X\left(y\right)=X\left(z\right)$$
191	186 190	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to \underset{\dot{}}{0}{+}_{R}X\left(z\right)=X\left(y\right)$$
192	120	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to \neg z\in x$$
193	189 192	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to \neg y\in x$$
194	193	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
195	189	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{1}$$
196	195	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=X\left(z\right){\cdot }_R\underset{\dot{}}{1}$$
197	10 170 4	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge X\left(z\right)\in {\mathrm{Base}}_R\right)\to X\left(z\right){\cdot }_R\underset{\dot{}}{1}=X\left(z\right)$$
198	132 127 197	syl2anc	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to X\left(z\right){\cdot }_R\underset{\dot{}}{1}=X\left(z\right)$$
199	198	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to X\left(z\right){\cdot }_R\underset{\dot{}}{1}=X\left(z\right)$$
200	196 199	eqtrd	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=X\left(z\right)$$
201	194 200	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\left(X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{\dot{}}{0}{+}_{R}X\left(z\right)$$
202		elun2	$$⊢y\in \left\{z\right\}\to y\in \left(x\cup \left\{z\right\}\right)$$
203	202	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to y\in \left(x\cup \left\{z\right\}\right)$$
204	203	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)=X\left(y\right)$$
205	191 201 204	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 D\right)\right)\wedge y\in D\right)\wedge y\in \left\{z\right\}\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\left(X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)$$
206	83	ad2antrr	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\to R\in \mathrm{Grp}$$
207	10 142 3	grprid	$$⊢\left(R\in \mathrm{Grp}\wedge if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}=if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)$$
208	206 147 207	syl2anc	$$⊢\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}=if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)$$
209	208	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 D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}=if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)$$
210		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 D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to \neg y\in \left\{z\right\}$$
211	210 188	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 D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to \neg y=z$$
212	211	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 D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
213	212	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 D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=X\left(z\right){\cdot }_R\underset{\dot{}}{0}$$
214	10 170 3	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge X\left(z\right)\in {\mathrm{Base}}_R\right)\to X\left(z\right){\cdot }_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
215	132 127 214	syl2anc	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to X\left(z\right){\cdot }_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
216	215	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 D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to X\left(z\right){\cdot }_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
217	213 216	eqtrd	$$⊢\left(\left(\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
218	217	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 D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\left(X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}$$
219		elun	$$⊢y\in \left(x\cup \left\{z\right\}\right)\leftrightarrow \left(y\in x\vee y\in \left\{z\right\}\right)$$
220		orcom	$$⊢\left(y\in x\vee y\in \left\{z\right\}\right)\leftrightarrow \left(y\in \left\{z\right\}\vee y\in x\right)$$
221	219 220	bitri	$$⊢y\in \left(x\cup \left\{z\right\}\right)\leftrightarrow \left(y\in \left\{z\right\}\vee y\in x\right)$$
222		biorf	$$⊢\neg y\in \left\{z\right\}\to \left(y\in x\leftrightarrow \left(y\in \left\{z\right\}\vee y\in x\right)\right)$$
223	221 222	bitr4id	$$⊢\neg y\in \left\{z\right\}\to \left(y\in \left(x\cup \left\{z\right\}\right)\leftrightarrow y\in x\right)$$
224	223	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 D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to \left(y\in \left(x\cup \left\{z\right\}\right)\leftrightarrow y\in x\right)$$
225	224	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 D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)=if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)$$
226	209 218 225	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 D\right)\right)\wedge y\in D\right)\wedge \neg y\in \left\{z\right\}\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\left(X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)$$
227	205 226	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 D\right)\right)\wedge y\in D\right)\to if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\left(X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)$$
228	227	mpteq2dva	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right){+}_R\left(X\left(z\right){\cdot }_{R}if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)$$
229	167 182 228	3eqtrrd	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right){+}_P\left(X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
230	141 229	eqeq12d	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(\underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(\underset{k\in x}{{\sum }_P},\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\right){+}_P\left(X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right){+}_P\left(X\left(z\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\right)$$
231	92 230	imbitrrid	$$⊢\left(\phi \wedge \left(\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\wedge x\cup \left\{z\right\}\subseteq D\right)\right)\to \left(\underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\to \underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)$$
232	231	expr	$$⊢\left(\phi \wedge \left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\right)\to \left(x\cup \left\{z\right\}\subseteq D\to \left(\underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\to \underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
233	232	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 D\to \underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\to \left(x\cup \left\{z\right\}\subseteq D\to \underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
234	91 233	syl5	$$⊢\left(\phi \wedge \left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\right)\to \left(\left(x\subseteq D\to \underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\to \left(x\cup \left\{z\right\}\subseteq D\to \underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
235	234	expcom	$$⊢\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\to \left(\phi \to \left(\left(x\subseteq D\to \underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\to \left(x\cup \left\{z\right\}\subseteq D\to \underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
236	235	a2d	$$⊢\left(x\in \mathrm{Fin}\wedge \neg z\in x\right)\to \left(\left(\phi \to \left(x\subseteq D\to \underset{k\in x}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)\to \left(\phi \to \left(x\cup \left\{z\right\}\subseteq D\to \underset{k\in x\cup \left\{z\right\}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in \left(x\cup \left\{z\right\}\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)\right)$$
237	54 63 72 81 87 236	findcard2s	$$⊢X\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\to \left(\phi \to \left(X\mathrm{supp}\underset{\dot{}}{0}\subseteq D\to \underset{k\in X\mathrm{supp}\underset{\dot{}}{0}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)\right)$$
238	38 237	mpcom	$$⊢\phi \to \left(X\mathrm{supp}\underset{\dot{}}{0}\subseteq D\to \underset{k\in X\mathrm{supp}\underset{\dot{}}{0}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)\right)$$
239	32 238	mpd	$$⊢\phi \to \underset{k\in X\mathrm{supp}\underset{\dot{}}{0}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\left(y\in D⟼if\left(y\in {supp}_{\underset{\dot{}}{0}}\left(X\right),X\left(y\right),\underset{\dot{}}{0}\right)\right)$$
240	30 239	eqtr4d	$$⊢\phi \to X=\underset{k\in X\mathrm{supp}\underset{\dot{}}{0}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
241	32	resmptd	$$⊢\phi \to {\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(X\right)}=\left(k\in {supp}_{\underset{\dot{}}{0}}\left(X\right)⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
242	241	oveq2d	$$⊢\phi \to {\sum }_P\left({\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(X\right)}\right)=\underset{k\in X\mathrm{supp}\underset{\dot{}}{0}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
243	115	fmpttd	$$⊢\phi \to \left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right):D⟶B$$
244	11 16 19 21	suppssr	$$⊢\left(\phi \wedge k\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)\to X\left(k\right)=\underset{\dot{}}{0}$$
245	244	oveq1d	$$⊢\left(\phi \wedge k\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)\to X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\underset{\dot{}}{0}\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
246		eldifi	$$⊢k\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\to k\in D$$
247	107	fveq2d	$$⊢\left(\phi \wedge k\in D\right)\to 0_R=0_{\mathrm{Scalar}\left(P\right)}$$
248	3 247	eqtrid	$$⊢\left(\phi \wedge k\in D\right)\to \underset{\dot{}}{0}=0_{\mathrm{Scalar}\left(P\right)}$$
249	248	oveq1d	$$⊢\left(\phi \wedge k\in D\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=0_{\mathrm{Scalar}\left(P\right)}\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
250		eqid	$$⊢0_{\mathrm{Scalar}\left(P\right)}=0_{\mathrm{Scalar}\left(P\right)}$$
251	6 112 7 250 44	lmod0vs	$$⊢\left(P\in \mathrm{LMod}\wedge \left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B\right)\to 0_{\mathrm{Scalar}\left(P\right)}\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=0_P$$
252	104 111 251	syl2anc	$$⊢\left(\phi \wedge k\in D\right)\to 0_{\mathrm{Scalar}\left(P\right)}\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=0_P$$
253	249 252	eqtrd	$$⊢\left(\phi \wedge k\in D\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=0_P$$
254	246 253	sylan2	$$⊢\left(\phi \wedge k\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=0_P$$
255	245 254	eqtrd	$$⊢\left(\phi \wedge k\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\right)\to X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=0_P$$
256	255 19	suppss2	$$⊢\phi \to \left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\subseteq X\mathrm{supp}\underset{\dot{}}{0}$$
257	18	mptex	$$⊢\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}$$
258		funmpt	$$⊢\mathrm{Fun}\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
259		fvex	$$⊢0_P\in \mathrm{V}$$
260	257 258 259	3pm3.2i	$$⊢\left(\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\wedge 0_P\in \mathrm{V}\right)$$
261	260	a1i	$$⊢\phi \to \left(\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\wedge 0_P\in \mathrm{V}\right)$$
262		suppssfifsupp	$$⊢\left(\left(\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\wedge 0_P\in \mathrm{V}\right)\wedge \left(X\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\wedge \left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\mathrm{supp}{0}_P\subseteq X\mathrm{supp}\underset{\dot{}}{0}\right)\right)\to {finSupp}_{0_P}\left(\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\right)$$
263	261 38 256 262	syl12anc	$$⊢\phi \to {finSupp}_{0_P}\left(\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\right)$$
264	6 44 96 19 243 256 263	gsumres	$$⊢\phi \to {\sum }_P\left({\left(k\in D⟼X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\upharpoonright }_{{supp}_{\underset{\dot{}}{0}}\left(X\right)}\right)=\underset{k\in D}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
265	242 264	eqtr3d	$$⊢\phi \to \underset{k\in X\mathrm{supp}\underset{\dot{}}{0}}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)=\underset{k\in D}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
266	240 265	eqtrd	$$⊢\phi \to X=\underset{k\in D}{{\sum }_P}\left(X\left(k\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=k,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$