Theorem esplyfvaln

Description: The last elementary symmetric polynomial is the product of all variables. (Contributed by Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	esplyfval1.w	$$⊢W=I\mathrm{mPoly}R$$
	esplyfval1.v	$$⊢V=I\mathrm{mVar}R$$
	esplyfval1.e	No typesetting found for |- E = ( I eSymPoly R ) with typecode |-
	esplyfval1.i	$$⊢\phi \to I\in \mathrm{Fin}$$
	esplyfvaln.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	esplyfvaln.n	$$⊢N=\left|I\right|$$
	esplyfvaln.m	$$⊢M={\mathrm{mulGrp}}_W$$
Assertion	esplyfvaln	$$⊢\phi \to E\left(N\right)={\sum }_{M}V$$

Proof

Step	Hyp	Ref	Expression
1		esplyfval1.w	$$⊢W=I\mathrm{mPoly}R$$
2		esplyfval1.v	$$⊢V=I\mathrm{mVar}R$$
3		esplyfval1.e	Could not format E = ( I eSymPoly R ) : No typesetting found for |- E = ( I eSymPoly R ) with typecode |-
4		esplyfval1.i	$$⊢\phi \to I\in \mathrm{Fin}$$
5		esplyfvaln.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		esplyfvaln.n	$$⊢N=\left|I\right|$$
7		esplyfvaln.m	$$⊢M={\mathrm{mulGrp}}_W$$
8	3	fveq1i	Could not format ( E ` N ) = ( ( I eSymPoly R ) ` N ) : No typesetting found for |- ( E ` N ) = ( ( I eSymPoly R ) ` N ) with typecode |-
9		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
10	5	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
11		hashcl	$$⊢I\in \mathrm{Fin}\to \left|I\right|\in {\mathbb{N}}_0$$
12	4 11	syl	$$⊢\phi \to \left|I\right|\in {\mathbb{N}}_0$$
13	6 12	eqeltrid	$$⊢\phi \to N\in {\mathbb{N}}_0$$
14		eqid	$$⊢0_R=0_R$$
15		eqid	$$⊢1_R=1_R$$
16	9 4 10 13 14 15	esplyfval3	Could not format ( ph -> ( ( I eSymPoly R ) ` N ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` N ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) with typecode |-
17		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
18		breq1	$$⊢h={𝟙}_I\left(\left\{i\right\}\right)\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left({𝟙}_I\left(\left\{i\right\}\right)\right)\right)$$
19		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
20	19	a1i	$$⊢\left(\phi \wedge i\in I\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
21	4	adantr	$$⊢\left(\phi \wedge i\in I\right)\to I\in \mathrm{Fin}$$
22		snssi	$$⊢i\in I\to \left\{i\right\}\subseteq I$$
23		indf	$$⊢\left(I\in \mathrm{Fin}\wedge \left\{i\right\}\subseteq I\right)\to {𝟙}_I\left(\left\{i\right\}\right):I⟶\left\{0,1\right\}$$
24	4 22 23	syl2an	$$⊢\left(\phi \wedge i\in I\right)\to {𝟙}_I\left(\left\{i\right\}\right):I⟶\left\{0,1\right\}$$
25		0nn0	$$⊢0\in {\mathbb{N}}_0$$
26	25	a1i	$$⊢\left(\phi \wedge i\in I\right)\to 0\in {\mathbb{N}}_0$$
27		1nn0	$$⊢1\in {\mathbb{N}}_0$$
28	27	a1i	$$⊢\left(\phi \wedge i\in I\right)\to 1\in {\mathbb{N}}_0$$
29	26 28	prssd	$$⊢\left(\phi \wedge i\in I\right)\to \left\{0,1\right\}\subseteq {\mathbb{N}}_0$$
30	24 29	fssd	$$⊢\left(\phi \wedge i\in I\right)\to {𝟙}_I\left(\left\{i\right\}\right):I⟶{\mathbb{N}}_0$$
31	20 21 30	elmapdd	$$⊢\left(\phi \wedge i\in I\right)\to {𝟙}_I\left(\left\{i\right\}\right)\in \left({{\mathbb{N}}_0}^I\right)$$
32	24 21 26	fidmfisupp	$$⊢\left(\phi \wedge i\in I\right)\to {finSupp}_0\left({𝟙}_I\left(\left\{i\right\}\right)\right)$$
33	18 31 32	elrabd	$$⊢\left(\phi \wedge i\in I\right)\to {𝟙}_I\left(\left\{i\right\}\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
34	33	fmpttd	$$⊢\phi \to \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right):I⟶\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
35		eqeq2	$$⊢t=y\to \left(u=t\leftrightarrow u=y\right)$$
36	35	ifbid	$$⊢t=y\to if\left(u=t,1_R,0_R\right)=if\left(u=y,1_R,0_R\right)$$
37	36	mpteq2dv	$$⊢t=y\to \left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)=\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=y,1_R,0_R\right)\right)$$
38		eqeq1	$$⊢u=z\to \left(u=y\leftrightarrow z=y\right)$$
39	38	ifbid	$$⊢u=z\to if\left(u=y,1_R,0_R\right)=if\left(z=y,1_R,0_R\right)$$
40	39	cbvmptv	$$⊢\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=y,1_R,0_R\right)\right)=\left(z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(z=y,1_R,0_R\right)\right)$$
41	37 40	eqtrdi	$$⊢t=y\to \left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)=\left(z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(z=y,1_R,0_R\right)\right)$$
42	41	cbvmptv	$$⊢\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(z=y,1_R,0_R\right)\right)\right)$$
43	1 17 5 4 9 4 34 15 14 7 42	mplmonprod	$$⊢\phi \to {\sum }_M\left(\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)\circ \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\right)=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)\left(\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)$$
44		eqid	$$⊢\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)$$
45		eqeq2	$$⊢t=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\to \left(u=t\leftrightarrow u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)$$
46	45	ifbid	$$⊢t=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\to if\left(u=t,1_R,0_R\right)=if\left(u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right),1_R,0_R\right)$$
47	46	mpteq2dv	$$⊢t=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\to \left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)=\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right),1_R,0_R\right)\right)$$
48		simpr	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)$$
49	48	rneqd	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to \mathrm{ran}u=\mathrm{ran}\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)$$
50		nfv	$$⊢Ⅎj\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)$$
51		eqid	$$⊢\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)$$
52		eqid	$$⊢\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)=\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)$$
53		sneq	$$⊢i=k\to \left\{i\right\}=\left\{k\right\}$$
54	53	fveq2d	$$⊢i=k\to {𝟙}_I\left(\left\{i\right\}\right)={𝟙}_I\left(\left\{k\right\}\right)$$
55		simpr	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to k\in I$$
56		fvexd	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to {𝟙}_I\left(\left\{k\right\}\right)\in \mathrm{V}$$
57	52 54 55 56	fvmptd3	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)={𝟙}_I\left(\left\{k\right\}\right)$$
58	57	fveq1d	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)={𝟙}_I\left(\left\{k\right\}\right)\left(j\right)$$
59	4	ad2antrr	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to I\in \mathrm{Fin}$$
60	55	snssd	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to \left\{k\right\}\subseteq I$$
61		simplr	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to j\in I$$
62		indfval	$$⊢\left(I\in \mathrm{Fin}\wedge \left\{k\right\}\subseteq I\wedge j\in I\right)\to {𝟙}_I\left(\left\{k\right\}\right)\left(j\right)=if\left(j\in \left\{k\right\},1,0\right)$$
63	59 60 61 62	syl3anc	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to {𝟙}_I\left(\left\{k\right\}\right)\left(j\right)=if\left(j\in \left\{k\right\},1,0\right)$$
64		velsn	$$⊢j\in \left\{k\right\}\leftrightarrow j=k$$
65		equcom	$$⊢j=k\leftrightarrow k=j$$
66	64 65	bitri	$$⊢j\in \left\{k\right\}\leftrightarrow k=j$$
67	66	a1i	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to \left(j\in \left\{k\right\}\leftrightarrow k=j\right)$$
68	67	ifbid	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to if\left(j\in \left\{k\right\},1,0\right)=if\left(k=j,1,0\right)$$
69	58 63 68	3eqtrd	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)=if\left(k=j,1,0\right)$$
70	69	mpteq2dva	$$⊢\left(\phi \wedge j\in I\right)\to \left(k\in I⟼\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)=\left(k\in I⟼if\left(k=j,1,0\right)\right)$$
71	70	oveq2d	$$⊢\left(\phi \wedge j\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)=\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}if\left(k=j,1,0\right)$$
72		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
73		cnfldfld	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Field}$$
74		id	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Field}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Field}$$
75	74	fldcrngd	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Field}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
76		crngring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
77		ringcmn	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
78	75 76 77	3syl	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Field}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
79	73 78	mp1i	$$⊢\left(\phi \wedge j\in I\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
80	79	cmnmndd	$$⊢\left(\phi \wedge j\in I\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
81	4	adantr	$$⊢\left(\phi \wedge j\in I\right)\to I\in \mathrm{Fin}$$
82		simpr	$$⊢\left(\phi \wedge j\in I\right)\to j\in I$$
83		eqid	$$⊢\left(k\in I⟼if\left(k=j,1,0\right)\right)=\left(k\in I⟼if\left(k=j,1,0\right)\right)$$
84		ax-1cn	$$⊢1\in ℂ$$
85		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
86	84 85	eleqtri	$$⊢1\in {\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
87	86	a1i	$$⊢\left(\phi \wedge j\in I\right)\to 1\in {\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
88	72 80 81 82 83 87	gsummptif1n0	$$⊢\left(\phi \wedge j\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}if\left(k=j,1,0\right)=1$$
89	71 88	eqtrd	$$⊢\left(\phi \wedge j\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)=1$$
90		1elpr01	$$⊢1\in \left\{0,1\right\}$$
91	89 90	eqeltrdi	$$⊢\left(\phi \wedge j\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\in \left\{0,1\right\}$$
92	91	adantlr	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge j\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\in \left\{0,1\right\}$$
93	50 51 92	rnmptssd	$$⊢\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \mathrm{ran}\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\subseteq \left\{0,1\right\}$$
94	93	adantr	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to \mathrm{ran}\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\subseteq \left\{0,1\right\}$$
95	49 94	eqsstrd	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to \mathrm{ran}u\subseteq \left\{0,1\right\}$$
96	48	oveq1d	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to u\mathrm{supp}0=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\mathrm{supp}0$$
97		suppssdm	$$⊢\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\mathrm{supp}0\subseteq \mathrm{dom}\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)$$
98		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
99	98	a1i	$$⊢\left(\phi \wedge j\in I\right)\to {\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
100	25	a1i	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to 0\in {\mathbb{N}}_0$$
101	27	a1i	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to 1\in {\mathbb{N}}_0$$
102	100 101	prssd	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to \left\{0,1\right\}\subseteq {\mathbb{N}}_0$$
103		indf	$$⊢\left(I\in \mathrm{Fin}\wedge \left\{k\right\}\subseteq I\right)\to {𝟙}_I\left(\left\{k\right\}\right):I⟶\left\{0,1\right\}$$
104	59 60 103	syl2anc	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to {𝟙}_I\left(\left\{k\right\}\right):I⟶\left\{0,1\right\}$$
105	104 61	ffvelcdmd	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to {𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\in \left\{0,1\right\}$$
106	102 105	sseldd	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to {𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\in {\mathbb{N}}_0$$
107	58 106	eqeltrd	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\in {\mathbb{N}}_0$$
108	107	fmpttd	$$⊢\left(\phi \wedge j\in I\right)\to \left(k\in I⟼\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right):I⟶{\mathbb{N}}_0$$
109	25	a1i	$$⊢\left(\phi \wedge j\in I\right)\to 0\in {\mathbb{N}}_0$$
110	108 81 109	fdmfifsupp	$$⊢\left(\phi \wedge j\in I\right)\to {finSupp}_0\left(\left(k\in I⟼\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)$$
111	72 79 81 99 108 110	gsumsubmcl	$$⊢\left(\phi \wedge j\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\in {\mathbb{N}}_0$$
112	51 111	dmmptd	$$⊢\phi \to \mathrm{dom}\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)=I$$
113	97 112	sseqtrid	$$⊢\phi \to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\mathrm{supp}0\subseteq I$$
114		nfv	$$⊢Ⅎj\left(\phi \wedge i\in I\right)$$
115		ovexd	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge j\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\in \mathrm{V}$$
116		eqid	$$⊢\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)$$
117	114 115 116	fnmptd	$$⊢\left(\phi \wedge i\in I\right)\to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)FnI$$
118		simpr	$$⊢\left(\phi \wedge i\in I\right)\to i\in I$$
119		fveq2	$$⊢j=i\to {𝟙}_I\left(\left\{k\right\}\right)\left(j\right)={𝟙}_I\left(\left\{k\right\}\right)\left(i\right)$$
120	119	mpteq2dv	$$⊢j=i\to \left(k\in I⟼{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)=\left(k\in I⟼{𝟙}_I\left(\left\{k\right\}\right)\left(i\right)\right)$$
121	120	oveq2d	$$⊢j=i\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)=\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(i\right)$$
122		ovexd	$$⊢\left(\phi \wedge i\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(i\right)\in \mathrm{V}$$
123	116 121 118 122	fvmptd3	$$⊢\left(\phi \wedge i\in I\right)\to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)\left(i\right)=\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(i\right)$$
124	4	ad2antrr	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to I\in \mathrm{Fin}$$
125		simpr	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to k\in I$$
126	125	snssd	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to \left\{k\right\}\subseteq I$$
127		simplr	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to i\in I$$
128		indfval	$$⊢\left(I\in \mathrm{Fin}\wedge \left\{k\right\}\subseteq I\wedge i\in I\right)\to {𝟙}_I\left(\left\{k\right\}\right)\left(i\right)=if\left(i\in \left\{k\right\},1,0\right)$$
129	124 126 127 128	syl3anc	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to {𝟙}_I\left(\left\{k\right\}\right)\left(i\right)=if\left(i\in \left\{k\right\},1,0\right)$$
130		velsn	$$⊢i\in \left\{k\right\}\leftrightarrow i=k$$
131		equcom	$$⊢i=k\leftrightarrow k=i$$
132	130 131	bitri	$$⊢i\in \left\{k\right\}\leftrightarrow k=i$$
133	132	a1i	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to \left(i\in \left\{k\right\}\leftrightarrow k=i\right)$$
134	133	ifbid	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to if\left(i\in \left\{k\right\},1,0\right)=if\left(k=i,1,0\right)$$
135	129 134	eqtrd	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to {𝟙}_I\left(\left\{k\right\}\right)\left(i\right)=if\left(k=i,1,0\right)$$
136	135	mpteq2dva	$$⊢\left(\phi \wedge i\in I\right)\to \left(k\in I⟼{𝟙}_I\left(\left\{k\right\}\right)\left(i\right)\right)=\left(k\in I⟼if\left(k=i,1,0\right)\right)$$
137	136	oveq2d	$$⊢\left(\phi \wedge i\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(i\right)=\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}if\left(k=i,1,0\right)$$
138	73 78	mp1i	$$⊢\left(\phi \wedge i\in I\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
139	138	cmnmndd	$$⊢\left(\phi \wedge i\in I\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
140		eqid	$$⊢\left(k\in I⟼if\left(k=i,1,0\right)\right)=\left(k\in I⟼if\left(k=i,1,0\right)\right)$$
141	86	a1i	$$⊢\left(\phi \wedge i\in I\right)\to 1\in {\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
142	72 139 21 118 140 141	gsummptif1n0	$$⊢\left(\phi \wedge i\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}if\left(k=i,1,0\right)=1$$
143	123 137 142	3eqtrd	$$⊢\left(\phi \wedge i\in I\right)\to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)\left(i\right)=1$$
144		ax-1ne0	$$⊢1\ne 0$$
145	144	a1i	$$⊢\left(\phi \wedge i\in I\right)\to 1\ne 0$$
146	143 145	eqnetrd	$$⊢\left(\phi \wedge i\in I\right)\to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)\left(i\right)\ne 0$$
147	117 21 26 118 146	elsuppfnd	$$⊢\left(\phi \wedge i\in I\right)\to i\in {supp}_0\left(\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)\right)$$
148	147	ex	$$⊢\phi \to \left(i\in I\to i\in {supp}_0\left(\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)\right)\right)$$
149	148	ssrdv	$$⊢\phi \to I\subseteq \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)\mathrm{supp}0$$
150	58	mpteq2dva	$$⊢\left(\phi \wedge j\in I\right)\to \left(k\in I⟼\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)=\left(k\in I⟼{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)$$
151	150	oveq2d	$$⊢\left(\phi \wedge j\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)=\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)$$
152	151	mpteq2dva	$$⊢\phi \to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)$$
153	152	oveq1d	$$⊢\phi \to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\mathrm{supp}0=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{𝟙}_I\left(\left\{k\right\}\right)\left(j\right)\right)\mathrm{supp}0$$
154	149 153	sseqtrrd	$$⊢\phi \to I\subseteq \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\mathrm{supp}0$$
155	113 154	eqssd	$$⊢\phi \to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\mathrm{supp}0=I$$
156	155	ad2antrr	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\mathrm{supp}0=I$$
157	96 156	eqtrd	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to u\mathrm{supp}0=I$$
158	157	fveq2d	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to \left|u\mathrm{supp}0\right|=\left|I\right|$$
159	158 6	eqtr4di	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to \left|u\mathrm{supp}0\right|=N$$
160	95 159	jca	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to \left(\mathrm{ran}u\subseteq \left\{0,1\right\}\wedge \left|u\mathrm{supp}0\right|=N\right)$$
161		simpllr	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to \mathrm{ran}u\subseteq \left\{0,1\right\}$$
162	4	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\to I\in \mathrm{Fin}$$
163	19	a1i	$$⊢\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
164		ssrab2	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
165	164	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
166	165	sselda	$$⊢\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to u\in \left({{\mathbb{N}}_0}^I\right)$$
167	166	ad2antrr	$$⊢\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\to u\in \left({{\mathbb{N}}_0}^I\right)$$
168	162 163 167	elmaprd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\to u:I⟶{\mathbb{N}}_0$$
169	168	adantr	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to u:I⟶{\mathbb{N}}_0$$
170	169	ffnd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to uFnI$$
171		simpr	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to j\in I$$
172	170 171	fnfvelrnd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to u\left(j\right)\in \mathrm{ran}u$$
173	161 172	sseldd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to u\left(j\right)\in \left\{0,1\right\}$$
174	162	adantr	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to I\in \mathrm{Fin}$$
175	25	a1i	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to 0\in {\mathbb{N}}_0$$
176		suppssdm	$$⊢u\mathrm{supp}0\subseteq \mathrm{dom}u$$
177	176 169	fssdm	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to u\mathrm{supp}0\subseteq I$$
178		simplr	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to \left|u\mathrm{supp}0\right|=N$$
179	178 6	eqtr2di	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to \left|I\right|=\left|u\mathrm{supp}0\right|$$
180	174 177 179	phphashd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to I=u\mathrm{supp}0$$
181	171 180	eleqtrd	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to j\in {supp}_0\left(u\right)$$
182		elsuppfn	$$⊢\left(uFnI\wedge I\in \mathrm{Fin}\wedge 0\in {\mathbb{N}}_0\right)\to \left(j\in {supp}_0\left(u\right)\leftrightarrow \left(j\in I\wedge u\left(j\right)\ne 0\right)\right)$$
183	182	simplbda	$$⊢\left(\left(uFnI\wedge I\in \mathrm{Fin}\wedge 0\in {\mathbb{N}}_0\right)\wedge j\in {supp}_0\left(u\right)\right)\to u\left(j\right)\ne 0$$
184	170 174 175 181 183	syl31anc	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to u\left(j\right)\ne 0$$
185		elprn1	$$⊢\left(u\left(j\right)\in \left\{0,1\right\}\wedge u\left(j\right)\ne 0\right)\to u\left(j\right)=1$$
186	173 184 185	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\wedge j\in I\right)\to u\left(j\right)=1$$
187	186	mpteq2dva	$$⊢\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\to \left(j\in I⟼u\left(j\right)\right)=\left(j\in I⟼1\right)$$
188	168	feqmptd	$$⊢\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\to u=\left(j\in I⟼u\left(j\right)\right)$$
189	89	mpteq2dva	$$⊢\phi \to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)=\left(j\in I⟼1\right)$$
190	189	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)=\left(j\in I⟼1\right)$$
191	187 188 190	3eqtr4d	$$⊢\left(\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \mathrm{ran}u\subseteq \left\{0,1\right\}\right)\wedge \left|u\mathrm{supp}0\right|=N\right)\to u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)$$
192	191	anasss	$$⊢\left(\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\wedge \left(\mathrm{ran}u\subseteq \left\{0,1\right\}\wedge \left|u\mathrm{supp}0\right|=N\right)\right)\to u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)$$
193	160 192	impbida	$$⊢\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \left(u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\leftrightarrow \left(\mathrm{ran}u\subseteq \left\{0,1\right\}\wedge \left|u\mathrm{supp}0\right|=N\right)\right)$$
194	193	ifbid	$$⊢\left(\phi \wedge u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to if\left(u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right),1_R,0_R\right)=if\left(\left(\mathrm{ran}u\subseteq \left\{0,1\right\}\wedge \left|u\mathrm{supp}0\right|=N\right),1_R,0_R\right)$$
195	194	mpteq2dva	$$⊢\phi \to \left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right),1_R,0_R\right)\right)=\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(\left(\mathrm{ran}u\subseteq \left\{0,1\right\}\wedge \left|u\mathrm{supp}0\right|=N\right),1_R,0_R\right)\right)$$
196		rneq	$$⊢u=f\to \mathrm{ran}u=\mathrm{ran}f$$
197	196	sseq1d	$$⊢u=f\to \left(\mathrm{ran}u\subseteq \left\{0,1\right\}\leftrightarrow \mathrm{ran}f\subseteq \left\{0,1\right\}\right)$$
198		oveq1	$$⊢u=f\to u\mathrm{supp}0=f\mathrm{supp}0$$
199	198	fveqeq2d	$$⊢u=f\to \left(\left|u\mathrm{supp}0\right|=N\leftrightarrow \left|f\mathrm{supp}0\right|=N\right)$$
200	197 199	anbi12d	$$⊢u=f\to \left(\left(\mathrm{ran}u\subseteq \left\{0,1\right\}\wedge \left|u\mathrm{supp}0\right|=N\right)\leftrightarrow \left(\mathrm{ran}f\subseteq \left\{0,1\right\}\wedge \left|f\mathrm{supp}0\right|=N\right)\right)$$
201	200	ifbid	$$⊢u=f\to if\left(\left(\mathrm{ran}u\subseteq \left\{0,1\right\}\wedge \left|u\mathrm{supp}0\right|=N\right),1_R,0_R\right)=if\left(\left(\mathrm{ran}f\subseteq \left\{0,1\right\}\wedge \left|f\mathrm{supp}0\right|=N\right),1_R,0_R\right)$$
202	201	cbvmptv	$$⊢\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(\left(\mathrm{ran}u\subseteq \left\{0,1\right\}\wedge \left|u\mathrm{supp}0\right|=N\right),1_R,0_R\right)\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(\left(\mathrm{ran}f\subseteq \left\{0,1\right\}\wedge \left|f\mathrm{supp}0\right|=N\right),1_R,0_R\right)\right)$$
203	195 202	eqtrdi	$$⊢\phi \to \left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right),1_R,0_R\right)\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(\left(\mathrm{ran}f\subseteq \left\{0,1\right\}\wedge \left|f\mathrm{supp}0\right|=N\right),1_R,0_R\right)\right)$$
204	47 203	sylan9eqr	$$⊢\left(\phi \wedge t=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\to \left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(\left(\mathrm{ran}f\subseteq \left\{0,1\right\}\wedge \left|f\mathrm{supp}0\right|=N\right),1_R,0_R\right)\right)$$
205		breq1	$$⊢h=\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)\right)$$
206	19	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
207	111	fmpttd	$$⊢\phi \to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right):I⟶{\mathbb{N}}_0$$
208	206 4 207	elmapdd	$$⊢\phi \to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\in \left({{\mathbb{N}}_0}^I\right)$$
209	25	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
210	207 4 209	fidmfisupp	$$⊢\phi \to {finSupp}_0\left(\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)$$
211	205 208 210	elrabd	$$⊢\phi \to \left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
212		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
213	212	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
214	213	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
215	214	mptexd	$$⊢\phi \to \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(\left(\mathrm{ran}f\subseteq \left\{0,1\right\}\wedge \left|f\mathrm{supp}0\right|=N\right),1_R,0_R\right)\right)\in \mathrm{V}$$
216	44 204 211 215	fvmptd2	$$⊢\phi \to \left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)\left(\left(j\in I⟼\underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\left(k\right)\left(j\right)\right)\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(\left(\mathrm{ran}f\subseteq \left\{0,1\right\}\wedge \left|f\mathrm{supp}0\right|=N\right),1_R,0_R\right)\right)$$
217	43 216	eqtrd	$$⊢\phi \to {\sum }_M\left(\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)\circ \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(\left(\mathrm{ran}f\subseteq \left\{0,1\right\}\wedge \left|f\mathrm{supp}0\right|=N\right),1_R,0_R\right)\right)$$
218		indval	$$⊢\left(I\in \mathrm{Fin}\wedge \left\{i\right\}\subseteq I\right)\to {𝟙}_I\left(\left\{i\right\}\right)=\left(j\in I⟼if\left(j\in \left\{i\right\},1,0\right)\right)$$
219	4 22 218	syl2an	$$⊢\left(\phi \wedge i\in I\right)\to {𝟙}_I\left(\left\{i\right\}\right)=\left(j\in I⟼if\left(j\in \left\{i\right\},1,0\right)\right)$$
220		velsn	$$⊢j\in \left\{i\right\}\leftrightarrow j=i$$
221	220	a1i	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge j\in I\right)\to \left(j\in \left\{i\right\}\leftrightarrow j=i\right)$$
222	221	ifbid	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge j\in I\right)\to if\left(j\in \left\{i\right\},1,0\right)=if\left(j=i,1,0\right)$$
223	222	mpteq2dva	$$⊢\left(\phi \wedge i\in I\right)\to \left(j\in I⟼if\left(j\in \left\{i\right\},1,0\right)\right)=\left(j\in I⟼if\left(j=i,1,0\right)\right)$$
224	219 223	eqtrd	$$⊢\left(\phi \wedge i\in I\right)\to {𝟙}_I\left(\left\{i\right\}\right)=\left(j\in I⟼if\left(j=i,1,0\right)\right)$$
225	224	eqeq2d	$$⊢\left(\phi \wedge i\in I\right)\to \left(u={𝟙}_I\left(\left\{i\right\}\right)\leftrightarrow u=\left(j\in I⟼if\left(j=i,1,0\right)\right)\right)$$
226	225	ifbid	$$⊢\left(\phi \wedge i\in I\right)\to if\left(u={𝟙}_I\left(\left\{i\right\}\right),1_R,0_R\right)=if\left(u=\left(j\in I⟼if\left(j=i,1,0\right)\right),1_R,0_R\right)$$
227	226	mpteq2dv	$$⊢\left(\phi \wedge i\in I\right)\to \left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u={𝟙}_I\left(\left\{i\right\}\right),1_R,0_R\right)\right)=\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=\left(j\in I⟼if\left(j=i,1,0\right)\right),1_R,0_R\right)\right)$$
228		eqeq1	$$⊢t=u\to \left(t=\left(j\in I⟼if\left(j=i,1,0\right)\right)\leftrightarrow u=\left(j\in I⟼if\left(j=i,1,0\right)\right)\right)$$
229	228	ifbid	$$⊢t=u\to if\left(t=\left(j\in I⟼if\left(j=i,1,0\right)\right),1_R,0_R\right)=if\left(u=\left(j\in I⟼if\left(j=i,1,0\right)\right),1_R,0_R\right)$$
230	229	cbvmptv	$$⊢\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(t=\left(j\in I⟼if\left(j=i,1,0\right)\right),1_R,0_R\right)\right)=\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=\left(j\in I⟼if\left(j=i,1,0\right)\right),1_R,0_R\right)\right)$$
231	227 230	eqtr4di	$$⊢\left(\phi \wedge i\in I\right)\to \left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u={𝟙}_I\left(\left\{i\right\}\right),1_R,0_R\right)\right)=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(t=\left(j\in I⟼if\left(j=i,1,0\right)\right),1_R,0_R\right)\right)$$
232	231	mpteq2dva	$$⊢\phi \to \left(i\in I⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u={𝟙}_I\left(\left\{i\right\}\right),1_R,0_R\right)\right)\right)=\left(i\in I⟼\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(t=\left(j\in I⟼if\left(j=i,1,0\right)\right),1_R,0_R\right)\right)\right)$$
233		eqidd	$$⊢\phi \to \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)=\left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)$$
234		eqidd	$$⊢\phi \to \left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)=\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)$$
235		eqeq2	$$⊢t={𝟙}_I\left(\left\{i\right\}\right)\to \left(u=t\leftrightarrow u={𝟙}_I\left(\left\{i\right\}\right)\right)$$
236	235	ifbid	$$⊢t={𝟙}_I\left(\left\{i\right\}\right)\to if\left(u=t,1_R,0_R\right)=if\left(u={𝟙}_I\left(\left\{i\right\}\right),1_R,0_R\right)$$
237	236	mpteq2dv	$$⊢t={𝟙}_I\left(\left\{i\right\}\right)\to \left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)=\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u={𝟙}_I\left(\left\{i\right\}\right),1_R,0_R\right)\right)$$
238	33 233 234 237	fmptco	$$⊢\phi \to \left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)\circ \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)=\left(i\in I⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u={𝟙}_I\left(\left\{i\right\}\right),1_R,0_R\right)\right)\right)$$
239	9	psrbasfsupp	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
240	2 239 14 15 4 5	mvrfval	$$⊢\phi \to V=\left(i\in I⟼\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(t=\left(j\in I⟼if\left(j=i,1,0\right)\right),1_R,0_R\right)\right)\right)$$
241	232 238 240	3eqtr4d	$$⊢\phi \to \left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)\circ \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)=V$$
242	241	oveq2d	$$⊢\phi \to {\sum }_M\left(\left(t\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\left(u\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(u=t,1_R,0_R\right)\right)\right)\circ \left(i\in I⟼{𝟙}_I\left(\left\{i\right\}\right)\right)\right)={\sum }_{M}V$$
243	16 217 242	3eqtr2d	Could not format ( ph -> ( ( I eSymPoly R ) ` N ) = ( M gsum V ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` N ) = ( M gsum V ) ) with typecode |-
244	8 243	eqtrid	$$⊢\phi \to E\left(N\right)={\sum }_{M}V$$