esplyind

Description: A recursive formula for the elementary symmetric polynomials. (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Hypotheses	esplyind.w	$⊢ W = I mPoly R$
	esplyind.v	$⊢ V = I mVar R$
	esplyind.p	$⊢ \underset{˙}{+} = +_{W}$
	esplyind.m	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	esplyind.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
	esplyind.g	No typesetting found for \|- G = ( ( I extendVars R ) ` Y ) with typecode \|-
	esplyind.i	$⊢ φ \to I \in Fin$
	esplyind.r	$⊢ φ \to R \in Ring$
	esplyind.y	$⊢ φ \to Y \in I$
	esplyind.j	$⊢ J = I ∖ \{Y\}$
	esplyind.e	No typesetting found for \|- E = ( J eSymPoly R ) with typecode \|-
	esplyind.k	$⊢ φ \to K \in (1 \dots \|I\|)$
	esplyind.1	$⊢ C = \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
Assertion	esplyind	Could not format assertion : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) .+ ( G ` ( E ` K ) ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		esplyind.w	$⊢ W = I mPoly R$
2		esplyind.v	$⊢ V = I mVar R$
3		esplyind.p	$⊢ \underset{˙}{+} = +_{W}$
4		esplyind.m	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		esplyind.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
6		esplyind.g	Could not format G = ( ( I extendVars R ) ` Y ) : No typesetting found for \|- G = ( ( I extendVars R ) ` Y ) with typecode \|-
7		esplyind.i	$⊢ φ \to I \in Fin$
8		esplyind.r	$⊢ φ \to R \in Ring$
9		esplyind.y	$⊢ φ \to Y \in I$
10		esplyind.j	$⊢ J = I ∖ \{Y\}$
11		esplyind.e	Could not format E = ( J eSymPoly R ) : No typesetting found for \|- E = ( J eSymPoly R ) with typecode \|-
12		esplyind.k	$⊢ φ \to K \in (1 \dots \|I\|)$
13		esplyind.1	$⊢ C = \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
14		ovif12	$⊢ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\}))) +_{R} if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R}) = if (f (Y) = 0, 0_{R} +_{R} if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})) +_{R} 0_{R})$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16		eqid	$⊢ +_{R} = +_{R}$
17		eqid	$⊢ 0_{R} = 0_{R}$
18	8	ringgrpd	$⊢ φ \to R \in Grp$
19	18	ad2antrr	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to R \in Grp$
20		eqid	$⊢ 1_{R} = 1_{R}$
21	15 20 8	ringidcld	$⊢ φ \to 1_{R} \in {Base}_{R}$
22	21	adantr	$⊢ (φ \land f \in D) \to 1_{R} \in {Base}_{R}$
23		ringgrp	$⊢ R \in Ring \to R \in Grp$
24	15 17	grpidcl	$⊢ R \in Grp \to 0_{R} \in {Base}_{R}$
25	8 23 24	3syl	$⊢ φ \to 0_{R} \in {Base}_{R}$
26	25	adantr	$⊢ (φ \land f \in D) \to 0_{R} \in {Base}_{R}$
27	22 26	ifcld	$⊢ (φ \land f \in D) \to if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}) \in {Base}_{R}$
28	27	adantr	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}) \in {Base}_{R}$
29	15 16 17 19 28	grplidd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to 0_{R} +_{R} if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}) = if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R})$
30		snsspr1	$⊢ \{0\} \subseteq \{0, 1\}$
31	30	biantru	$⊢ ran ({f ↾}_{J}) \subseteq \{0, 1\} \leftrightarrow (ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \{0\} \subseteq \{0, 1\})$
32		unss	$⊢ (ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \{0\} \subseteq \{0, 1\}) \leftrightarrow ran ({f ↾}_{J}) \cup \{0\} \subseteq \{0, 1\}$
33	31 32	bitri	$⊢ ran ({f ↾}_{J}) \subseteq \{0, 1\} \leftrightarrow ran ({f ↾}_{J}) \cup \{0\} \subseteq \{0, 1\}$
34	7	adantr	$⊢ (φ \land f \in D) \to I \in Fin$
35		nn0ex	$⊢ ℕ_{0} \in V$
36	35	a1i	$⊢ (φ \land f \in D) \to ℕ_{0} \in V$
37	5	ssrab3	$⊢ D \subseteq {ℕ_{0}}^{I}$
38	37	a1i	$⊢ φ \to D \subseteq {ℕ_{0}}^{I}$
39	38	sselda	$⊢ (φ \land f \in D) \to f \in ({ℕ_{0}}^{I})$
40	34 36 39	elmaprd	$⊢ (φ \land f \in D) \to f : I ⟶ ℕ_{0}$
41	40	freld	$⊢ (φ \land f \in D) \to Rel f$
42	40	ffnd	$⊢ (φ \land f \in D) \to f Fn I$
43	42	fndmd	$⊢ (φ \land f \in D) \to dom f = I$
44	10	uneq1i	$⊢ J \cup \{Y\} = (I ∖ \{Y\}) \cup \{Y\}$
45	9	snssd	$⊢ φ \to \{Y\} \subseteq I$
46		undifr	$⊢ \{Y\} \subseteq I \leftrightarrow (I ∖ \{Y\}) \cup \{Y\} = I$
47	45 46	sylib	$⊢ φ \to (I ∖ \{Y\}) \cup \{Y\} = I$
48	44 47	eqtr2id	$⊢ φ \to I = J \cup \{Y\}$
49	48	adantr	$⊢ (φ \land f \in D) \to I = J \cup \{Y\}$
50	43 49	eqtrd	$⊢ (φ \land f \in D) \to dom f = J \cup \{Y\}$
51	10	ineq1i	$⊢ J \cap \{Y\} = (I ∖ \{Y\}) \cap \{Y\}$
52		disjdifr	$⊢ (I ∖ \{Y\}) \cap \{Y\} = \emptyset$
53	51 52	eqtri	$⊢ J \cap \{Y\} = \emptyset$
54	53	a1i	$⊢ (φ \land f \in D) \to J \cap \{Y\} = \emptyset$
55		reldisjun	$⊢ (Rel f \land dom f = J \cup \{Y\} \land J \cap \{Y\} = \emptyset) \to f = ({f ↾}_{J}) \cup ({f ↾}_{\{Y\}})$
56	41 50 54 55	syl3anc	$⊢ (φ \land f \in D) \to f = ({f ↾}_{J}) \cup ({f ↾}_{\{Y\}})$
57	56	rneqd	$⊢ (φ \land f \in D) \to ran f = ran (({f ↾}_{J}) \cup ({f ↾}_{\{Y\}}))$
58		rnun	$⊢ ran (({f ↾}_{J}) \cup ({f ↾}_{\{Y\}})) = ran ({f ↾}_{J}) \cup ran ({f ↾}_{\{Y\}})$
59	57 58	eqtr2di	$⊢ (φ \land f \in D) \to ran ({f ↾}_{J}) \cup ran ({f ↾}_{\{Y\}}) = ran f$
60	42	fnfund	$⊢ (φ \land f \in D) \to Fun f$
61	9	adantr	$⊢ (φ \land f \in D) \to Y \in I$
62	61 43	eleqtrrd	$⊢ (φ \land f \in D) \to Y \in dom f$
63		rnressnsn	$⊢ (Fun f \land Y \in dom f) \to ran ({f ↾}_{\{Y\}}) = \{f (Y)\}$
64	60 62 63	syl2anc	$⊢ (φ \land f \in D) \to ran ({f ↾}_{\{Y\}}) = \{f (Y)\}$
65	64	uneq2d	$⊢ (φ \land f \in D) \to ran ({f ↾}_{J}) \cup ran ({f ↾}_{\{Y\}}) = ran ({f ↾}_{J}) \cup \{f (Y)\}$
66	59 65	eqtr3d	$⊢ (φ \land f \in D) \to ran f = ran ({f ↾}_{J}) \cup \{f (Y)\}$
67	66	adantr	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to ran f = ran ({f ↾}_{J}) \cup \{f (Y)\}$
68		simpr	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to f (Y) = 0$
69	68	sneqd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to \{f (Y)\} = \{0\}$
70	69	uneq2d	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to ran ({f ↾}_{J}) \cup \{f (Y)\} = ran ({f ↾}_{J}) \cup \{0\}$
71	67 70	eqtrd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to ran f = ran ({f ↾}_{J}) \cup \{0\}$
72	71	sseq1d	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to (ran f \subseteq \{0, 1\} \leftrightarrow ran ({f ↾}_{J}) \cup \{0\} \subseteq \{0, 1\})$
73	33 72	bitr4id	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to (ran ({f ↾}_{J}) \subseteq \{0, 1\} \leftrightarrow ran f \subseteq \{0, 1\})$
74	56	oveq1d	$⊢ (φ \land f \in D) \to f supp 0 = (({f ↾}_{J}) \cup ({f ↾}_{\{Y\}})) supp 0$
75	39	resexd	$⊢ (φ \land f \in D) \to {f ↾}_{J} \in V$
76	39	resexd	$⊢ (φ \land f \in D) \to {f ↾}_{\{Y\}} \in V$
77		0nn0	$⊢ 0 \in ℕ_{0}$
78	77	a1i	$⊢ (φ \land f \in D) \to 0 \in ℕ_{0}$
79	75 76 78	suppun2	$⊢ (φ \land f \in D) \to (({f ↾}_{J}) \cup ({f ↾}_{\{Y\}})) supp 0 = {supp}_{0} (({f ↾}_{J})) \cup {supp}_{0} (({f ↾}_{\{Y\}}))$
80	74 79	eqtrd	$⊢ (φ \land f \in D) \to f supp 0 = {supp}_{0} (({f ↾}_{J})) \cup {supp}_{0} (({f ↾}_{\{Y\}}))$
81	80	adantr	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to f supp 0 = {supp}_{0} (({f ↾}_{J})) \cup {supp}_{0} (({f ↾}_{\{Y\}}))$
82		fnressn	$⊢ (f Fn I \land Y \in I) \to {f ↾}_{\{Y\}} = \{⟨Y, f (Y)⟩\}$
83	42 61 82	syl2anc	$⊢ (φ \land f \in D) \to {f ↾}_{\{Y\}} = \{⟨Y, f (Y)⟩\}$
84	83	oveq1d	$⊢ (φ \land f \in D) \to ({f ↾}_{\{Y\}}) supp 0 = \{⟨Y, f (Y)⟩\} supp 0$
85	40 61	ffvelcdmd	$⊢ (φ \land f \in D) \to f (Y) \in ℕ_{0}$
86		eqid	$⊢ \{⟨Y, f (Y)⟩\} = \{⟨Y, f (Y)⟩\}$
87	86	suppsnop	$⊢ (Y \in I \land f (Y) \in ℕ_{0} \land 0 \in ℕ_{0}) \to \{⟨Y, f (Y)⟩\} supp 0 = if (f (Y) = 0, \emptyset, \{Y\})$
88	61 85 78 87	syl3anc	$⊢ (φ \land f \in D) \to \{⟨Y, f (Y)⟩\} supp 0 = if (f (Y) = 0, \emptyset, \{Y\})$
89	84 88	eqtrd	$⊢ (φ \land f \in D) \to ({f ↾}_{\{Y\}}) supp 0 = if (f (Y) = 0, \emptyset, \{Y\})$
90	89	adantr	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to ({f ↾}_{\{Y\}}) supp 0 = if (f (Y) = 0, \emptyset, \{Y\})$
91	68	iftrued	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to if (f (Y) = 0, \emptyset, \{Y\}) = \emptyset$
92	90 91	eqtrd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to ({f ↾}_{\{Y\}}) supp 0 = \emptyset$
93	92	uneq2d	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to {supp}_{0} (({f ↾}_{J})) \cup {supp}_{0} (({f ↾}_{\{Y\}})) = {supp}_{0} (({f ↾}_{J})) \cup \emptyset$
94		un0	$⊢ {supp}_{0} (({f ↾}_{J})) \cup \emptyset = ({f ↾}_{J}) supp 0$
95	93 94	eqtrdi	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to {supp}_{0} (({f ↾}_{J})) \cup {supp}_{0} (({f ↾}_{\{Y\}})) = ({f ↾}_{J}) supp 0$
96	81 95	eqtr2d	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to ({f ↾}_{J}) supp 0 = f supp 0$
97	96	fveqeq2d	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to (\|({f ↾}_{J}) supp 0\| = K \leftrightarrow \|f supp 0\| = K)$
98	73 97	anbi12d	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K) \leftrightarrow (ran f \subseteq \{0, 1\} \land \|f supp 0\| = K))$
99	98	ifbid	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}) = if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R})$
100	29 99	eqtrd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to 0_{R} +_{R} if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}) = if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R})$
101	18	ad2antrr	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to R \in Grp$
102		eqid	$⊢ {Base}_{W} = {Base}_{W}$
103	5	psrbasfsupp	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
104	6	fveq1i	Could not format ( G ` ( E ` ( K - 1 ) ) ) = ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) : No typesetting found for \|- ( G ` ( E ` ( K - 1 ) ) ) = ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) with typecode \|-
105		eqid	$⊢ {Base}_{(J mPoly R)} = {Base}_{(J mPoly R)}$
106	1	fveq2i	$⊢ {Base}_{W} = {Base}_{(I mPoly R)}$
107	5 17 7 8 15 10 105 9 106	extvfvalf	Could not format ( ph -> ( ( I extendVars R ) ` Y ) : ( Base ` ( J mPoly R ) ) --> ( Base ` W ) ) : No typesetting found for \|- ( ph -> ( ( I extendVars R ) ` Y ) : ( Base ` ( J mPoly R ) ) --> ( Base ` W ) ) with typecode \|-
108	11	fveq1i	Could not format ( E ` ( K - 1 ) ) = ( ( J eSymPoly R ) ` ( K - 1 ) ) : No typesetting found for \|- ( E ` ( K - 1 ) ) = ( ( J eSymPoly R ) ` ( K - 1 ) ) with typecode \|-
109		difssd	$⊢ φ \to I ∖ \{Y\} \subseteq I$
110	10 109	eqsstrid	$⊢ φ \to J \subseteq I$
111	7 110	ssfid	$⊢ φ \to J \in Fin$
112		elfznn	$⊢ K \in (1 \dots \|I\|) \to K \in ℕ$
113		nnm1nn0	$⊢ K \in ℕ \to K - 1 \in ℕ_{0}$
114	12 112 113	3syl	$⊢ φ \to K - 1 \in ℕ_{0}$
115	13 111 8 114 105	esplympl	Could not format ( ph -> ( ( J eSymPoly R ) ` ( K - 1 ) ) e. ( Base ` ( J mPoly R ) ) ) : No typesetting found for \|- ( ph -> ( ( J eSymPoly R ) ` ( K - 1 ) ) e. ( Base ` ( J mPoly R ) ) ) with typecode \|-
116	108 115	eqeltrid	$⊢ φ \to E (K - 1) \in {Base}_{(J mPoly R)}$
117	107 116	ffvelcdmd	Could not format ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) e. ( Base ` W ) ) : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) e. ( Base ` W ) ) with typecode \|-
118	104 117	eqeltrid	$⊢ φ \to G (E (K - 1)) \in {Base}_{W}$
119	1 15 102 103 118	mplelf	$⊢ φ \to G (E (K - 1)) : D ⟶ {Base}_{R}$
120	119	ad2antrr	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to G (E (K - 1)) : D ⟶ {Base}_{R}$
121		simplr	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to f \in D$
122		indf	$⊢ (I \in Fin \land \{Y\} \subseteq I) \to 𝟙_{I} (\{Y\}) : I ⟶ \{0, 1\}$
123	7 45 122	syl2anc	$⊢ φ \to 𝟙_{I} (\{Y\}) : I ⟶ \{0, 1\}$
124	77	a1i	$⊢ φ \to 0 \in ℕ_{0}$
125		1nn0	$⊢ 1 \in ℕ_{0}$
126	125	a1i	$⊢ φ \to 1 \in ℕ_{0}$
127	124 126	prssd	$⊢ φ \to \{0, 1\} \subseteq ℕ_{0}$
128	123 127	fssd	$⊢ φ \to 𝟙_{I} (\{Y\}) : I ⟶ ℕ_{0}$
129	128	ad2antrr	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to 𝟙_{I} (\{Y\}) : I ⟶ ℕ_{0}$
130	7	ad2antrr	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to I \in Fin$
131	130	ad2antrr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to I \in Fin$
132	45	ad4antr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to \{Y\} \subseteq I$
133		simpr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to x = Y$
134		velsn	$⊢ x \in \{Y\} \leftrightarrow x = Y$
135	133 134	sylibr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to x \in \{Y\}$
136		ind1	$⊢ (I \in Fin \land \{Y\} \subseteq I \land x \in \{Y\}) \to 𝟙_{I} (\{Y\}) (x) = 1$
137	131 132 135 136	syl3anc	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to 𝟙_{I} (\{Y\}) (x) = 1$
138	40	ad3antrrr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to f : I ⟶ ℕ_{0}$
139		simplr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to x \in I$
140	138 139	ffvelcdmd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to f (x) \in ℕ_{0}$
141	133	fveq2d	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to f (x) = f (Y)$
142		simpllr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to \neg f (Y) = 0$
143	142	neqned	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to f (Y) \neq 0$
144	141 143	eqnetrd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to f (x) \neq 0$
145		elnnne0	$⊢ f (x) \in ℕ \leftrightarrow (f (x) \in ℕ_{0} \land f (x) \neq 0)$
146	140 144 145	sylanbrc	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to f (x) \in ℕ$
147	146	nnge1d	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to 1 \leq f (x)$
148	137 147	eqbrtrd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x = Y) \to 𝟙_{I} (\{Y\}) (x) \leq f (x)$
149	130	ad2antrr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x \neq Y) \to I \in Fin$
150	45	ad4antr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x \neq Y) \to \{Y\} \subseteq I$
151		simplr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x \neq Y) \to x \in I$
152		simpr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x \neq Y) \to x \neq Y$
153	151 152	eldifsnd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x \neq Y) \to x \in (I ∖ \{Y\})$
154		ind0	$⊢ (I \in Fin \land \{Y\} \subseteq I \land x \in (I ∖ \{Y\})) \to 𝟙_{I} (\{Y\}) (x) = 0$
155	149 150 153 154	syl3anc	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x \neq Y) \to 𝟙_{I} (\{Y\}) (x) = 0$
156	40	adantr	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to f : I ⟶ ℕ_{0}$
157	156	ffvelcdmda	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \to f (x) \in ℕ_{0}$
158	157	adantr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x \neq Y) \to f (x) \in ℕ_{0}$
159	158	nn0ge0d	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x \neq Y) \to 0 \leq f (x)$
160	155 159	eqbrtrd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \land x \neq Y) \to 𝟙_{I} (\{Y\}) (x) \leq f (x)$
161	148 160	pm2.61dane	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \to 𝟙_{I} (\{Y\}) (x) \leq f (x)$
162	161	ralrimiva	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to \forall x \in I 𝟙_{I} (\{Y\}) (x) \leq f (x)$
163	129	ffnd	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to 𝟙_{I} (\{Y\}) Fn I$
164	42	adantr	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to f Fn I$
165		inidm	$⊢ I \cap I = I$
166		eqidd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \to 𝟙_{I} (\{Y\}) (x) = 𝟙_{I} (\{Y\}) (x)$
167		eqidd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land x \in I) \to f (x) = f (x)$
168	163 164 130 130 165 166 167	ofrfval	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to (𝟙_{I} (\{Y\}) \leq_{f} f \leftrightarrow \forall x \in I 𝟙_{I} (\{Y\}) (x) \leq f (x))$
169	162 168	mpbird	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to 𝟙_{I} (\{Y\}) \leq_{f} f$
170	103	psrbagcon	$⊢ (f \in D \land 𝟙_{I} (\{Y\}) : I ⟶ ℕ_{0} \land 𝟙_{I} (\{Y\}) \leq_{f} f) \to (f -_{f} 𝟙_{I} (\{Y\}) \in D \land (f -_{f} 𝟙_{I} (\{Y\})) \leq_{f} f)$
171	170	simpld	$⊢ (f \in D \land 𝟙_{I} (\{Y\}) : I ⟶ ℕ_{0} \land 𝟙_{I} (\{Y\}) \leq_{f} f) \to f -_{f} 𝟙_{I} (\{Y\}) \in D$
172	121 129 169 171	syl3anc	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to f -_{f} 𝟙_{I} (\{Y\}) \in D$
173	120 172	ffvelcdmd	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})) \in {Base}_{R}$
174	15 16 17 101 173	grpridd	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})) +_{R} 0_{R} = G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\}))$
175	104	fveq1i	Could not format ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) = ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) : No typesetting found for \|- ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) = ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) with typecode \|-
176	175	a1i	Could not format ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) = ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) = ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) with typecode \|-
177	8	ad2antrr	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to R \in Ring$
178	9	ad2antrr	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to Y \in I$
179	116	ad2antrr	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to E (K - 1) \in {Base}_{(J mPoly R)}$
180	5 17 130 177 178 10 105 179 172	extvfvv	Could not format ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) = if ( ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 , ( ( E ` ( K - 1 ) ) ` ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) \|` J ) ) , ( 0g ` R ) ) ) : No typesetting found for \|- ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) = if ( ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 , ( ( E ` ( K - 1 ) ) ` ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) \|` J ) ) , ( 0g ` R ) ) ) with typecode \|-
181	13 111 8 114 17 20	esplyfval3	Could not format ( ph -> ( ( J eSymPoly R ) ` ( K - 1 ) ) = ( z e. C \|-> if ( ( ran z C_ { 0 , 1 } /\ ( # ` ( z supp 0 ) ) = ( K - 1 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) : No typesetting found for \|- ( ph -> ( ( J eSymPoly R ) ` ( K - 1 ) ) = ( z e. C \|-> if ( ( ran z C_ { 0 , 1 } /\ ( # ` ( z supp 0 ) ) = ( K - 1 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) with typecode \|-
182	108 181	eqtrid	$⊢ φ \to E (K - 1) = (z \in C ⟼ if ((ran z \subseteq \{0, 1\} \land \|z supp 0\| = K - 1), 1_{R}, 0_{R}))$
183	182	ad3antrrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to E (K - 1) = (z \in C ⟼ if ((ran z \subseteq \{0, 1\} \land \|z supp 0\| = K - 1), 1_{R}, 0_{R}))$
184	59	ad4antr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to ran ({f ↾}_{J}) \cup ran ({f ↾}_{\{Y\}}) = ran f$
185		simpr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}$
186	123	ffnd	$⊢ φ \to 𝟙_{I} (\{Y\}) Fn I$
187	186	adantr	$⊢ (φ \land f \in D) \to 𝟙_{I} (\{Y\}) Fn I$
188	42 187 34 34 165	offn	$⊢ (φ \land f \in D) \to (f -_{f} 𝟙_{I} (\{Y\})) Fn I$
189	188	ad3antrrr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to (f -_{f} 𝟙_{I} (\{Y\})) Fn I$
190	110	ad4antr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to J \subseteq I$
191	189 190	fnssresd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to ({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) Fn J$
192		fneq1	$⊢ z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J} \to (z Fn J \leftrightarrow ({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) Fn J)$
193	192	biimpar	$⊢ (z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J} \land ({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) Fn J) \to z Fn J$
194	185 191 193	syl2anc	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to z Fn J$
195	42	ad2antrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f Fn I$
196	110	ad3antrrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to J \subseteq I$
197	195 196	fnssresd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to ({f ↾}_{J}) Fn J$
198	197	adantr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to ({f ↾}_{J}) Fn J$
199		simplr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}$
200	199	fveq1d	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to z (x) = ({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) (x)$
201		simpr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to x \in J$
202	201	fvresd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to ({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) (x) = (f -_{f} 𝟙_{I} (\{Y\})) (x)$
203	195	ad2antrr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to f Fn I$
204	163	adantr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to 𝟙_{I} (\{Y\}) Fn I$
205	204	ad2antrr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to 𝟙_{I} (\{Y\}) Fn I$
206	34	ad2antrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to I \in Fin$
207	206	ad2antrr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to I \in Fin$
208	190	sselda	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to x \in I$
209		fnfvof	$⊢ ((f Fn I \land 𝟙_{I} (\{Y\}) Fn I) \land (I \in Fin \land x \in I)) \to (f -_{f} 𝟙_{I} (\{Y\})) (x) = f (x) - 𝟙_{I} (\{Y\}) (x)$
210	203 205 207 208 209	syl22anc	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to (f -_{f} 𝟙_{I} (\{Y\})) (x) = f (x) - 𝟙_{I} (\{Y\}) (x)$
211	45	ad5antr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to \{Y\} \subseteq I$
212	201 10	eleqtrdi	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to x \in (I ∖ \{Y\})$
213	207 211 212 154	syl3anc	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to 𝟙_{I} (\{Y\}) (x) = 0$
214	213	oveq2d	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to f (x) - 𝟙_{I} (\{Y\}) (x) = f (x) - 0$
215	156	ad3antrrr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to f : I ⟶ ℕ_{0}$
216	215 208	ffvelcdmd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to f (x) \in ℕ_{0}$
217	216	nn0cnd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to f (x) \in ℂ$
218	217	subid1d	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to f (x) - 0 = f (x)$
219	201	fvresd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to ({f ↾}_{J}) (x) = f (x)$
220	218 219	eqtr4d	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to f (x) - 0 = ({f ↾}_{J}) (x)$
221	210 214 220	3eqtrd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to (f -_{f} 𝟙_{I} (\{Y\})) (x) = ({f ↾}_{J}) (x)$
222	200 202 221	3eqtrd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land x \in J) \to z (x) = ({f ↾}_{J}) (x)$
223	194 198 222	eqfnfvd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to z = {f ↾}_{J}$
224	223	rneqd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to ran z = ran ({f ↾}_{J})$
225	224	adantr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to ran z = ran ({f ↾}_{J})$
226		simpr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to ran z \subseteq \{0, 1\}$
227	225 226	eqsstrrd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to ran ({f ↾}_{J}) \subseteq \{0, 1\}$
228	60	ad4antr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to Fun f$
229	62	ad4antr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to Y \in dom f$
230	228 229 63	syl2anc	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to ran ({f ↾}_{\{Y\}}) = \{f (Y)\}$
231	85	ad2antrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f (Y) \in ℕ_{0}$
232	231	nn0cnd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f (Y) \in ℂ$
233	123 9	ffvelcdmd	$⊢ φ \to 𝟙_{I} (\{Y\}) (Y) \in \{0, 1\}$
234	127 233	sseldd	$⊢ φ \to 𝟙_{I} (\{Y\}) (Y) \in ℕ_{0}$
235	234	nn0cnd	$⊢ φ \to 𝟙_{I} (\{Y\}) (Y) \in ℂ$
236	235	ad3antrrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to 𝟙_{I} (\{Y\}) (Y) \in ℂ$
237	178	adantr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to Y \in I$
238		fnfvof	$⊢ ((f Fn I \land 𝟙_{I} (\{Y\}) Fn I) \land (I \in Fin \land Y \in I)) \to (f -_{f} 𝟙_{I} (\{Y\})) (Y) = f (Y) - 𝟙_{I} (\{Y\}) (Y)$
239	195 204 206 237 238	syl22anc	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to (f -_{f} 𝟙_{I} (\{Y\})) (Y) = f (Y) - 𝟙_{I} (\{Y\}) (Y)$
240		simpr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0$
241	239 240	eqtr3d	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f (Y) - 𝟙_{I} (\{Y\}) (Y) = 0$
242	232 236 241	subeq0d	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f (Y) = 𝟙_{I} (\{Y\}) (Y)$
243		snidg	$⊢ Y \in I \to Y \in \{Y\}$
244	9 243	syl	$⊢ φ \to Y \in \{Y\}$
245		ind1	$⊢ (I \in Fin \land \{Y\} \subseteq I \land Y \in \{Y\}) \to 𝟙_{I} (\{Y\}) (Y) = 1$
246	7 45 244 245	syl3anc	$⊢ φ \to 𝟙_{I} (\{Y\}) (Y) = 1$
247	246	ad3antrrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to 𝟙_{I} (\{Y\}) (Y) = 1$
248	242 247	eqtrd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f (Y) = 1$
249	248	ad2antrr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to f (Y) = 1$
250	249	sneqd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to \{f (Y)\} = \{1\}$
251	230 250	eqtrd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to ran ({f ↾}_{\{Y\}}) = \{1\}$
252		snsspr2	$⊢ \{1\} \subseteq \{0, 1\}$
253	251 252	eqsstrdi	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to ran ({f ↾}_{\{Y\}}) \subseteq \{0, 1\}$
254	227 253	unssd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to ran ({f ↾}_{J}) \cup ran ({f ↾}_{\{Y\}}) \subseteq \{0, 1\}$
255	184 254	eqsstrrd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran z \subseteq \{0, 1\}) \to ran f \subseteq \{0, 1\}$
256	223	adantr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran f \subseteq \{0, 1\}) \to z = {f ↾}_{J}$
257	256	rneqd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran f \subseteq \{0, 1\}) \to ran z = ran ({f ↾}_{J})$
258		rnresss	$⊢ ran ({f ↾}_{J}) \subseteq ran f$
259		simpr	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran f \subseteq \{0, 1\}) \to ran f \subseteq \{0, 1\}$
260	258 259	sstrid	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran f \subseteq \{0, 1\}) \to ran ({f ↾}_{J}) \subseteq \{0, 1\}$
261	257 260	eqsstrd	$⊢ (((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \land ran f \subseteq \{0, 1\}) \to ran z \subseteq \{0, 1\}$
262	255 261	impbida	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to (ran z \subseteq \{0, 1\} \leftrightarrow ran f \subseteq \{0, 1\})$
263	223	oveq1d	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to z supp 0 = ({f ↾}_{J}) supp 0$
264	263	fveqeq2d	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to (\|z supp 0\| = K - 1 \leftrightarrow \|({f ↾}_{J}) supp 0\| = K - 1)$
265	262 264	anbi12d	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to ((ran z \subseteq \{0, 1\} \land \|z supp 0\| = K - 1) \leftrightarrow (ran f \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K - 1))$
266	265	ifbid	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land z = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) \to if ((ran z \subseteq \{0, 1\} \land \|z supp 0\| = K - 1), 1_{R}, 0_{R}) = if ((ran f \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K - 1), 1_{R}, 0_{R})$
267		breq1	$⊢ h = {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J})))$
268	35	a1i	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to ℕ_{0} \in V$
269	206 196	ssexd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to J \in V$
270	37 172	sselid	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to f -_{f} 𝟙_{I} (\{Y\}) \in ({ℕ_{0}}^{I})$
271	270	adantr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f -_{f} 𝟙_{I} (\{Y\}) \in ({ℕ_{0}}^{I})$
272	206 268 271	elmaprd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to (f -_{f} 𝟙_{I} (\{Y\})) : I ⟶ ℕ_{0}$
273	272 196	fssresd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to ({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) : J ⟶ ℕ_{0}$
274	268 269 273	elmapdd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J} \in ({ℕ_{0}}^{J})$
275		breq1	$⊢ h = f -_{f} 𝟙_{I} (\{Y\}) \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} ((f -_{f} 𝟙_{I} (\{Y\}))))$
276	172	adantr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f -_{f} 𝟙_{I} (\{Y\}) \in D$
277	276 5	eleqtrdi	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f -_{f} 𝟙_{I} (\{Y\}) \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
278	275 277	elrabrd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to {finSupp}_{0} ((f -_{f} 𝟙_{I} (\{Y\})))$
279	77	a1i	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to 0 \in ℕ_{0}$
280	278 279	fsuppres	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to {finSupp}_{0} (({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}))$
281	267 274 280	elrabd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J} \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
282	281 13	eleqtrrdi	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to {(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J} \in C$
283	22	ad2antrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to 1_{R} \in {Base}_{R}$
284	26	ad2antrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to 0_{R} \in {Base}_{R}$
285	283 284	ifcld	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to if ((ran f \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K - 1), 1_{R}, 0_{R}) \in {Base}_{R}$
286	183 266 282 285	fvmptd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to E (K - 1) ({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) = if ((ran f \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K - 1), 1_{R}, 0_{R})$
287		eqcom	$⊢ K - 1 = \|({f ↾}_{J}) supp 0\| \leftrightarrow \|({f ↾}_{J}) supp 0\| = K - 1$
288		fz1ssfz0	$⊢ (1 \dots \|I\|) \subseteq (0 \dots \|I\|)$
289		fz0ssnn0	$⊢ (0 \dots \|I\|) \subseteq ℕ_{0}$
290	288 289	sstri	$⊢ (1 \dots \|I\|) \subseteq ℕ_{0}$
291	290 12	sselid	$⊢ φ \to K \in ℕ_{0}$
292	291	nn0cnd	$⊢ φ \to K \in ℂ$
293	292	ad3antrrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to K \in ℂ$
294		1cnd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to 1 \in ℂ$
295		c0ex	$⊢ 0 \in V$
296	295	a1i	$⊢ (φ \land f \in D) \to 0 \in V$
297	40 34 296	fidmfisupp	$⊢ (φ \land f \in D) \to {finSupp}_{0} (f)$
298	297 296	fsuppres	$⊢ (φ \land f \in D) \to {finSupp}_{0} (({f ↾}_{J}))$
299	298	ad2antrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to {finSupp}_{0} (({f ↾}_{J}))$
300	299	fsuppimpd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to ({f ↾}_{J}) supp 0 \in Fin$
301		hashcl	$⊢ ({f ↾}_{J}) supp 0 \in Fin \to \|({f ↾}_{J}) supp 0\| \in ℕ_{0}$
302	300 301	syl	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to \|({f ↾}_{J}) supp 0\| \in ℕ_{0}$
303	302	nn0cnd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to \|({f ↾}_{J}) supp 0\| \in ℂ$
304	293 294 303	subadd2d	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to (K - 1 = \|({f ↾}_{J}) supp 0\| \leftrightarrow \|({f ↾}_{J}) supp 0\| + 1 = K)$
305	287 304	bitr3id	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to (\|({f ↾}_{J}) supp 0\| = K - 1 \leftrightarrow \|({f ↾}_{J}) supp 0\| + 1 = K)$
306	80	ad2antrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f supp 0 = {supp}_{0} (({f ↾}_{J})) \cup {supp}_{0} (({f ↾}_{\{Y\}}))$
307	89	ad2antrr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to ({f ↾}_{\{Y\}}) supp 0 = if (f (Y) = 0, \emptyset, \{Y\})$
308		simplr	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to \neg f (Y) = 0$
309	308	iffalsed	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to if (f (Y) = 0, \emptyset, \{Y\}) = \{Y\}$
310	307 309	eqtrd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to ({f ↾}_{\{Y\}}) supp 0 = \{Y\}$
311	310	uneq2d	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to {supp}_{0} (({f ↾}_{J})) \cup {supp}_{0} (({f ↾}_{\{Y\}})) = {supp}_{0} (({f ↾}_{J})) \cup \{Y\}$
312	306 311	eqtrd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to f supp 0 = {supp}_{0} (({f ↾}_{J})) \cup \{Y\}$
313	312	fveq2d	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to \|f supp 0\| = \|{supp}_{0} (({f ↾}_{J})) \cup \{Y\}\|$
314		suppssdm	$⊢ ({f ↾}_{J}) supp 0 \subseteq dom ({f ↾}_{J})$
315		resdmss	$⊢ dom ({f ↾}_{J}) \subseteq J$
316	314 315	sstri	$⊢ ({f ↾}_{J}) supp 0 \subseteq J$
317	316	a1i	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to ({f ↾}_{J}) supp 0 \subseteq J$
318	10	eqimssi	$⊢ J \subseteq I ∖ \{Y\}$
319		ssdifsn	$⊢ J \subseteq I ∖ \{Y\} \leftrightarrow (J \subseteq I \land \neg Y \in J)$
320	318 319	mpbi	$⊢ (J \subseteq I \land \neg Y \in J)$
321	320	simpri	$⊢ \neg Y \in J$
322	321	a1i	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to \neg Y \in J$
323	317 322	ssneldd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to \neg Y \in {supp}_{0} (({f ↾}_{J}))$
324		hashunsng	$⊢ Y \in I \to ((({f ↾}_{J}) supp 0 \in Fin \land \neg Y \in {supp}_{0} (({f ↾}_{J}))) \to \|{supp}_{0} (({f ↾}_{J})) \cup \{Y\}\| = \|({f ↾}_{J}) supp 0\| + 1)$
325	324	imp	$⊢ (Y \in I \land (({f ↾}_{J}) supp 0 \in Fin \land \neg Y \in {supp}_{0} (({f ↾}_{J})))) \to \|{supp}_{0} (({f ↾}_{J})) \cup \{Y\}\| = \|({f ↾}_{J}) supp 0\| + 1$
326	237 300 323 325	syl12anc	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to \|{supp}_{0} (({f ↾}_{J})) \cup \{Y\}\| = \|({f ↾}_{J}) supp 0\| + 1$
327	313 326	eqtrd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to \|f supp 0\| = \|({f ↾}_{J}) supp 0\| + 1$
328	327	eqeq1d	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to (\|f supp 0\| = K \leftrightarrow \|({f ↾}_{J}) supp 0\| + 1 = K)$
329	305 328	bitr4d	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to (\|({f ↾}_{J}) supp 0\| = K - 1 \leftrightarrow \|f supp 0\| = K)$
330	329	anbi2d	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to ((ran f \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K - 1) \leftrightarrow (ran f \subseteq \{0, 1\} \land \|f supp 0\| = K))$
331	330	ifbid	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to if ((ran f \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K - 1), 1_{R}, 0_{R}) = if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R})$
332	286 331	eqtrd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to E (K - 1) ({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}) = if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R})$
333		simpr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to ran f \subseteq \{0, 1\}$
334	164	ad2antrr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to f Fn I$
335	178	ad2antrr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to Y \in I$
336	334 335	fnfvelrnd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to f (Y) \in ran f$
337	333 336	sseldd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to f (Y) \in \{0, 1\}$
338		simpllr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to \neg f (Y) = 0$
339	338	neqned	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to f (Y) \neq 0$
340	85	nn0cnd	$⊢ (φ \land f \in D) \to f (Y) \in ℂ$
341	340	ad3antrrr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to f (Y) \in ℂ$
342		1cnd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to 1 \in ℂ$
343		simplr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0$
344	163	ad2antrr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to 𝟙_{I} (\{Y\}) Fn I$
345	130	ad2antrr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to I \in Fin$
346	334 344 345 335 238	syl22anc	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to (f -_{f} 𝟙_{I} (\{Y\})) (Y) = f (Y) - 𝟙_{I} (\{Y\}) (Y)$
347	246	ad4antr	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to 𝟙_{I} (\{Y\}) (Y) = 1$
348	347	oveq2d	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to f (Y) - 𝟙_{I} (\{Y\}) (Y) = f (Y) - 1$
349	346 348	eqtrd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to (f -_{f} 𝟙_{I} (\{Y\})) (Y) = f (Y) - 1$
350	349	eqeq1d	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to ((f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0 \leftrightarrow f (Y) - 1 = 0)$
351	343 350	mtbid	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to \neg f (Y) - 1 = 0$
352		subeq0	$⊢ (f (Y) \in ℂ \land 1 \in ℂ) \to (f (Y) - 1 = 0 \leftrightarrow f (Y) = 1)$
353	352	notbid	$⊢ (f (Y) \in ℂ \land 1 \in ℂ) \to (\neg f (Y) - 1 = 0 \leftrightarrow \neg f (Y) = 1)$
354	353	biimpa	$⊢ ((f (Y) \in ℂ \land 1 \in ℂ) \land \neg f (Y) - 1 = 0) \to \neg f (Y) = 1$
355	341 342 351 354	syl21anc	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to \neg f (Y) = 1$
356	355	neqned	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to f (Y) \neq 1$
357	339 356	nelprd	$⊢ ((((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \land ran f \subseteq \{0, 1\}) \to \neg f (Y) \in \{0, 1\}$
358	337 357	pm2.65da	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to \neg ran f \subseteq \{0, 1\}$
359	358	intnanrd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to \neg (ran f \subseteq \{0, 1\} \land \|f supp 0\| = K)$
360	359	iffalsed	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R}) = 0_{R}$
361	360	eqcomd	$⊢ (((φ \land f \in D) \land \neg f (Y) = 0) \land \neg (f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0) \to 0_{R} = if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R})$
362	332 361	ifeqda	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to if ((f -_{f} 𝟙_{I} (\{Y\})) (Y) = 0, E (K - 1) ({(f -_{f} 𝟙_{I} (\{Y\})) ↾}_{J}), 0_{R}) = if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R})$
363	176 180 362	3eqtrd	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})) = if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R})$
364	174 363	eqtrd	$⊢ ((φ \land f \in D) \land \neg f (Y) = 0) \to G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})) +_{R} 0_{R} = if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R})$
365	100 364	ifeqda	$⊢ (φ \land f \in D) \to if (f (Y) = 0, 0_{R} +_{R} if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})) +_{R} 0_{R}) = if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R})$
366	14 365	eqtrid	$⊢ (φ \land f \in D) \to if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\}))) +_{R} if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R}) = if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R})$
367	366	mpteq2dva	$⊢ φ \to (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\}))) +_{R} if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R})) = (f \in D ⟼ if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), 1_{R}, 0_{R}))$
368	1 7 8	mplringd	$⊢ φ \to W \in Ring$
369	1 2 102 7 8 9	mvrcl	$⊢ φ \to V (Y) \in {Base}_{W}$
370	102 4 368 369 118	ringcld	$⊢ φ \to V (Y) \underset{˙}{\cdot} G (E (K - 1)) \in {Base}_{W}$
371	6	fveq1i	Could not format ( G ` ( E ` K ) ) = ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) : No typesetting found for \|- ( G ` ( E ` K ) ) = ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) with typecode \|-
372	11	fveq1i	Could not format ( E ` K ) = ( ( J eSymPoly R ) ` K ) : No typesetting found for \|- ( E ` K ) = ( ( J eSymPoly R ) ` K ) with typecode \|-
373	13 111 8 291 105	esplympl	Could not format ( ph -> ( ( J eSymPoly R ) ` K ) e. ( Base ` ( J mPoly R ) ) ) : No typesetting found for \|- ( ph -> ( ( J eSymPoly R ) ` K ) e. ( Base ` ( J mPoly R ) ) ) with typecode \|-
374	372 373	eqeltrid	$⊢ φ \to E (K) \in {Base}_{(J mPoly R)}$
375	107 374	ffvelcdmd	Could not format ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) e. ( Base ` W ) ) : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) e. ( Base ` W ) ) with typecode \|-
376	371 375	eqeltrid	$⊢ φ \to G (E (K)) \in {Base}_{W}$
377	1 102 16 3 370 376	mpladd	$⊢ φ \to (V (Y) \underset{˙}{\cdot} G (E (K - 1))) \underset{˙}{+} G (E (K)) = (V (Y) \underset{˙}{\cdot} G (E (K - 1))) {+_{R}}_{f} G (E (K))$
378	2	fveq1i	$⊢ V (Y) = (I mVar R) (Y)$
379		eqid	$⊢ 𝟙_{I} (\{Y\}) = 𝟙_{I} (\{Y\})$
380	1 378 102 4 17 5 379 7 9 8 118	mplmulmvr	$⊢ φ \to V (Y) \underset{˙}{\cdot} G (E (K - 1)) = (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\}))))$
381	6	a1i	Could not format ( ph -> G = ( ( I extendVars R ) ` Y ) ) : No typesetting found for \|- ( ph -> G = ( ( I extendVars R ) ` Y ) ) with typecode \|-
382	13 111 8 291 17 20	esplyfval3	Could not format ( ph -> ( ( J eSymPoly R ) ` K ) = ( g e. C \|-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) : No typesetting found for \|- ( ph -> ( ( J eSymPoly R ) ` K ) = ( g e. C \|-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) with typecode \|-
383	372 382	eqtrid	$⊢ φ \to E (K) = (g \in C ⟼ if ((ran g \subseteq \{0, 1\} \land \|g supp 0\| = K), 1_{R}, 0_{R}))$
384	381 383	fveq12d	Could not format ( ph -> ( G ` ( E ` K ) ) = ( ( ( I extendVars R ) ` Y ) ` ( g e. C \|-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) : No typesetting found for \|- ( ph -> ( G ` ( E ` K ) ) = ( ( ( I extendVars R ) ` Y ) ` ( g e. C \|-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) with typecode \|-
385	382 373	eqeltrrd	$⊢ φ \to (g \in C ⟼ if ((ran g \subseteq \{0, 1\} \land \|g supp 0\| = K), 1_{R}, 0_{R})) \in {Base}_{(J mPoly R)}$
386	5 17 7 8 9 10 105 385	extvfv	Could not format ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( g e. C \|-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( f e. D \|-> if ( ( f ` Y ) = 0 , ( ( g e. C \|-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ` ( f \|` J ) ) , ( 0g ` R ) ) ) ) : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( g e. C \|-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( f e. D \|-> if ( ( f ` Y ) = 0 , ( ( g e. C \|-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ` ( f \|` J ) ) , ( 0g ` R ) ) ) ) with typecode \|-
387		rneq	$⊢ g = {f ↾}_{J} \to ran g = ran ({f ↾}_{J})$
388	387	sseq1d	$⊢ g = {f ↾}_{J} \to (ran g \subseteq \{0, 1\} \leftrightarrow ran ({f ↾}_{J}) \subseteq \{0, 1\})$
389		oveq1	$⊢ g = {f ↾}_{J} \to g supp 0 = ({f ↾}_{J}) supp 0$
390	389	fveqeq2d	$⊢ g = {f ↾}_{J} \to (\|g supp 0\| = K \leftrightarrow \|({f ↾}_{J}) supp 0\| = K)$
391	388 390	anbi12d	$⊢ g = {f ↾}_{J} \to ((ran g \subseteq \{0, 1\} \land \|g supp 0\| = K) \leftrightarrow (ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K))$
392	391	ifbid	$⊢ g = {f ↾}_{J} \to if ((ran g \subseteq \{0, 1\} \land \|g supp 0\| = K), 1_{R}, 0_{R}) = if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R})$
393		eqidd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to (g \in C ⟼ if ((ran g \subseteq \{0, 1\} \land \|g supp 0\| = K), 1_{R}, 0_{R})) = (g \in C ⟼ if ((ran g \subseteq \{0, 1\} \land \|g supp 0\| = K), 1_{R}, 0_{R}))$
394		breq1	$⊢ h = {f ↾}_{J} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (({f ↾}_{J})))$
395	35	a1i	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to ℕ_{0} \in V$
396	111	ad2antrr	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to J \in Fin$
397	40	adantr	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to f : I ⟶ ℕ_{0}$
398	110	ad2antrr	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to J \subseteq I$
399	397 398	fssresd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to ({f ↾}_{J}) : J ⟶ ℕ_{0}$
400	395 396 399	elmapdd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to {f ↾}_{J} \in ({ℕ_{0}}^{J})$
401	298	adantr	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to {finSupp}_{0} (({f ↾}_{J}))$
402	394 400 401	elrabd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to {f ↾}_{J} \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
403	402 13	eleqtrrdi	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to {f ↾}_{J} \in C$
404		fvexd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to 1_{R} \in V$
405		fvexd	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to 0_{R} \in V$
406	404 405	ifcld	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}) \in V$
407	392 393 403 406	fvmptd4	$⊢ ((φ \land f \in D) \land f (Y) = 0) \to (g \in C ⟼ if ((ran g \subseteq \{0, 1\} \land \|g supp 0\| = K), 1_{R}, 0_{R})) ({f ↾}_{J}) = if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R})$
408	407	ifeq1da	$⊢ (φ \land f \in D) \to if (f (Y) = 0, (g \in C ⟼ if ((ran g \subseteq \{0, 1\} \land \|g supp 0\| = K), 1_{R}, 0_{R})) ({f ↾}_{J}), 0_{R}) = if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R})$
409	408	mpteq2dva	$⊢ φ \to (f \in D ⟼ if (f (Y) = 0, (g \in C ⟼ if ((ran g \subseteq \{0, 1\} \land \|g supp 0\| = K), 1_{R}, 0_{R})) ({f ↾}_{J}), 0_{R})) = (f \in D ⟼ if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R}))$
410	384 386 409	3eqtrd	$⊢ φ \to G (E (K)) = (f \in D ⟼ if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R}))$
411	380 410	oveq12d	$⊢ φ \to (V (Y) \underset{˙}{\cdot} G (E (K - 1))) {+_{R}}_{f} G (E (K)) = (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})))) {+_{R}}_{f} (f \in D ⟼ if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R}))$
412		ovex	$⊢ {ℕ_{0}}^{I} \in V$
413	5 412	rabex2	$⊢ D \in V$
414	413	a1i	$⊢ φ \to D \in V$
415		nfv	$⊢ Ⅎ f φ$
416		fvexd	$⊢ (φ \land f \in D) \to G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})) \in V$
417	26 416	ifexd	$⊢ (φ \land f \in D) \to if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\}))) \in V$
418		eqid	$⊢ (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})))) = (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\}))))$
419	415 417 418	fnmptd	$⊢ φ \to (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})))) Fn D$
420	27 26	ifcld	$⊢ (φ \land f \in D) \to if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R}) \in {Base}_{R}$
421		eqid	$⊢ (f \in D ⟼ if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R})) = (f \in D ⟼ if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R}))$
422	415 420 421	fnmptd	$⊢ φ \to (f \in D ⟼ if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R})) Fn D$
423		ofmpteq	$⊢ (D \in V \land (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})))) Fn D \land (f \in D ⟼ if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R})) Fn D) \to (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})))) {+_{R}}_{f} (f \in D ⟼ if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R})) = (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\}))) +_{R} if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R}))$
424	414 419 422 423	syl3anc	$⊢ φ \to (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\})))) {+_{R}}_{f} (f \in D ⟼ if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R})) = (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\}))) +_{R} if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R}))$
425	377 411 424	3eqtrd	$⊢ φ \to (V (Y) \underset{˙}{\cdot} G (E (K - 1))) \underset{˙}{+} G (E (K)) = (f \in D ⟼ if (f (Y) = 0, 0_{R}, G (E (K - 1)) (f -_{f} 𝟙_{I} (\{Y\}))) +_{R} if (f (Y) = 0, if ((ran ({f ↾}_{J}) \subseteq \{0, 1\} \land \|({f ↾}_{J}) supp 0\| = K), 1_{R}, 0_{R}), 0_{R}))$
426	5 7 8 291 17 20	esplyfval3	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) with typecode \|-
427	367 425 426	3eqtr4rd	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) .+ ( G ` ( E ` K ) ) ) ) : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) .+ ( G ` ( E ` K ) ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem esplyind

Proof