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	mplring	$$⊢\left(I\in W\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{Ring}$$
95	5 8 94	syl2anc	$$⊢\phi \to P\in \mathrm{Ring}$$
96		ringcmn	$$⊢P\in \mathrm{Ring}\to P\in \mathrm{CMnd}$$
97	95 96	syl	$$⊢\phi \to P\in \mathrm{CMnd}$$
98	97	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}$$
99		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}$$
100		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$$
101	100	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$$
102	101	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$$
103	5	adantr	$$⊢\left(\phi \wedge k\in D\right)\to I\in W$$
104	8	adantr	$$⊢\left(\phi \wedge k\in D\right)\to R\in \mathrm{Ring}$$
105	1	mpllmod	$$⊢\left(I\in W\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{LMod}$$
106	103 104 105	syl2anc	$$⊢\left(\phi \wedge k\in D\right)\to P\in \mathrm{LMod}$$
107	11	ffvelrnda	$$⊢\left(\phi \wedge k\in D\right)\to X\left(k\right)\in {\mathrm{Base}}_R$$
108	1 5 8	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
109	108	adantr	$$⊢\left(\phi \wedge k\in D\right)\to R=\mathrm{Scalar}\left(P\right)$$
110	109	fveq2d	$$⊢\left(\phi \wedge k\in D\right)\to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
111	107 110	eleqtrd	$$⊢\left(\phi \wedge k\in D\right)\to X\left(k\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
112		simpr	$$⊢\left(\phi \wedge k\in D\right)\to k\in D$$
113	1 6 3 4 2 103 104 112	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$$
114		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
115		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
116	6 114 7 115	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$$
117	106 111 113 116	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$$
118	117	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$$
119	102 118	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$$
120		vex	$$⊢z\in \mathrm{V}$$
121	120	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}$$
122		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$$
123	5 8 105	syl2anc	$$⊢\phi \to P\in \mathrm{LMod}$$
124	123	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}$$
125	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$$
126	100	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$$
127	120	snss	$$⊢z\in D\leftrightarrow \left\{z\right\}\subseteq D$$
128	126 127	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$$
129	125 128	ffvelrnd	$$⊢\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$$
130	108	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)$$
131	130	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)}$$
132	129 131	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)}$$
133	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$$
134	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}$$
135	1 6 3 4 2 133 134 128	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$$
136	6 114 7 115	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$$
137	124 132 135 136	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$$
138		fveq2	$$⊢k=z\to X\left(k\right)=X\left(z\right)$$
139		equequ2	$$⊢k=z\to \left(y=k\leftrightarrow y=z\right)$$
140	139	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)$$
141	140	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)$$
142	138 141	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)$$
143	6 93 98 99 119 121 122 137 142	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)$$
144		eqid	$$⊢{+}_R={+}_R$$
145	125	ffvelrnda	$$⊢\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$$
146	10 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
147	8 146	syl	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
148	147	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$$
149	145 148	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$$
150	149	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$$
151		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
152	151 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$$
153	150 152	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)$$
154	33 10 2 34 133	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$$
155	153 154	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)}$$
156	18	mptex	$$⊢\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
157		funmpt	$$⊢\mathrm{Fun}\left(y\in D⟼if\left(y\in x,X\left(y\right),\underset{\dot{}}{0}\right)\right)$$
158	156 157 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)$$
159	158	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)$$
160		eldifn	$$⊢y\in \left(D\setminus x\right)\to \neg y\in x$$
161	160	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$$
162	161	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}$$
163	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}$$
164	162 163	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$$
165		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)$$
166	159 99 164 165	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)$$
167	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)$$
168	155 166 167	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$$
169	1 6 144 93 168 137	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)$$
170		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}$$
171		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)$$
172		eqid	$$⊢{\cdot }_R={\cdot }_R$$
173	1 7 10 6 172 2 129 135	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)$$
174	129	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$$
175	10 4	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
176	175 146	ifcld	$$⊢R\in \mathrm{Ring}\to if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
177	8 176	syl	$$⊢\phi \to if\left(y=z,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
178	177	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$$
179		fconstmpt	$$⊢D\times \left\{X\left(z\right)\right\}=\left(y\in D⟼X\left(z\right)\right)$$
180	179	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)$$
181		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)$$
182	163 174 178 180 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(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)$$
183	173 182	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)$$
184	163 149 170 171 183	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)$$
185	134 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}$$
186	10 144 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)$$
187	185 129 186	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)$$
188	187	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)$$
189		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\}$$
190		velsn	$$⊢y\in \left\{z\right\}\leftrightarrow y=z$$
191	189 190	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$$
192	191	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)$$
193	188 192	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)$$
194	122	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$$
195	191 194	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$$
196	195	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}$$
197	191	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}$$
198	197	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}$$
199	10 172 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)$$
200	134 129 199	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)$$
201	200	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)$$
202	198 201	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)$$
203	196 202	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)$$
204		elun2	$$⊢y\in \left\{z\right\}\to y\in \left(x\cup \left\{z\right\}\right)$$
205	204	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)$$
206	205	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)$$
207	193 203 206	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)$$
208	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}$$
209	10 144 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)$$
210	208 149 209	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)$$
211	210	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)$$
212		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\}$$
213	212 190	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$$
214	213	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}$$
215	214	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}$$
216	10 172 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}$$
217	134 129 216	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}$$
218	217	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}$$
219	215 218	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}$$
220	219	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}$$
221		elun	$$⊢y\in \left(x\cup \left\{z\right\}\right)\leftrightarrow \left(y\in x\vee y\in \left\{z\right\}\right)$$
222		orcom	$$⊢\left(y\in x\vee y\in \left\{z\right\}\right)\leftrightarrow \left(y\in \left\{z\right\}\vee y\in x\right)$$
223	221 222	bitri	$$⊢y\in \left(x\cup \left\{z\right\}\right)\leftrightarrow \left(y\in \left\{z\right\}\vee y\in x\right)$$
224		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)$$
225	223 224	bitr4id	$$⊢\neg y\in \left\{z\right\}\to \left(y\in \left(x\cup \left\{z\right\}\right)\leftrightarrow y\in x\right)$$
226	225	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)$$
227	226	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)$$
228	211 220 227	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)$$
229	207 228	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)$$
230	229	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)$$
231	169 184 230	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)$$
232	143 231	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)$$
233	92 232	syl5ibr	$$⊢\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)$$
234	233	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)$$
235	234	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)$$
236	91 235	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)$$
237	236	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)$$
238	237	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)$$
239	54 63 72 81 87 238	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)$$
240	38 239	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)$$
241	32 240	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)$$
242	30 241	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)$$
243	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)$$
244	243	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)$$
245	117	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$$
246	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}$$
247	246	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)$$
248		eldifi	$$⊢k\in \left(D\setminus {supp}_{\underset{\dot{}}{0}}\left(X\right)\right)\to k\in D$$
249	109	fveq2d	$$⊢\left(\phi \wedge k\in D\right)\to 0_R=0_{\mathrm{Scalar}\left(P\right)}$$
250	3 249	eqtrid	$$⊢\left(\phi \wedge k\in D\right)\to \underset{\dot{}}{0}=0_{\mathrm{Scalar}\left(P\right)}$$
251	250	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)$$
252		eqid	$$⊢0_{\mathrm{Scalar}\left(P\right)}=0_{\mathrm{Scalar}\left(P\right)}$$
253	6 114 7 252 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$$
254	106 113 253	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$$
255	251 254	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$$
256	248 255	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$$
257	247 256	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$$
258	257 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}$$
259	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}$$
260		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)$$
261		fvex	$$⊢0_P\in \mathrm{V}$$
262	259 260 261	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)$$
263	262	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)$$
264		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)$$
265	263 38 258 264	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)$$
266	6 44 97 19 245 258 265	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)$$
267	244 266	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)$$
268	242 267	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)$$