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		ssrab2	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
163	162	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\subseteq {{\mathbb{N}}_0}^I$$
164	163	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)$$
165	164	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)$$
166	165	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$$
167	166	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$$
168	167	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$$
169		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$$
170	168 169	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$$
171	161 170	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\}$$
172	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}$$
173	172	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}$$
174	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$$
175		suppssdm	$$⊢u\mathrm{supp}0\subseteq \mathrm{dom}u$$
176	175 167	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$$
177		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$$
178	177 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|$$
179	173 176 178	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$$
180	169 179	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)$$
181		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)$$
182	181	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$$
183	168 173 174 180 182	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$$
184		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$$
185	171 183 184	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$$
186	185	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)$$
187	166	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)$$
188	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)$$
189	188	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)$$
190	186 187 189	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)$$
191	190	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)$$
192	160 191	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)$$
193	192	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)$$
194	193	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)$$
195		rneq	$$⊢u=f\to \mathrm{ran}u=\mathrm{ran}f$$
196	195	sseq1d	$$⊢u=f\to \left(\mathrm{ran}u\subseteq \left\{0,1\right\}\leftrightarrow \mathrm{ran}f\subseteq \left\{0,1\right\}\right)$$
197		oveq1	$$⊢u=f\to u\mathrm{supp}0=f\mathrm{supp}0$$
198	197	fveqeq2d	$$⊢u=f\to \left(\left|u\mathrm{supp}0\right|=N\leftrightarrow \left|f\mathrm{supp}0\right|=N\right)$$
199	196 198	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)$$
200	199	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)$$
201	200	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)$$
202	194 201	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)$$
203	47 202	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)$$
204		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)$$
205	19	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
206	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$$
207	205 4 206	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)$$
208	25	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
209	206 4 208	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)$$
210	204 207 209	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\}$$
211		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
212	211	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
213	212	a1i	$$⊢\phi \to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
214	213	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}$$
215	44 203 210 214	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)$$
216	43 215	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)$$
217		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)$$
218	4 22 217	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)$$
219		velsn	$$⊢j\in \left\{i\right\}\leftrightarrow j=i$$
220	219	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)$$
221	220	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)$$
222	221	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)$$
223	218 222	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)$$
224	223	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)$$
225	224	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)$$
226	225	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)$$
227		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)$$
228	227	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)$$
229	228	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)$$
230	226 229	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)$$
231	230	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)$$
232		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)$$
233		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)$$
234		eqeq2	$$⊢t={𝟙}_I\left(\left\{i\right\}\right)\to \left(u=t\leftrightarrow u={𝟙}_I\left(\left\{i\right\}\right)\right)$$
235	234	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)$$
236	235	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)$$
237	33 232 233 236	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)$$
238	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\}$$
239	2 238 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)$$
240	231 237 239	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$$
241	240	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$$
242	16 216 241	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 |-
243	8 242	eqtrid	$$⊢\phi \to E\left(N\right)={\sum }_{M}V$$