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