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		1ex	$$⊢1\in \mathrm{V}$$
91	90	prid2	$$⊢1\in \left\{0,1\right\}$$
92	89 91	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\}$$
93	92	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\}$$
94	50 51 93	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\}$$
95	94	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\}$$
96	49 95	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\}$$
97	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$$
98		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)$$
99		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
100	99	a1i	$$⊢\left(\phi \wedge j\in I\right)\to {\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
101	25	a1i	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to 0\in {\mathbb{N}}_0$$
102	27	a1i	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to 1\in {\mathbb{N}}_0$$
103	101 102	prssd	$$⊢\left(\left(\phi \wedge j\in I\right)\wedge k\in I\right)\to \left\{0,1\right\}\subseteq {\mathbb{N}}_0$$
104		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\}$$
105	59 60 104	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\}$$
106	105 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\}$$
107	103 106	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$$
108	58 107	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$$
109	108	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$$
110	25	a1i	$$⊢\left(\phi \wedge j\in I\right)\to 0\in {\mathbb{N}}_0$$
111	109 81 110	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)$$
112	72 79 81 100 109 111	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$$
113	51 112	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$$
114	98 113	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$$
115		nfv	$$⊢Ⅎj\left(\phi \wedge i\in I\right)$$
116		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}$$
117		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)$$
118	115 116 117	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$$
119		simpr	$$⊢\left(\phi \wedge i\in I\right)\to i\in I$$
120		fveq2	$$⊢j=i\to {𝟙}_I\left(\left\{k\right\}\right)\left(j\right)={𝟙}_I\left(\left\{k\right\}\right)\left(i\right)$$
121	120	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)$$
122	121	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)$$
123		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}$$
124	117 122 119 123	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)$$
125	4	ad2antrr	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to I\in \mathrm{Fin}$$
126		simpr	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to k\in I$$
127	126	snssd	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to \left\{k\right\}\subseteq I$$
128		simplr	$$⊢\left(\left(\phi \wedge i\in I\right)\wedge k\in I\right)\to i\in I$$
129		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)$$
130	125 127 128 129	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)$$
131		velsn	$$⊢i\in \left\{k\right\}\leftrightarrow i=k$$
132		equcom	$$⊢i=k\leftrightarrow k=i$$
133	131 132	bitri	$$⊢i\in \left\{k\right\}\leftrightarrow k=i$$
134	133	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)$$
135	134	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)$$
136	130 135	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)$$
137	136	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)$$
138	137	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)$$
139	73 78	mp1i	$$⊢\left(\phi \wedge i\in I\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
140	139	cmnmndd	$$⊢\left(\phi \wedge i\in I\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
141		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)$$
142	86	a1i	$$⊢\left(\phi \wedge i\in I\right)\to 1\in {\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
143	72 140 21 119 141 142	gsummptif1n0	$$⊢\left(\phi \wedge i\in I\right)\to \underset{k\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}}}if\left(k=i,1,0\right)=1$$
144	124 138 143	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$$
145		ax-1ne0	$$⊢1\ne 0$$
146	145	a1i	$$⊢\left(\phi \wedge i\in I\right)\to 1\ne 0$$
147	144 146	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$$
148	118 21 26 119 147	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)$$
149	148	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)$$
150	149	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$$
151	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)$$
152	151	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)$$
153	152	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)$$
154	153	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$$
155	150 154	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$$
156	114 155	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$$
157	156	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$$
158	97 157	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$$
159	158	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|$$
160	159 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$$
161	96 160	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)$$
162		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\}$$
163	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}$$
164	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}$$
165		ssrab2	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
166	165	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
167	166	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)$$
168	167	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)$$
169	163 164 168	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$$
170	169	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$$
171	170	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$$
172		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$$
173	171 172	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$$
174	162 173	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\}$$
175	163	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}$$
176	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$$
177		suppssdm	$$⊢u\mathrm{supp}0\subseteq \mathrm{dom}u$$
178	177 170	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$$
179		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$$
180	179 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|$$
181	175 178 180	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$$
182	172 181	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)$$
183		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)$$
184	183	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$$
185	171 175 176 182 184	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$$
186		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$$
187	174 185 186	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$$
188	187	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)$$
189	169	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)$$
190	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)$$
191	190	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)$$
192	188 189 191	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)$$
193	192	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)$$
194	161 193	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)$$
195	194	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)$$
196	195	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)$$
197		rneq	$$⊢u=f\to \mathrm{ran}u=\mathrm{ran}f$$
198	197	sseq1d	$$⊢u=f\to \left(\mathrm{ran}u\subseteq \left\{0,1\right\}\leftrightarrow \mathrm{ran}f\subseteq \left\{0,1\right\}\right)$$
199		oveq1	$$⊢u=f\to u\mathrm{supp}0=f\mathrm{supp}0$$
200	199	fveqeq2d	$$⊢u=f\to \left(\left|u\mathrm{supp}0\right|=N\leftrightarrow \left|f\mathrm{supp}0\right|=N\right)$$
201	198 200	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)$$
202	201	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)$$
203	202	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)$$
204	196 203	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)$$
205	47 204	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)$$
206		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)$$
207	19	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
208	112	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$$
209	207 4 208	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)$$
210	25	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
211	208 4 210	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)$$
212	206 209 211	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\}$$
213		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
214	213	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
215	214	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
216	215	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}$$
217	44 205 212 216	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)$$
218	43 217	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)$$
219		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)$$
220	4 22 219	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)$$
221		velsn	$$⊢j\in \left\{i\right\}\leftrightarrow j=i$$
222	221	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)$$
223	222	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)$$
224	223	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)$$
225	220 224	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)$$
226	225	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)$$
227	226	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)$$
228	227	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)$$
229		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)$$
230	229	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)$$
231	230	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)$$
232	228 231	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)$$
233	232	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)$$
234		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)$$
235		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)$$
236		eqeq2	$$⊢t={𝟙}_I\left(\left\{i\right\}\right)\to \left(u=t\leftrightarrow u={𝟙}_I\left(\left\{i\right\}\right)\right)$$
237	236	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)$$
238	237	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)$$
239	33 234 235 238	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)$$
240	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\}$$
241	2 240 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)$$
242	233 239 241	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$$
243	242	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$$
244	16 218 243	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 |-
245	8 244	eqtrid	$$⊢\phi \to E\left(N\right)={\sum }_{M}V$$