esplyfval1

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

	Ref	Expression
Hypotheses	esplyfval1.w	$⊢ W = I mPoly R$
	esplyfval1.v	$⊢ V = I mVar R$
	esplyfval1.e	No typesetting found for \|- E = ( I eSymPoly R ) with typecode \|-
	esplyfval1.i	$⊢ φ \to I \in Fin$
	esplyfval1.r	$⊢ φ \to R \in Ring$
Assertion	esplyfval1	$⊢ φ \to E (1) = \sum_{W} V$

Proof

Step	Hyp	Ref	Expression
1		esplyfval1.w	$⊢ W = I mPoly R$
2		esplyfval1.v	$⊢ V = I 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	$⊢ φ \to I \in Fin$
5		esplyfval1.r	$⊢ φ \to R \in Ring$
6		eqid	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
7	6	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
8		eqid	$⊢ 0_{R} = 0_{R}$
9		eqid	$⊢ 1_{R} = 1_{R}$
10	4	ad2antrr	$⊢ ((φ \land i \in I) \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to I \in Fin$
11	5	ad2antrr	$⊢ ((φ \land i \in I) \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to R \in Ring$
12		simplr	$⊢ ((φ \land i \in I) \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to i \in I$
13		simpr	$⊢ ((φ \land i \in I) \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
14	2 7 8 9 10 11 12 13	mvrval2	$⊢ ((φ \land i \in I) \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to V (i) (f) = if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R})$
15	14	ad4ant14	$⊢ ((((φ \land i \in I) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to V (i) (f) = if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R})$
16	15	an52ds	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \to V (i) (f) = if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R})$
17	16	mpteq2dva	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to (i \in I ⟼ V (i) (f)) = (i \in I ⟼ if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R}))$
18	17	oveq2d	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to \underset{i \in I}{\sum_{R}} V (i) (f) = \underset{i \in I}{\sum_{R}} if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R})$
19		nfv	$⊢ Ⅎ j ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I)$
20		nfmpt1	$⊢ \underline{Ⅎ} j (j \in I ⟼ if (j = i, 1, 0))$
21	20	nfeq2	$⊢ Ⅎ j f = (j \in I ⟼ if (j = i, 1, 0))$
22		nfv	$⊢ Ⅎ j i = ⋃ {supp}_{0} (f)$
23	21 22	nfbi	$⊢ Ⅎ j (f = (j \in I ⟼ if (j = i, 1, 0)) \leftrightarrow i = ⋃ {supp}_{0} (f))$
24		unisnv	$⊢ ⋃ \{j\} = j$
25	24	eqeq2i	$⊢ i = ⋃ \{j\} \leftrightarrow i = j$
26	25	a1i	$⊢ ((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to (i = ⋃ \{j\} \leftrightarrow i = j)$
27		simpr	$⊢ (((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to f supp 0 = \{j\}$
28	27	unieqd	$⊢ (((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to ⋃ {supp}_{0} (f) = ⋃ \{j\}$
29	28	adantllr	$⊢ ((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to ⋃ {supp}_{0} (f) = ⋃ \{j\}$
30	29	eqeq2d	$⊢ ((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to (i = ⋃ {supp}_{0} (f) \leftrightarrow i = ⋃ \{j\})$
31		simplr	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land i = j) \to f supp 0 = \{j\}$
32	31	fveq2d	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land i = j) \to 𝟙_{I} (f supp 0) = 𝟙_{I} (\{j\})$
33	4	ad2antrr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to I \in Fin$
34		ssrab2	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
35	34	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
36	35	sselda	$⊢ (φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f \in ({ℕ_{0}}^{I})$
37	36	elmaprd	$⊢ (φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f : I ⟶ ℕ_{0}$
38	37	adantr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to f : I ⟶ ℕ_{0}$
39		ffrn	$⊢ f : I ⟶ ℕ_{0} \to f : I ⟶ ran f$
40	38 39	syl	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to f : I ⟶ ran f$
41		simpr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to ran f \subseteq \{0, 1\}$
42	40 41	fssd	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to f : I ⟶ \{0, 1\}$
43	33 42	indfsid	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to f = 𝟙_{I} (f supp 0)$
44	43	ad5antr	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land i = j) \to f = 𝟙_{I} (f supp 0)$
45		sneq	$⊢ i = j \to \{i\} = \{j\}$
46	45	adantl	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land i = j) \to \{i\} = \{j\}$
47	46	fveq2d	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land i = j) \to 𝟙_{I} (\{i\}) = 𝟙_{I} (\{j\})$
48	32 44 47	3eqtr4d	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land i = j) \to f = 𝟙_{I} (\{i\})$
49		simpr	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land f = 𝟙_{I} (\{i\})) \to f = 𝟙_{I} (\{i\})$
50	49	oveq1d	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land f = 𝟙_{I} (\{i\})) \to f supp 0 = 𝟙_{I} (\{i\}) supp 0$
51		simplr	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land f = 𝟙_{I} (\{i\})) \to f supp 0 = \{j\}$
52	4	ad3antrrr	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to I \in Fin$
53	52	ad4antr	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land f = 𝟙_{I} (\{i\})) \to I \in Fin$
54		snssi	$⊢ i \in I \to \{i\} \subseteq I$
55	54	adantl	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \to \{i\} \subseteq I$
56	55	ad3antrrr	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land f = 𝟙_{I} (\{i\})) \to \{i\} \subseteq I$
57		indsupp	$⊢ (I \in Fin \land \{i\} \subseteq I) \to 𝟙_{I} (\{i\}) supp 0 = \{i\}$
58	53 56 57	syl2anc	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land f = 𝟙_{I} (\{i\})) \to 𝟙_{I} (\{i\}) supp 0 = \{i\}$
59	50 51 58	3eqtr3rd	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land f = 𝟙_{I} (\{i\})) \to \{i\} = \{j\}$
60		vex	$⊢ i \in V$
61	60	sneqr	$⊢ \{i\} = \{j\} \to i = j$
62	59 61	syl	$⊢ (((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \land f = 𝟙_{I} (\{i\})) \to i = j$
63	48 62	impbida	$⊢ ((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to (i = j \leftrightarrow f = 𝟙_{I} (\{i\}))$
64		indsn	$⊢ (I \in Fin \land i \in I) \to 𝟙_{I} (\{i\}) = (j \in I ⟼ if (j = i, 1, 0))$
65	52 64	sylan	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \to 𝟙_{I} (\{i\}) = (j \in I ⟼ if (j = i, 1, 0))$
66	65	ad2antrr	$⊢ ((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to 𝟙_{I} (\{i\}) = (j \in I ⟼ if (j = i, 1, 0))$
67	66	eqeq2d	$⊢ ((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to (f = 𝟙_{I} (\{i\}) \leftrightarrow f = (j \in I ⟼ if (j = i, 1, 0)))$
68	63 67	bitr2d	$⊢ ((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to (f = (j \in I ⟼ if (j = i, 1, 0)) \leftrightarrow i = j)$
69	26 30 68	3bitr4rd	$⊢ ((((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to (f = (j \in I ⟼ if (j = i, 1, 0)) \leftrightarrow i = ⋃ {supp}_{0} (f))$
70		ovexd	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to f supp 0 \in V$
71		simpr	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to \|f supp 0\| = 1$
72		hash1snb	$⊢ f supp 0 \in V \to (\|f supp 0\| = 1 \leftrightarrow \exists j f supp 0 = \{j\})$
73	72	biimpa	$⊢ (f supp 0 \in V \land \|f supp 0\| = 1) \to \exists j f supp 0 = \{j\}$
74	70 71 73	syl2anc	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to \exists j f supp 0 = \{j\}$
75		exsnrex	$⊢ \exists j f supp 0 = \{j\} \leftrightarrow \exists j \in {supp}_{0} (f) f supp 0 = \{j\}$
76	74 75	sylib	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to \exists j \in {supp}_{0} (f) f supp 0 = \{j\}$
77	76	adantr	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \to \exists j \in {supp}_{0} (f) f supp 0 = \{j\}$
78	19 23 69 77	r19.29af2	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \to (f = (j \in I ⟼ if (j = i, 1, 0)) \leftrightarrow i = ⋃ {supp}_{0} (f))$
79	78	ifbid	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land i \in I) \to if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R}) = if (i = ⋃ {supp}_{0} (f), 1_{R}, 0_{R})$
80	79	mpteq2dva	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to (i \in I ⟼ if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R})) = (i \in I ⟼ if (i = ⋃ {supp}_{0} (f), 1_{R}, 0_{R}))$
81	80	oveq2d	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to \underset{i \in I}{\sum_{R}} if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R}) = \underset{i \in I}{\sum_{R}} if (i = ⋃ {supp}_{0} (f), 1_{R}, 0_{R})$
82		ringmnd	$⊢ R \in Ring \to R \in Mnd$
83	5 82	syl	$⊢ φ \to R \in Mnd$
84	83	ad3antrrr	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to R \in Mnd$
85		suppssdm	$⊢ f supp 0 \subseteq dom f$
86	37	fdmd	$⊢ (φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to dom f = I$
87	86	ad4antr	$⊢ (((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to dom f = I$
88	85 87	sseqtrid	$⊢ (((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to f supp 0 \subseteq I$
89		simplr	$⊢ (((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to j \in {supp}_{0} (f)$
90	88 89	sseldd	$⊢ (((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to j \in I$
91	24 90	eqeltrid	$⊢ (((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to ⋃ \{j\} \in I$
92	28 91	eqeltrd	$⊢ (((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \land j \in {supp}_{0} (f)) \land f supp 0 = \{j\}) \to ⋃ {supp}_{0} (f) \in I$
93	92 76	r19.29a	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to ⋃ {supp}_{0} (f) \in I$
94		eqid	$⊢ (i \in I ⟼ if (i = ⋃ {supp}_{0} (f), 1_{R}, 0_{R})) = (i \in I ⟼ if (i = ⋃ {supp}_{0} (f), 1_{R}, 0_{R}))$
95		eqid	$⊢ {Base}_{R} = {Base}_{R}$
96	95 9 5	ringidcld	$⊢ φ \to 1_{R} \in {Base}_{R}$
97	96	ad3antrrr	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to 1_{R} \in {Base}_{R}$
98	8 84 52 93 94 97	gsummptif1n0	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to \underset{i \in I}{\sum_{R}} if (i = ⋃ {supp}_{0} (f), 1_{R}, 0_{R}) = 1_{R}$
99	18 81 98	3eqtrrd	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \land \|f supp 0\| = 1) \to 1_{R} = \underset{i \in I}{\sum_{R}} V (i) (f)$
100	99	anasss	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land (ran f \subseteq \{0, 1\} \land \|f supp 0\| = 1)) \to 1_{R} = \underset{i \in I}{\sum_{R}} V (i) (f)$
101	83	ad2antrr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \to R \in Mnd$
102	4	ad2antrr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \to I \in Fin$
103	8	gsumz	$⊢ (R \in Mnd \land I \in Fin) \to \underset{i \in I}{\sum_{R}} 0_{R} = 0_{R}$
104	101 102 103	syl2anc	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \to \underset{i \in I}{\sum_{R}} 0_{R} = 0_{R}$
105	14	an32s	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \to V (i) (f) = if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R})$
106	105	adantlr	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \land i \in I) \to V (i) (f) = if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R})$
107		simpr	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to f = (j \in I ⟼ if (j = i, 1, 0))$
108	107	rneqd	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to ran f = ran (j \in I ⟼ if (j = i, 1, 0))$
109		nfv	$⊢ Ⅎ j ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I)$
110	109 21	nfan	$⊢ Ⅎ j (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0)))$
111		eqid	$⊢ (j \in I ⟼ if (j = i, 1, 0)) = (j \in I ⟼ if (j = i, 1, 0))$
112		1nn0	$⊢ 1 \in ℕ_{0}$
113		prid2g	$⊢ 1 \in ℕ_{0} \to 1 \in \{0, 1\}$
114	112 113	mp1i	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \land j \in I) \to 1 \in \{0, 1\}$
115		0nn0	$⊢ 0 \in ℕ_{0}$
116		prid1g	$⊢ 0 \in ℕ_{0} \to 0 \in \{0, 1\}$
117	115 116	mp1i	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \land j \in I) \to 0 \in \{0, 1\}$
118	114 117	ifcld	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \land j \in I) \to if (j = i, 1, 0) \in \{0, 1\}$
119	110 111 118	rnmptssd	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to ran (j \in I ⟼ if (j = i, 1, 0)) \subseteq \{0, 1\}$
120	108 119	eqsstrd	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to ran f \subseteq \{0, 1\}$
121	120	adantllr	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to ran f \subseteq \{0, 1\}$
122		simpllr	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to \neg ran f \subseteq \{0, 1\}$
123	121 122	pm2.65da	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \land i \in I) \to \neg f = (j \in I ⟼ if (j = i, 1, 0))$
124	123	iffalsed	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \land i \in I) \to if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R}) = 0_{R}$
125	106 124	eqtr2d	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \land i \in I) \to 0_{R} = V (i) (f)$
126	125	mpteq2dva	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \to (i \in I ⟼ 0_{R}) = (i \in I ⟼ V (i) (f))$
127	126	oveq2d	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \to \underset{i \in I}{\sum_{R}} 0_{R} = \underset{i \in I}{\sum_{R}} V (i) (f)$
128	104 127	eqtr3d	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \to 0_{R} = \underset{i \in I}{\sum_{R}} V (i) (f)$
129	128	adantlr	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg (ran f \subseteq \{0, 1\} \land \|f supp 0\| = 1)) \land \neg ran f \subseteq \{0, 1\}) \to 0_{R} = \underset{i \in I}{\sum_{R}} V (i) (f)$
130	83	ad2antrr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \to R \in Mnd$
131	4	ad2antrr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \to I \in Fin$
132	130 131 103	syl2anc	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \to \underset{i \in I}{\sum_{R}} 0_{R} = 0_{R}$
133	105	adantlr	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \to V (i) (f) = if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R})$
134		simpr	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to f = (j \in I ⟼ if (j = i, 1, 0))$
135	4 64	sylan	$⊢ (φ \land i \in I) \to 𝟙_{I} (\{i\}) = (j \in I ⟼ if (j = i, 1, 0))$
136	135	ad5ant14	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to 𝟙_{I} (\{i\}) = (j \in I ⟼ if (j = i, 1, 0))$
137	134 136	eqtr4d	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to f = 𝟙_{I} (\{i\})$
138	137	oveq1d	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to f supp 0 = 𝟙_{I} (\{i\}) supp 0$
139	131	ad2antrr	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to I \in Fin$
140	54	ad2antlr	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to \{i\} \subseteq I$
141	139 140 57	syl2anc	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to 𝟙_{I} (\{i\}) supp 0 = \{i\}$
142	138 141	eqtrd	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to f supp 0 = \{i\}$
143	142	fveq2d	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to \|f supp 0\| = \|\{i\}\|$
144		hashsng	$⊢ i \in I \to \|\{i\}\| = 1$
145	144	ad2antlr	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to \|\{i\}\| = 1$
146	143 145	eqtrd	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to \|f supp 0\| = 1$
147		simpllr	$⊢ ((((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \land f = (j \in I ⟼ if (j = i, 1, 0))) \to \neg \|f supp 0\| = 1$
148	146 147	pm2.65da	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \to \neg f = (j \in I ⟼ if (j = i, 1, 0))$
149	148	iffalsed	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \to if (f = (j \in I ⟼ if (j = i, 1, 0)), 1_{R}, 0_{R}) = 0_{R}$
150	133 149	eqtr2d	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \land i \in I) \to 0_{R} = V (i) (f)$
151	150	mpteq2dva	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \to (i \in I ⟼ 0_{R}) = (i \in I ⟼ V (i) (f))$
152	151	oveq2d	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \to \underset{i \in I}{\sum_{R}} 0_{R} = \underset{i \in I}{\sum_{R}} V (i) (f)$
153	132 152	eqtr3d	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \to 0_{R} = \underset{i \in I}{\sum_{R}} V (i) (f)$
154	153	adantlr	$⊢ (((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg (ran f \subseteq \{0, 1\} \land \|f supp 0\| = 1)) \land \neg \|f supp 0\| = 1) \to 0_{R} = \underset{i \in I}{\sum_{R}} V (i) (f)$
155		pm3.13	$⊢ \neg (ran f \subseteq \{0, 1\} \land \|f supp 0\| = 1) \to (\neg ran f \subseteq \{0, 1\} \lor \neg \|f supp 0\| = 1)$
156	155	adantl	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg (ran f \subseteq \{0, 1\} \land \|f supp 0\| = 1)) \to (\neg ran f \subseteq \{0, 1\} \lor \neg \|f supp 0\| = 1)$
157	129 154 156	mpjaodan	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg (ran f \subseteq \{0, 1\} \land \|f supp 0\| = 1)) \to 0_{R} = \underset{i \in I}{\sum_{R}} V (i) (f)$
158	100 157	ifeqda	$⊢ (φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = 1), 1_{R}, 0_{R}) = \underset{i \in I}{\sum_{R}} V (i) (f)$
159	158	mpteq2dva	$⊢ φ \to (f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = 1), 1_{R}, 0_{R})) = (f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ \underset{i \in I}{\sum_{R}} V (i) (f))$
160	3	fveq1i	Could not format ( E ` 1 ) = ( ( I eSymPoly R ) ` 1 ) : No typesetting found for \|- ( E ` 1 ) = ( ( I eSymPoly R ) ` 1 ) with typecode \|-
161	112	a1i	$⊢ φ \to 1 \in ℕ_{0}$
162	6 4 5 161 8 9	esplyfval3	Could not format ( ph -> ( ( I eSymPoly R ) ` 1 ) = ( f e. { h e. ( NN0 ^m I ) \| h finSupp 0 } \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` 1 ) = ( f e. { h e. ( NN0 ^m I ) \| h finSupp 0 } \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) with typecode \|-
163	160 162	eqtrid	$⊢ φ \to E (1) = (f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = 1), 1_{R}, 0_{R}))$
164		eqid	$⊢ {Base}_{W} = {Base}_{W}$
165	1 2 164 4 5	mvrf2	$⊢ φ \to V : I ⟶ {Base}_{W}$
166	1 164 5 4 6 4 165	mplgsum	$⊢ φ \to \sum_{W} V = (f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ \underset{i \in I}{\sum_{R}} V (i) (f))$
167	159 163 166	3eqtr4d	$⊢ φ \to E (1) = \sum_{W} V$

Metamath Proof Explorer

Theorem esplyfval1

Proof