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