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	4	adantr	$⊢ (φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to I \in Fin$
35		nn0ex	$⊢ ℕ_{0} \in V$
36	35	a1i	$⊢ (φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to ℕ_{0} \in V$
37		ssrab2	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
38	37	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
39	38	sselda	$⊢ (φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f \in ({ℕ_{0}}^{I})$
40	34 36 39	elmaprd	$⊢ (φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f : I ⟶ ℕ_{0}$
41	40	adantr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to f : I ⟶ ℕ_{0}$
42		ffrn	$⊢ f : I ⟶ ℕ_{0} \to f : I ⟶ ran f$
43	41 42	syl	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to f : I ⟶ ran f$
44		simpr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to ran f \subseteq \{0, 1\}$
45	43 44	fssd	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to f : I ⟶ \{0, 1\}$
46	33 45	indfsid	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land ran f \subseteq \{0, 1\}) \to f = 𝟙_{I} (f supp 0)$
47	46	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)$
48		sneq	$⊢ i = j \to \{i\} = \{j\}$
49	48	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\}$
50	49	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\})$
51	32 47 50	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\})$
52		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\})$
53	52	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$
54		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\}$
55	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$
56	55	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$
57		snssi	$⊢ i \in I \to \{i\} \subseteq I$
58	57	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$
59	58	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$
60		indsupp	$⊢ (I \in Fin \land \{i\} \subseteq I) \to 𝟙_{I} (\{i\}) supp 0 = \{i\}$
61	56 59 60	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\}$
62	53 54 61	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\}$
63		vex	$⊢ i \in V$
64	63	sneqr	$⊢ \{i\} = \{j\} \to i = j$
65	62 64	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$
66	51 65	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\}))$
67		indsn	$⊢ (I \in Fin \land i \in I) \to 𝟙_{I} (\{i\}) = (j \in I ⟼ if (j = i, 1, 0))$
68	55 67	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))$
69	68	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))$
70	69	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)))$
71	66 70	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)$
72	26 30 71	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))$
73		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$
74		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$
75		hash1snb	$⊢ f supp 0 \in V \to (\|f supp 0\| = 1 \leftrightarrow \exists j f supp 0 = \{j\})$
76	75	biimpa	$⊢ (f supp 0 \in V \land \|f supp 0\| = 1) \to \exists j f supp 0 = \{j\}$
77	73 74 76	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\}$
78		exsnrex	$⊢ \exists j f supp 0 = \{j\} \leftrightarrow \exists j \in {supp}_{0} (f) f supp 0 = \{j\}$
79	77 78	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\}$
80	79	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\}$
81	19 23 72 80	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))$
82	81	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})$
83	82	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}))$
84	83	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})$
85		ringmnd	$⊢ R \in Ring \to R \in Mnd$
86	5 85	syl	$⊢ φ \to R \in Mnd$
87	86	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$
88		suppssdm	$⊢ f supp 0 \subseteq dom f$
89	40	fdmd	$⊢ (φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to dom f = I$
90	89	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$
91	88 90	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$
92		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)$
93	91 92	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$
94	24 93	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$
95	28 94	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$
96	95 79	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$
97		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}))$
98		eqid	$⊢ {Base}_{R} = {Base}_{R}$
99	98 9 5	ringidcld	$⊢ φ \to 1_{R} \in {Base}_{R}$
100	99	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}$
101	8 87 55 96 97 100	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}$
102	18 84 101	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)$
103	102	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)$
104	86	ad2antrr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \to R \in Mnd$
105	4	ad2antrr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg ran f \subseteq \{0, 1\}) \to I \in Fin$
106	8	gsumz	$⊢ (R \in Mnd \land I \in Fin) \to \underset{i \in I}{\sum_{R}} 0_{R} = 0_{R}$
107	104 105 106	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}$
108	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})$
109	108	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})$
110		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))$
111	110	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))$
112		nfv	$⊢ Ⅎ j ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I)$
113	112 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)))$
114		eqid	$⊢ (j \in I ⟼ if (j = i, 1, 0)) = (j \in I ⟼ if (j = i, 1, 0))$
115		1nn0	$⊢ 1 \in ℕ_{0}$
116		prid2g	$⊢ 1 \in ℕ_{0} \to 1 \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 1 \in \{0, 1\}$
118		0nn0	$⊢ 0 \in ℕ_{0}$
119		prid1g	$⊢ 0 \in ℕ_{0} \to 0 \in \{0, 1\}$
120	118 119	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\}$
121	117 120	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\}$
122	113 114 121	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\}$
123	111 122	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\}$
124	123	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\}$
125		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\}$
126	124 125	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))$
127	126	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}$
128	109 127	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)$
129	128	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))$
130	129	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)$
131	107 130	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)$
132	131	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)$
133	86	ad2antrr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \to R \in Mnd$
134	4	ad2antrr	$⊢ ((φ \land f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land \neg \|f supp 0\| = 1) \to I \in Fin$
135	133 134 106	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}$
136	108	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})$
137		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))$
138	4 67	sylan	$⊢ (φ \land i \in I) \to 𝟙_{I} (\{i\}) = (j \in I ⟼ if (j = i, 1, 0))$
139	138	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))$
140	137 139	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\})$
141	140	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$
142	134	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$
143	57	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$
144	142 143 60	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\}$
145	141 144	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\}$
146	145	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\}\|$
147		hashsng	$⊢ i \in I \to \|\{i\}\| = 1$
148	147	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$
149	146 148	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$
150		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$
151	149 150	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))$
152	151	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}$
153	136 152	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)$
154	153	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))$
155	154	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)$
156	135 155	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)$
157	156	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)$
158		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)$
159	158	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)$
160	132 157 159	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)$
161	103 160	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)$
162	161	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))$
163	3	fveq1i	Could not format ( E ` 1 ) = ( ( I eSymPoly R ) ` 1 ) : No typesetting found for \|- ( E ` 1 ) = ( ( I eSymPoly R ) ` 1 ) with typecode \|-
164	115	a1i	$⊢ φ \to 1 \in ℕ_{0}$
165	6 4 5 164 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 \|-
166	163 165	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}))$
167		eqid	$⊢ {Base}_{W} = {Base}_{W}$
168	1 2 167 4 5	mvrf2	$⊢ φ \to V : I ⟶ {Base}_{W}$
169	1 167 5 4 6 4 168	mplgsum	$⊢ φ \to \sum_{W} V = (f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ \underset{i \in I}{\sum_{R}} V (i) (f))$
170	162 166 169	3eqtr4d	$⊢ φ \to E (1) = \sum_{W} V$

Metamath Proof Explorer

Theorem esplyfval1

Proof