Theorem esplyind 33882

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

Hypotheses

Ref	Expression
esplyind.w	⊢ 𝑊 = (𝐼 mPoly 𝑅)
esplyind.v	⊢ 𝑉 = (𝐼 mVar 𝑅)
esplyind.p	⊢ + = (+g‘𝑊)
esplyind.m	⊢ · = (.r‘𝑊)
esplyind.d	⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
esplyind.g	⊢ 𝐺 = ((𝐼extendVars𝑅)‘𝑌)
esplyind.i	⊢ (𝜑 → 𝐼 ∈ Fin)
esplyind.r	⊢ (𝜑 → 𝑅 ∈ Ring)
esplyind.y	⊢ (𝜑 → 𝑌 ∈ 𝐼)
esplyind.j	⊢ 𝐽 = (𝐼 ∖ {𝑌})
esplyind.e	⊢ 𝐸 = (𝐽eSymPoly𝑅)
esplyind.k	⊢ (𝜑 → 𝐾 ∈ (1...(♯‘𝐼)))
esplyind.1	⊢ 𝐶 = {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}

Assertion

Ref	Expression
esplyind	⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) + (𝐺‘(𝐸‘𝐾))))

Distinct variable groups:   ℎ,𝐼   ℎ,𝐽   ℎ,𝑌

Allowed substitution hints:   𝜑(ℎ)   𝐶(ℎ)   𝐷(ℎ)   + (ℎ)   𝑅(ℎ)   · (ℎ)   𝐸(ℎ)   𝐺(ℎ)   𝐾(ℎ)   𝑉(ℎ)   𝑊(ℎ)

Proof of Theorem esplyind

Dummy variables 𝑓 𝑔 𝑧 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovif12 7500	. . . 4 ⊢ (if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))(+g‘𝑅)if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))) = if((𝑓‘𝑌) = 0, ((0g‘𝑅)(+g‘𝑅)if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))), (((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))(+g‘𝑅)(0g‘𝑅)))
2		eqid 2765	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		eqid 2765	. . . . . . 7 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2765	. . . . . . 7 ⊢ (0g‘𝑅) = (0g‘𝑅)
5		esplyind.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Ring)
6	5	ringgrpd 20315	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
7	6	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → 𝑅 ∈ Grp)
8		eqid 2765	. . . . . . . . . . 11 ⊢ (1r‘𝑅) = (1r‘𝑅)
9	2, 8, 5	ringidcld 20340	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅))
10	9	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (1r‘𝑅) ∈ (Base‘𝑅))
11		ringgrp 20311	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
12	2, 4	grpidcl 19022	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Grp → (0g‘𝑅) ∈ (Base‘𝑅))
13	5, 11, 12	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
14	13	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (0g‘𝑅) ∈ (Base‘𝑅))
15	10, 14	ifcld 4530	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) ∈ (Base‘𝑅))
16	15	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) ∈ (Base‘𝑅))
17	2, 3, 4, 7, 16	grplidd 19026	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((0g‘𝑅)(+g‘𝑅)if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))) = if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
18		snsspr1 4775	. . . . . . . . . . 11 ⊢ {0} ⊆ {0, 1}
19	18	biantru 538	. . . . . . . . . 10 ⊢ (ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ↔ (ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ {0} ⊆ {0, 1}))
20		unss 4145	. . . . . . . . . 10 ⊢ ((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ {0} ⊆ {0, 1}) ↔ (ran (𝑓 ↾ 𝐽) ∪ {0}) ⊆ {0, 1})
21	19, 20	bitri 278	. . . . . . . . 9 ⊢ (ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ↔ (ran (𝑓 ↾ 𝐽) ∪ {0}) ⊆ {0, 1})
22		esplyind.i	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐼 ∈ Fin)
23	22	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝐼 ∈ Fin)
24		nn0ex 12501	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ0 ∈ V
25	24	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ℕ0 ∈ V)
26		esplyind.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
27	26	ssrab3 4038	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐷 ⊆ (ℕ0 ↑m 𝐼)
28	27	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ⊆ (ℕ0 ↑m 𝐼))
29	28	sselda 3939	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ (ℕ0 ↑m 𝐼))
30	23, 25, 29	elmaprd 32937	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓:𝐼⟶ℕ0)
31	30	freld 6702	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → Rel 𝑓)
32	30	ffnd 6696	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 Fn 𝐼)
33	32	fndmd 6630	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → dom 𝑓 = 𝐼)
34		esplyind.j	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (𝐼 ∖ {𝑌})
35	34	uneq1i 4120	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 ∪ {𝑌}) = ((𝐼 ∖ {𝑌}) ∪ {𝑌})
36		esplyind.y	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑌 ∈ 𝐼)
37	36	snssd 4748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝑌} ⊆ 𝐼)
38		undifr 4440	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑌} ⊆ 𝐼 ↔ ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
39	37, 38	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
40	35, 39	eqtr2id 2813	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐼 = (𝐽 ∪ {𝑌}))
41	40	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝐼 = (𝐽 ∪ {𝑌}))
42	33, 41	eqtrd 2800	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → dom 𝑓 = (𝐽 ∪ {𝑌}))
43		reldmun 6024	. . . . . . . . . . . . . . . 16 ⊢ ((Rel 𝑓 ∧ dom 𝑓 = (𝐽 ∪ {𝑌})) → 𝑓 = ((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})))
44	31, 42, 43	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 = ((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})))
45	44	rneqd 5919	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ran 𝑓 = ran ((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})))
46		rnun 6133	. . . . . . . . . . . . . 14 ⊢ ran ((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})) = (ran (𝑓 ↾ 𝐽) ∪ ran (𝑓 ↾ {𝑌}))
47	45, 46	eqtr2di 2817	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (ran (𝑓 ↾ 𝐽) ∪ ran (𝑓 ↾ {𝑌})) = ran 𝑓)
48	32	fnfund 6626	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → Fun 𝑓)
49	36	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑌 ∈ 𝐼)
50	49, 33	eleqtrrd 2868	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑌 ∈ dom 𝑓)
51		rnressnsn 32934	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝑓 ∧ 𝑌 ∈ dom 𝑓) → ran (𝑓 ↾ {𝑌}) = {(𝑓‘𝑌)})
52	48, 50, 51	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ran (𝑓 ↾ {𝑌}) = {(𝑓‘𝑌)})
53	52	uneq2d 4124	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (ran (𝑓 ↾ 𝐽) ∪ ran (𝑓 ↾ {𝑌})) = (ran (𝑓 ↾ 𝐽) ∪ {(𝑓‘𝑌)}))
54	47, 53	eqtr3d 2802	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ran 𝑓 = (ran (𝑓 ↾ 𝐽) ∪ {(𝑓‘𝑌)}))
55	54	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ran 𝑓 = (ran (𝑓 ↾ 𝐽) ∪ {(𝑓‘𝑌)}))
56		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓‘𝑌) = 0)
57	56	sneqd 4597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → {(𝑓‘𝑌)} = {0})
58	57	uneq2d 4124	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (ran (𝑓 ↾ 𝐽) ∪ {(𝑓‘𝑌)}) = (ran (𝑓 ↾ 𝐽) ∪ {0}))
59	55, 58	eqtrd 2800	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ran 𝑓 = (ran (𝑓 ↾ 𝐽) ∪ {0}))
60	59	sseq1d 3970	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (ran 𝑓 ⊆ {0, 1} ↔ (ran (𝑓 ↾ 𝐽) ∪ {0}) ⊆ {0, 1}))
61	21, 60	bitr4id 293	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ↔ ran 𝑓 ⊆ {0, 1}))
62	44	oveq1d 7415	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 supp 0) = (((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})) supp 0))
63	29	resexd 6018	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 ↾ 𝐽) ∈ V)
64	29	resexd 6018	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 ↾ {𝑌}) ∈ V)
65		0nn0 12510	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
66	65	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 0 ∈ ℕ0)
67	63, 64, 66	suppun2 32941	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})) supp 0) = (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)))
68	62, 67	eqtrd 2800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 supp 0) = (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)))
69	68	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 supp 0) = (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)))
70		fnressn 7145	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 Fn 𝐼 ∧ 𝑌 ∈ 𝐼) → (𝑓 ↾ {𝑌}) = {⟨𝑌, (𝑓‘𝑌)⟩})
71	32, 49, 70	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 ↾ {𝑌}) = {⟨𝑌, (𝑓‘𝑌)⟩})
72	71	oveq1d 7415	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ((𝑓 ↾ {𝑌}) supp 0) = ({⟨𝑌, (𝑓‘𝑌)⟩} supp 0))
73	30, 49	ffvelcdmd 7070	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓‘𝑌) ∈ ℕ0)
74		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑌, (𝑓‘𝑌)⟩} = {⟨𝑌, (𝑓‘𝑌)⟩}
75	74	suppsnop 8162	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ 𝐼 ∧ (𝑓‘𝑌) ∈ ℕ0 ∧ 0 ∈ ℕ0) → ({⟨𝑌, (𝑓‘𝑌)⟩} supp 0) = if((𝑓‘𝑌) = 0, ∅, {𝑌}))
76	49, 73, 66, 75	syl3anc 1394	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ({⟨𝑌, (𝑓‘𝑌)⟩} supp 0) = if((𝑓‘𝑌) = 0, ∅, {𝑌}))
77	72, 76	eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ((𝑓 ↾ {𝑌}) supp 0) = if((𝑓‘𝑌) = 0, ∅, {𝑌}))
78	77	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((𝑓 ↾ {𝑌}) supp 0) = if((𝑓‘𝑌) = 0, ∅, {𝑌}))
79	56	iftrued 4491	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → if((𝑓‘𝑌) = 0, ∅, {𝑌}) = ∅)
80	78, 79	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((𝑓 ↾ {𝑌}) supp 0) = ∅)
81	80	uneq2d 4124	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)) = (((𝑓 ↾ 𝐽) supp 0) ∪ ∅))
82		un0 4351	. . . . . . . . . . 11 ⊢ (((𝑓 ↾ 𝐽) supp 0) ∪ ∅) = ((𝑓 ↾ 𝐽) supp 0)
83	81, 82	eqtrdi 2816	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)) = ((𝑓 ↾ 𝐽) supp 0))
84	69, 83	eqtr2d 2801	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((𝑓 ↾ 𝐽) supp 0) = (𝑓 supp 0))
85	84	fveqeq2d 6879	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾 ↔ (♯‘(𝑓 supp 0)) = 𝐾))
86	61, 85	anbi12d 643	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾) ↔ (ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾)))
87	86	ifbid 4507	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
88	17, 87	eqtrd 2800	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((0g‘𝑅)(+g‘𝑅)if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
89	6	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑅 ∈ Grp)
90		esplyind.w	. . . . . . . . . 10 ⊢ 𝑊 = (𝐼 mPoly 𝑅)
91		eqid 2765	. . . . . . . . . 10 ⊢ (Base‘𝑊) = (Base‘𝑊)
92	26	psrbasfsupp 33818	. . . . . . . . . 10 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
93		esplyind.g	. . . . . . . . . . . 12 ⊢ 𝐺 = ((𝐼extendVars𝑅)‘𝑌)
94	93	fveq1i 6872	. . . . . . . . . . 11 ⊢ (𝐺‘(𝐸‘(𝐾 − 1))) = (((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘(𝐾 − 1)))
95		eqid 2765	. . . . . . . . . . . . 13 ⊢ (Base‘(𝐽 mPoly 𝑅)) = (Base‘(𝐽 mPoly 𝑅))
96	90	fveq2i 6874	. . . . . . . . . . . . 13 ⊢ (Base‘𝑊) = (Base‘(𝐼 mPoly 𝑅))
97	26, 4, 22, 5, 2, 34, 95, 36, 96	extvfvalf 33844	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐼extendVars𝑅)‘𝑌):(Base‘(𝐽 mPoly 𝑅))⟶(Base‘𝑊))
98		esplyind.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝐽eSymPoly𝑅)
99	98	fveq1i 6872	. . . . . . . . . . . . 13 ⊢ (𝐸‘(𝐾 − 1)) = ((𝐽eSymPoly𝑅)‘(𝐾 − 1))
100		esplyind.1	. . . . . . . . . . . . . 14 ⊢ 𝐶 = {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}
101		difssd 4093	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 ∖ {𝑌}) ⊆ 𝐼)
102	34, 101	eqsstrid 3977	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐽 ⊆ 𝐼)
103	22, 102	ssfid 9217	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ Fin)
104		esplyind.k	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ (1...(♯‘𝐼)))
105		elfznn 13572	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...(♯‘𝐼)) → 𝐾 ∈ ℕ)
106		nnm1nn0 12536	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ0)
107	104, 105, 106	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾 − 1) ∈ ℕ0)
108	100, 103, 5, 107, 95	esplympl 33874	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘(𝐾 − 1)) ∈ (Base‘(𝐽 mPoly 𝑅)))
109	99, 108	eqeltrid 2869	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘(𝐾 − 1)) ∈ (Base‘(𝐽 mPoly 𝑅)))
110	97, 109	ffvelcdmd 7070	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘(𝐾 − 1))) ∈ (Base‘𝑊))
111	94, 110	eqeltrid 2869	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘(𝐸‘(𝐾 − 1))) ∈ (Base‘𝑊))
112	90, 2, 91, 92, 111	mplelf 22107	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘(𝐸‘(𝐾 − 1))):𝐷⟶(Base‘𝑅))
113	112	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (𝐺‘(𝐸‘(𝐾 − 1))):𝐷⟶(Base‘𝑅))
114		simplr 780	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑓 ∈ 𝐷)
115		indf 12215	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ Fin ∧ {𝑌} ⊆ 𝐼) → ((𝟭‘𝐼)‘{𝑌}):𝐼⟶{0, 1})
116	22, 37, 115	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝟭‘𝐼)‘{𝑌}):𝐼⟶{0, 1})
117	65	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℕ0)
118		1nn0 12511	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
119	118	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℕ0)
120	117, 119	prssd 4783	. . . . . . . . . . 11 ⊢ (𝜑 → {0, 1} ⊆ ℕ0)
121	116, 120	fssd 6713	. . . . . . . . . 10 ⊢ (𝜑 → ((𝟭‘𝐼)‘{𝑌}):𝐼⟶ℕ0)
122	121	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝟭‘𝐼)‘{𝑌}):𝐼⟶ℕ0)
123	22	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝐼 ∈ Fin)
124	123	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 𝐼 ∈ Fin)
125	37	ad4antr 744	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → {𝑌} ⊆ 𝐼)
126		velsn 4601	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑌} ↔ 𝑥 = 𝑌)
127	126	bilanri 511	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 𝑥 ∈ {𝑌})
128		ind1 12218	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ Fin ∧ {𝑌} ⊆ 𝐼 ∧ 𝑥 ∈ {𝑌}) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = 1)
129	124, 125, 127, 128	syl3anc 1394	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = 1)
130	30	ad3antrrr 742	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 𝑓:𝐼⟶ℕ0)
131		simplr 780	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 𝑥 ∈ 𝐼)
132	130, 131	ffvelcdmd 7070	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (𝑓‘𝑥) ∈ ℕ0)
133		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 𝑥 = 𝑌)
134	133	fveq2d 6875	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (𝑓‘𝑥) = (𝑓‘𝑌))
135		simpllr 787	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → ¬ (𝑓‘𝑌) = 0)
136	135	neqned 2967	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (𝑓‘𝑌) ≠ 0)
137	134, 136	eqnetrd 3027	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (𝑓‘𝑥) ≠ 0)
138		elnnne0 12509	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑥) ∈ ℕ ↔ ((𝑓‘𝑥) ∈ ℕ0 ∧ (𝑓‘𝑥) ≠ 0))
139	132, 137, 138	sylanbrc 594	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (𝑓‘𝑥) ∈ ℕ)
140	139	nnge1d 12275	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 1 ≤ (𝑓‘𝑥))
141	129, 140	eqbrtrd 5127	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) ≤ (𝑓‘𝑥))
142	123	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → 𝐼 ∈ Fin)
143	37	ad4antr 744	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → {𝑌} ⊆ 𝐼)
144		simplr 780	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → 𝑥 ∈ 𝐼)
145		simpr 489	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → 𝑥 ≠ 𝑌)
146	144, 145	eldifsnd 4750	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → 𝑥 ∈ (𝐼 ∖ {𝑌}))
147		ind0 12219	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ Fin ∧ {𝑌} ⊆ 𝐼 ∧ 𝑥 ∈ (𝐼 ∖ {𝑌})) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = 0)
148	142, 143, 146, 147	syl3anc 1394	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = 0)
149	30	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑓:𝐼⟶ℕ0)
150	149	ffvelcdmda 7069	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℕ0)
151	150	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → (𝑓‘𝑥) ∈ ℕ0)
152	151	nn0ge0d 12559	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → 0 ≤ (𝑓‘𝑥))
153	148, 152	eqbrtrd 5127	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) ≤ (𝑓‘𝑥))
154	141, 153	pm2.61dane 3047	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) ≤ (𝑓‘𝑥))
155	154	ralrimiva 3157	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ∀𝑥 ∈ 𝐼 (((𝟭‘𝐼)‘{𝑌})‘𝑥) ≤ (𝑓‘𝑥))
156	122	ffnd 6696	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
157	32	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑓 Fn 𝐼)
158		inidm 4181	. . . . . . . . . . 11 ⊢ (𝐼 ∩ 𝐼) = 𝐼
159		eqidd 2766	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = (((𝟭‘𝐼)‘{𝑌})‘𝑥))
160		eqidd 2766	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥))
161	156, 157, 123, 123, 158, 159, 160	ofrfval 7674	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (((𝟭‘𝐼)‘{𝑌}) ∘r ≤ 𝑓 ↔ ∀𝑥 ∈ 𝐼 (((𝟭‘𝐼)‘{𝑌})‘𝑥) ≤ (𝑓‘𝑥)))
162	155, 161	mpbird 260	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝟭‘𝐼)‘{𝑌}) ∘r ≤ 𝑓)
163	92	psrbagcon 22035	. . . . . . . . . 10 ⊢ ((𝑓 ∈ 𝐷 ∧ ((𝟭‘𝐼)‘{𝑌}):𝐼⟶ℕ0 ∧ ((𝟭‘𝐼)‘{𝑌}) ∘r ≤ 𝑓) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ 𝐷 ∧ (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∘r ≤ 𝑓))
164	163	simpld 499	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐷 ∧ ((𝟭‘𝐼)‘{𝑌}):𝐼⟶ℕ0 ∧ ((𝟭‘𝐼)‘{𝑌}) ∘r ≤ 𝑓) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ 𝐷)
165	114, 122, 162, 164	syl3anc 1394	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ 𝐷)
166	113, 165	ffvelcdmd 7070	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) ∈ (Base‘𝑅))
167	2, 3, 4, 89, 166	grpridd 19027	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))(+g‘𝑅)(0g‘𝑅)) = ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))
168	94	fveq1i 6872	. . . . . . . 8 ⊢ ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) = ((((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))
169	168	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) = ((((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))
170	5	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑅 ∈ Ring)
171	36	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑌 ∈ 𝐼)
172	109	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (𝐸‘(𝐾 − 1)) ∈ (Base‘(𝐽 mPoly 𝑅)))
173	26, 4, 123, 170, 171, 34, 95, 172, 165	extvfvv 33841	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) = if(((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0, ((𝐸‘(𝐾 − 1))‘((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)), (0g‘𝑅)))
174	100, 103, 5, 107, 4, 8	esplyfval3 33879	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘(𝐾 − 1)) = (𝑧 ∈ 𝐶 ↦ if((ran 𝑧 ⊆ {0, 1} ∧ (♯‘(𝑧 supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅))))
175	99, 174	eqtrid 2812	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘(𝐾 − 1)) = (𝑧 ∈ 𝐶 ↦ if((ran 𝑧 ⊆ {0, 1} ∧ (♯‘(𝑧 supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅))))
176	175	ad3antrrr 742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝐸‘(𝐾 − 1)) = (𝑧 ∈ 𝐶 ↦ if((ran 𝑧 ⊆ {0, 1} ∧ (♯‘(𝑧 supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅))))
177	47	ad4antr 744	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → (ran (𝑓 ↾ 𝐽) ∪ ran (𝑓 ↾ {𝑌})) = ran 𝑓)
178		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽))
179	116	ffnd 6696	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
180	179	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
181	32, 180, 23, 23, 158	offn 7677	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) Fn 𝐼)
182	181	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) Fn 𝐼)
183	102	ad4antr 744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → 𝐽 ⊆ 𝐼)
184	182, 183	fnssresd 6649	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) Fn 𝐽)
185		fneq1 6616	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) → (𝑧 Fn 𝐽 ↔ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) Fn 𝐽))
186	185	biimpar 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) Fn 𝐽) → 𝑧 Fn 𝐽)
187	178, 184, 186	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → 𝑧 Fn 𝐽)
188	32	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 𝑓 Fn 𝐼)
189	102	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 𝐽 ⊆ 𝐼)
190	188, 189	fnssresd 6649	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ↾ 𝐽) Fn 𝐽)
191	190	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → (𝑓 ↾ 𝐽) Fn 𝐽)
192		simplr 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽))
193	192	fveq1d 6873	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (𝑧‘𝑥) = (((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)‘𝑥))
194		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐽)
195	194	fvresd 6891	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)‘𝑥) = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑥))
196	188	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑓 Fn 𝐼)
197	156	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
198	197	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
199	23	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 𝐼 ∈ Fin)
200	199	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝐼 ∈ Fin)
201	183	sselda 3939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐼)
202		fnfvof 7681	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 Fn 𝐼 ∧ ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼) ∧ (𝐼 ∈ Fin ∧ 𝑥 ∈ 𝐼)) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑥) = ((𝑓‘𝑥) − (((𝟭‘𝐼)‘{𝑌})‘𝑥)))
203	196, 198, 200, 201, 202	syl22anc 851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑥) = ((𝑓‘𝑥) − (((𝟭‘𝐼)‘{𝑌})‘𝑥)))
204	37	ad5antr 746	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → {𝑌} ⊆ 𝐼)
205	194, 34	eleqtrdi 2875	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ (𝐼 ∖ {𝑌}))
206	200, 204, 205, 147	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = 0)
207	206	oveq2d 7416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓‘𝑥) − (((𝟭‘𝐼)‘{𝑌})‘𝑥)) = ((𝑓‘𝑥) − 0))
208	149	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑓:𝐼⟶ℕ0)
209	208, 201	ffvelcdmd 7070	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (𝑓‘𝑥) ∈ ℕ0)
210	209	nn0cnd 12558	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (𝑓‘𝑥) ∈ ℂ)
211	210	subid1d 11546	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓‘𝑥) − 0) = (𝑓‘𝑥))
212	194	fvresd 6891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓 ↾ 𝐽)‘𝑥) = (𝑓‘𝑥))
213	211, 212	eqtr4d 2803	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓‘𝑥) − 0) = ((𝑓 ↾ 𝐽)‘𝑥))
214	203, 207, 213	3eqtrd 2804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑥) = ((𝑓 ↾ 𝐽)‘𝑥))
215	193, 195, 214	3eqtrd 2804	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (𝑧‘𝑥) = ((𝑓 ↾ 𝐽)‘𝑥))
216	187, 191, 215	eqfnfvd 7018	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → 𝑧 = (𝑓 ↾ 𝐽))
217	216	rneqd 5919	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → ran 𝑧 = ran (𝑓 ↾ 𝐽))
218	217	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran 𝑧 = ran (𝑓 ↾ 𝐽))
219		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran 𝑧 ⊆ {0, 1})
220	218, 219	eqsstrrd 3974	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran (𝑓 ↾ 𝐽) ⊆ {0, 1})
221	48	ad4antr 744	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → Fun 𝑓)
222	50	ad4antr 744	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → 𝑌 ∈ dom 𝑓)
223	221, 222, 51	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran (𝑓 ↾ {𝑌}) = {(𝑓‘𝑌)})
224	73	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓‘𝑌) ∈ ℕ0)
225	224	nn0cnd 12558	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓‘𝑌) ∈ ℂ)
226	116, 36	ffvelcdmd 7070	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((𝟭‘𝐼)‘{𝑌})‘𝑌) ∈ {0, 1})
227	120, 226	sseldd 3940	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝟭‘𝐼)‘{𝑌})‘𝑌) ∈ ℕ0)
228	227	nn0cnd 12558	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝟭‘𝐼)‘{𝑌})‘𝑌) ∈ ℂ)
229	228	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (((𝟭‘𝐼)‘{𝑌})‘𝑌) ∈ ℂ)
230	171	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 𝑌 ∈ 𝐼)
231		fnfvof 7681	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓 Fn 𝐼 ∧ ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼) ∧ (𝐼 ∈ Fin ∧ 𝑌 ∈ 𝐼)) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = ((𝑓‘𝑌) − (((𝟭‘𝐼)‘{𝑌})‘𝑌)))
232	188, 197, 199, 230, 231	syl22anc 851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = ((𝑓‘𝑌) − (((𝟭‘𝐼)‘{𝑌})‘𝑌)))
233		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0)
234	232, 233	eqtr3d 2802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓‘𝑌) − (((𝟭‘𝐼)‘{𝑌})‘𝑌)) = 0)
235	225, 229, 234	subeq0d 11565	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓‘𝑌) = (((𝟭‘𝐼)‘{𝑌})‘𝑌))
236		snidg 4622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑌 ∈ 𝐼 → 𝑌 ∈ {𝑌})
237	36, 236	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑌 ∈ {𝑌})
238		ind1 12218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ Fin ∧ {𝑌} ⊆ 𝐼 ∧ 𝑌 ∈ {𝑌}) → (((𝟭‘𝐼)‘{𝑌})‘𝑌) = 1)
239	22, 37, 237, 238	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝟭‘𝐼)‘{𝑌})‘𝑌) = 1)
240	239	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (((𝟭‘𝐼)‘{𝑌})‘𝑌) = 1)
241	235, 240	eqtrd 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓‘𝑌) = 1)
242	241	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → (𝑓‘𝑌) = 1)
243	242	sneqd 4597	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → {(𝑓‘𝑌)} = {1})
244	223, 243	eqtrd 2800	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran (𝑓 ↾ {𝑌}) = {1})
245		snsspr2 4776	. . . . . . . . . . . . . . . 16 ⊢ {1} ⊆ {0, 1}
246	244, 245	eqsstrdi 3983	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran (𝑓 ↾ {𝑌}) ⊆ {0, 1})
247	220, 246	unssd 4147	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → (ran (𝑓 ↾ 𝐽) ∪ ran (𝑓 ↾ {𝑌})) ⊆ {0, 1})
248	177, 247	eqsstrrd 3974	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran 𝑓 ⊆ {0, 1})
249	216	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑓 ⊆ {0, 1}) → 𝑧 = (𝑓 ↾ 𝐽))
250	249	rneqd 5919	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑓 ⊆ {0, 1}) → ran 𝑧 = ran (𝑓 ↾ 𝐽))
251		rnresss 6007	. . . . . . . . . . . . . . 15 ⊢ ran (𝑓 ↾ 𝐽) ⊆ ran 𝑓
252		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑓 ⊆ {0, 1}) → ran 𝑓 ⊆ {0, 1})
253	251, 252	sstrid 3950	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑓 ⊆ {0, 1}) → ran (𝑓 ↾ 𝐽) ⊆ {0, 1})
254	250, 253	eqsstrd 3973	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑓 ⊆ {0, 1}) → ran 𝑧 ⊆ {0, 1})
255	248, 254	impbida 812	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → (ran 𝑧 ⊆ {0, 1} ↔ ran 𝑓 ⊆ {0, 1}))
256	216	oveq1d 7415	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → (𝑧 supp 0) = ((𝑓 ↾ 𝐽) supp 0))
257	256	fveqeq2d 6879	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → ((♯‘(𝑧 supp 0)) = (𝐾 − 1) ↔ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)))
258	255, 257	anbi12d 643	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → ((ran 𝑧 ⊆ {0, 1} ∧ (♯‘(𝑧 supp 0)) = (𝐾 − 1)) ↔ (ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1))))
259	258	ifbid 4507	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → if((ran 𝑧 ⊆ {0, 1} ∧ (♯‘(𝑧 supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅)))
260		breq1 5108	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) → (ℎ finSupp 0 ↔ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) finSupp 0))
261	27, 165	sselid 3937	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ (ℕ0 ↑m 𝐼))
262	261	adantr 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ (ℕ0 ↑m 𝐼))
263	262, 189	elmapssresd 8853	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽))
264		breq1 5108	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) → (ℎ finSupp 0 ↔ (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) finSupp 0))
265	165	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ 𝐷)
266	265, 26	eleqtrdi 2875	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
267	264, 266	elrabrd 3656	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) finSupp 0)
268	65	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 0 ∈ ℕ0)
269	267, 268	fsuppres 9341	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) finSupp 0)
270	260, 263, 269	elrabd 3655	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0})
271	270, 100	eleqtrrdi 2876	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) ∈ 𝐶)
272	10	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (1r‘𝑅) ∈ (Base‘𝑅))
273	14	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (0g‘𝑅) ∈ (Base‘𝑅))
274	272, 273	ifcld 4530	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅)) ∈ (Base‘𝑅))
275	176, 259, 271, 274	fvmptd 6987	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝐸‘(𝐾 − 1))‘((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅)))
276		eqcom 2772	. . . . . . . . . . . . 13 ⊢ ((𝐾 − 1) = (♯‘((𝑓 ↾ 𝐽) supp 0)) ↔ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1))
277		fz1ssfz0 13642	. . . . . . . . . . . . . . . . . 18 ⊢ (1...(♯‘𝐼)) ⊆ (0...(♯‘𝐼))
278		fz0ssnn0 13641	. . . . . . . . . . . . . . . . . 18 ⊢ (0...(♯‘𝐼)) ⊆ ℕ0
279	277, 278	sstri 3948	. . . . . . . . . . . . . . . . 17 ⊢ (1...(♯‘𝐼)) ⊆ ℕ0
280	279, 104	sselid 3937	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
281	280	nn0cnd 12558	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ ℂ)
282	281	ad3antrrr 742	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 𝐾 ∈ ℂ)
283		1cnd 11190	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 1 ∈ ℂ)
284		c0ex 11188	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ V
285	284	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 0 ∈ V)
286	30, 23, 285	fidmfisupp 9320	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 finSupp 0)
287	286, 285	fsuppres 9341	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 ↾ 𝐽) finSupp 0)
288	287	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ↾ 𝐽) finSupp 0)
289	288	fsuppimpd 9317	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ↾ 𝐽) supp 0) ∈ Fin)
290		hashcl 14383	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ↾ 𝐽) supp 0) ∈ Fin → (♯‘((𝑓 ↾ 𝐽) supp 0)) ∈ ℕ0)
291	289, 290	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (♯‘((𝑓 ↾ 𝐽) supp 0)) ∈ ℕ0)
292	291	nn0cnd 12558	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (♯‘((𝑓 ↾ 𝐽) supp 0)) ∈ ℂ)
293	282, 283, 292	subadd2d 11576	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝐾 − 1) = (♯‘((𝑓 ↾ 𝐽) supp 0)) ↔ ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1) = 𝐾))
294	276, 293	bitr3id 288	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1) ↔ ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1) = 𝐾))
295	68	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 supp 0) = (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)))
296	77	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ↾ {𝑌}) supp 0) = if((𝑓‘𝑌) = 0, ∅, {𝑌}))
297		simplr 780	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ¬ (𝑓‘𝑌) = 0)
298	297	iffalsed 4494	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → if((𝑓‘𝑌) = 0, ∅, {𝑌}) = {𝑌})
299	296, 298	eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ↾ {𝑌}) supp 0) = {𝑌})
300	299	uneq2d 4124	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)) = (((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌}))
301	295, 300	eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 supp 0) = (((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌}))
302	301	fveq2d 6875	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (♯‘(𝑓 supp 0)) = (♯‘(((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌})))
303		suppssdm 8161	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ↾ 𝐽) supp 0) ⊆ dom (𝑓 ↾ 𝐽)
304		resdmss 6226	. . . . . . . . . . . . . . . . . 18 ⊢ dom (𝑓 ↾ 𝐽) ⊆ 𝐽
305	303, 304	sstri 3948	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ↾ 𝐽) supp 0) ⊆ 𝐽
306	305	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ↾ 𝐽) supp 0) ⊆ 𝐽)
307	34	eqimssi 3999	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐽 ⊆ (𝐼 ∖ {𝑌})
308		ssdifsn 4751	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 ⊆ (𝐼 ∖ {𝑌}) ↔ (𝐽 ⊆ 𝐼 ∧ ¬ 𝑌 ∈ 𝐽))
309	307, 308	mpbi 233	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ⊆ 𝐼 ∧ ¬ 𝑌 ∈ 𝐽)
310	309	simpri 490	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 𝑌 ∈ 𝐽
311	310	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ¬ 𝑌 ∈ 𝐽)
312	306, 311	ssneldd 3942	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ¬ 𝑌 ∈ ((𝑓 ↾ 𝐽) supp 0))
313		hashunsng 14419	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ∈ 𝐼 → ((((𝑓 ↾ 𝐽) supp 0) ∈ Fin ∧ ¬ 𝑌 ∈ ((𝑓 ↾ 𝐽) supp 0)) → (♯‘(((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌})) = ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1)))
314	313	imp 411	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∈ 𝐼 ∧ (((𝑓 ↾ 𝐽) supp 0) ∈ Fin ∧ ¬ 𝑌 ∈ ((𝑓 ↾ 𝐽) supp 0))) → (♯‘(((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌})) = ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1))
315	230, 289, 312, 314	syl12anc 849	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (♯‘(((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌})) = ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1))
316	302, 315	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (♯‘(𝑓 supp 0)) = ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1))
317	316	eqeq1d 2767	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((♯‘(𝑓 supp 0)) = 𝐾 ↔ ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1) = 𝐾))
318	294, 317	bitr4d 285	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1) ↔ (♯‘(𝑓 supp 0)) = 𝐾))
319	318	anbi2d 641	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)) ↔ (ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾)))
320	319	ifbid 4507	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
321	275, 320	eqtrd 2800	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝐸‘(𝐾 − 1))‘((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
322		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ran 𝑓 ⊆ {0, 1})
323	157	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → 𝑓 Fn 𝐼)
324	171	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → 𝑌 ∈ 𝐼)
325	323, 324	fnfvelrnd 7067	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓‘𝑌) ∈ ran 𝑓)
326	322, 325	sseldd 3940	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓‘𝑌) ∈ {0, 1})
327		simpllr 787	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ¬ (𝑓‘𝑌) = 0)
328	327	neqned 2967	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓‘𝑌) ≠ 0)
329	73	nn0cnd 12558	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓‘𝑌) ∈ ℂ)
330	329	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓‘𝑌) ∈ ℂ)
331		1cnd 11190	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → 1 ∈ ℂ)
332		simplr 780	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0)
333	156	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
334	123	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → 𝐼 ∈ Fin)
335	323, 333, 334, 324, 231	syl22anc 851	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = ((𝑓‘𝑌) − (((𝟭‘𝐼)‘{𝑌})‘𝑌)))
336	239	ad4antr 744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (((𝟭‘𝐼)‘{𝑌})‘𝑌) = 1)
337	336	oveq2d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ((𝑓‘𝑌) − (((𝟭‘𝐼)‘{𝑌})‘𝑌)) = ((𝑓‘𝑌) − 1))
338	335, 337	eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = ((𝑓‘𝑌) − 1))
339	338	eqeq1d 2767	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0 ↔ ((𝑓‘𝑌) − 1) = 0))
340	332, 339	mtbid 327	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ¬ ((𝑓‘𝑌) − 1) = 0)
341		subeq0 11472	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓‘𝑌) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑓‘𝑌) − 1) = 0 ↔ (𝑓‘𝑌) = 1))
342	341	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑌) ∈ ℂ ∧ 1 ∈ ℂ) → (¬ ((𝑓‘𝑌) − 1) = 0 ↔ ¬ (𝑓‘𝑌) = 1))
343	342	biimpa 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑓‘𝑌) ∈ ℂ ∧ 1 ∈ ℂ) ∧ ¬ ((𝑓‘𝑌) − 1) = 0) → ¬ (𝑓‘𝑌) = 1)
344	330, 331, 340, 343	syl21anc 850	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ¬ (𝑓‘𝑌) = 1)
345	344	neqned 2967	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓‘𝑌) ≠ 1)
346	328, 345	nelprd 4619	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ¬ (𝑓‘𝑌) ∈ {0, 1})
347	326, 346	pm2.65da 828	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ¬ ran 𝑓 ⊆ {0, 1})
348	347	intnanrd 494	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ¬ (ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾))
349	348	iffalsed 4494	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅))
350	349	eqcomd 2771	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (0g‘𝑅) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
351	321, 350	ifeqda 4520	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → if(((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0, ((𝐸‘(𝐾 − 1))‘((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)), (0g‘𝑅)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
352	169, 173, 351	3eqtrd 2804	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
353	167, 352	eqtrd 2800	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))(+g‘𝑅)(0g‘𝑅)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
354	88, 353	ifeqda 4520	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → if((𝑓‘𝑌) = 0, ((0g‘𝑅)(+g‘𝑅)if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))), (((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))(+g‘𝑅)(0g‘𝑅))) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
355	1, 354	eqtrid 2812	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))(+g‘𝑅)if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
356	355	mpteq2dva 5198	. 2 ⊢ (𝜑 → (𝑓 ∈ 𝐷 ↦ (if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))(+g‘𝑅)if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))) = (𝑓 ∈ 𝐷 ↦ if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))))
357		esplyind.p	. . . 4 ⊢ + = (+g‘𝑊)
358		esplyind.m	. . . . 5 ⊢ · = (.r‘𝑊)
359	90, 22, 5	mplringd 22132	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Ring)
360		esplyind.v	. . . . . 6 ⊢ 𝑉 = (𝐼 mVar 𝑅)
361	90, 360, 91, 22, 5, 36	mvrcl 22101	. . . . 5 ⊢ (𝜑 → (𝑉‘𝑌) ∈ (Base‘𝑊))
362	91, 358, 359, 361, 111	ringcld 20333	. . . 4 ⊢ (𝜑 → ((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) ∈ (Base‘𝑊))
363	93	fveq1i 6872	. . . . 5 ⊢ (𝐺‘(𝐸‘𝐾)) = (((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘𝐾))
364	98	fveq1i 6872	. . . . . . 7 ⊢ (𝐸‘𝐾) = ((𝐽eSymPoly𝑅)‘𝐾)
365	100, 103, 5, 280, 95	esplympl 33874	. . . . . . 7 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘𝐾) ∈ (Base‘(𝐽 mPoly 𝑅)))
366	364, 365	eqeltrid 2869	. . . . . 6 ⊢ (𝜑 → (𝐸‘𝐾) ∈ (Base‘(𝐽 mPoly 𝑅)))
367	97, 366	ffvelcdmd 7070	. . . . 5 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘𝐾)) ∈ (Base‘𝑊))
368	363, 367	eqeltrid 2869	. . . 4 ⊢ (𝜑 → (𝐺‘(𝐸‘𝐾)) ∈ (Base‘𝑊))
369	90, 91, 3, 357, 362, 368	mpladd 22118	. . 3 ⊢ (𝜑 → (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) + (𝐺‘(𝐸‘𝐾))) = (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) ∘f (+g‘𝑅)(𝐺‘(𝐸‘𝐾))))
370	360	fveq1i 6872	. . . . 5 ⊢ (𝑉‘𝑌) = ((𝐼 mVar 𝑅)‘𝑌)
371		eqid 2765	. . . . 5 ⊢ ((𝟭‘𝐼)‘{𝑌}) = ((𝟭‘𝐼)‘{𝑌})
372	90, 370, 91, 358, 4, 26, 371, 22, 36, 5, 111	mplmulmvr 33846	. . . 4 ⊢ (𝜑 → ((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))))
373	93	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐺 = ((𝐼extendVars𝑅)‘𝑌))
374	100, 103, 5, 280, 4, 8	esplyfval3 33879	. . . . . . 7 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘𝐾) = (𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))))
375	364, 374	eqtrid 2812	. . . . . 6 ⊢ (𝜑 → (𝐸‘𝐾) = (𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))))
376	373, 375	fveq12d 6878	. . . . 5 ⊢ (𝜑 → (𝐺‘(𝐸‘𝐾)) = (((𝐼extendVars𝑅)‘𝑌)‘(𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))))
377	374, 365	eqeltrrd 2866	. . . . . 6 ⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘(𝐽 mPoly 𝑅)))
378	26, 4, 22, 5, 36, 34, 95, 377	extvfv 33840	. . . . 5 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝑌)‘(𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, ((𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))‘(𝑓 ↾ 𝐽)), (0g‘𝑅))))
379		rneq 5917	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → ran 𝑔 = ran (𝑓 ↾ 𝐽))
380	379	sseq1d 3970	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → (ran 𝑔 ⊆ {0, 1} ↔ ran (𝑓 ↾ 𝐽) ⊆ {0, 1}))
381		oveq1 7407	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → (𝑔 supp 0) = ((𝑓 ↾ 𝐽) supp 0))
382	381	fveqeq2d 6879	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → ((♯‘(𝑔 supp 0)) = 𝐾 ↔ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾))
383	380, 382	anbi12d 643	. . . . . . . . 9 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → ((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾) ↔ (ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾)))
384	383	ifbid 4507	. . . . . . . 8 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) = if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
385		eqidd 2766	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))) = (𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))))
386		breq1 5108	. . . . . . . . . 10 ⊢ (ℎ = (𝑓 ↾ 𝐽) → (ℎ finSupp 0 ↔ (𝑓 ↾ 𝐽) finSupp 0))
387	24	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ℕ0 ∈ V)
388	103	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → 𝐽 ∈ Fin)
389	30	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → 𝑓:𝐼⟶ℕ0)
390	102	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → 𝐽 ⊆ 𝐼)
391	389, 390	fssresd 6735	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 ↾ 𝐽):𝐽⟶ℕ0)
392	387, 388, 391	elmapdd 8826	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽))
393	287	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 ↾ 𝐽) finSupp 0)
394	386, 392, 393	elrabd 3655	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 ↾ 𝐽) ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0})
395	394, 100	eleqtrrdi 2876	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 ↾ 𝐽) ∈ 𝐶)
396		fvexd 6886	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (1r‘𝑅) ∈ V)
397		fvexd 6886	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (0g‘𝑅) ∈ V)
398	396, 397	ifcld 4530	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) ∈ V)
399	384, 385, 395, 398	fvmptd4 7004	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))‘(𝑓 ↾ 𝐽)) = if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
400	399	ifeq1da 4515	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → if((𝑓‘𝑌) = 0, ((𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))‘(𝑓 ↾ 𝐽)), (0g‘𝑅)) = if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))
401	400	mpteq2dva 5198	. . . . 5 ⊢ (𝜑 → (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, ((𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))‘(𝑓 ↾ 𝐽)), (0g‘𝑅))) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))))
402	376, 378, 401	3eqtrd 2804	. . . 4 ⊢ (𝜑 → (𝐺‘(𝐸‘𝐾)) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))))
403	372, 402	oveq12d 7418	. . 3 ⊢ (𝜑 → (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) ∘f (+g‘𝑅)(𝐺‘(𝐸‘𝐾))) = ((𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))) ∘f (+g‘𝑅)(𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))))
404		ovex 7433	. . . . . 6 ⊢ (ℕ0 ↑m 𝐼) ∈ V
405	26, 404	rabex2 5302	. . . . 5 ⊢ 𝐷 ∈ V
406	405	a1i 11	. . . 4 ⊢ (𝜑 → 𝐷 ∈ V)
407		nfv 1937	. . . . 5 ⊢ Ⅎ𝑓𝜑
408		fvexd 6886	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) ∈ V)
409	14, 408	ifexd 4532	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))) ∈ V)
410		eqid 2765	. . . . 5 ⊢ (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))))
411	407, 409, 410	fnmptd 6666	. . . 4 ⊢ (𝜑 → (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))) Fn 𝐷)
412	15, 14	ifcld 4530	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)) ∈ (Base‘𝑅))
413		eqid 2765	. . . . 5 ⊢ (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))
414	407, 412, 413	fnmptd 6666	. . . 4 ⊢ (𝜑 → (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))) Fn 𝐷)
415		ofmpteq 7687	. . . 4 ⊢ ((𝐷 ∈ V ∧ (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))) Fn 𝐷 ∧ (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))) Fn 𝐷) → ((𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))) ∘f (+g‘𝑅)(𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))) = (𝑓 ∈ 𝐷 ↦ (if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))(+g‘𝑅)if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))))
416	406, 411, 414, 415	syl3anc 1394	. . 3 ⊢ (𝜑 → ((𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))) ∘f (+g‘𝑅)(𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))) = (𝑓 ∈ 𝐷 ↦ (if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))(+g‘𝑅)if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))))
417	369, 403, 416	3eqtrd 2804	. 2 ⊢ (𝜑 → (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) + (𝐺‘(𝐸‘𝐾))) = (𝑓 ∈ 𝐷 ↦ (if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))(+g‘𝑅)if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))))
418	26, 22, 5, 280, 4, 8	esplyfval3 33879	. 2 ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = (𝑓 ∈ 𝐷 ↦ if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))))
419	356, 417, 418	3eqtr4rd 2811	1 ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) + (𝐺‘(𝐸‘𝐾))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145   ≠ wne 2960  ∀wral 3079  {crab 3417  Vcvv 3457   ∖ cdif 3904   ∪ cun 3905   ⊆ wss 3907  ∅c0 4288  ifcif 4483  {csn 4585  {cpr 4587  ⟨cop 4591   class class class wbr 5105   ↦ cmpt 5186  dom cdm 5652  ran crn 5653   ↾ cres 5654  Rel wrel 5657  Fun wfun 6519   Fn wfn 6520  ⟶wf 6521  ‘cfv 6525  (class class class)co 7400   ∘_f cof 7662   ∘_r cofr 7663   supp csupp 8144   ↑_m cmap 8812  Fincfn 8931   finSupp cfsupp 9309  ℂcc 11086  0cc0 11088  1c1 11089   + caddc 11091   ≤ cle 11232   − cmin 11429  𝟭cind 12209  ℕcn 12224  ℕ₀cn0 12495  ...cfz 13526  ♯chash 14357  Basecbs 17259  +_gcplusg 17300  ._rcmulr 17301  0_gc0g 17482  Grpcgrp 18990  1_rcur 20254  Ringcrg 20306   mVar cmvr 22015   mPoly cmpl 22016  extendVarscextv 33836  eSymPolycesply 33863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165  ax-addf 11167  ax-mulf 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4869  df-int 4909  df-iun 4954  df-iin 4955  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-se 5606  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-isom 6534  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-of 7664  df-ofr 7665  df-om 7851  df-1st 7974  df-2nd 7975  df-supp 8145  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-2o 8442  df-oadd 8445  df-er 8682  df-map 8814  df-pm 8815  df-ixp 8884  df-en 8932  df-dom 8933  df-sdom 8934  df-fin 8935  df-fsupp 9310  df-sup 9390  df-oi 9460  df-dju 9875  df-card 9913  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-ind 12210  df-nn 12225  df-2 12294  df-3 12295  df-4 12296  df-5 12297  df-6 12298  df-7 12299  df-8 12300  df-9 12301  df-n0 12496  df-xnn0 12569  df-z 12583  df-dec 12703  df-uz 12854  df-rp 13008  df-fz 13527  df-fzo 13674  df-seq 14029  df-fac 14301  df-bc 14330  df-hash 14358  df-struct 17197  df-sets 17214  df-slot 17232  df-ndx 17244  df-base 17260  df-ress 17281  df-plusg 17313  df-mulr 17314  df-starv 17315  df-sca 17316  df-vsca 17317  df-ip 17318  df-tset 17319  df-ple 17320  df-ds 17322  df-unif 17323  df-hom 17324  df-cco 17325  df-0g 17484  df-gsum 17485  df-prds 17490  df-pws 17492  df-mre 17628  df-mrc 17629  df-acs 17631  df-mgm 18688  df-sgrp 18767  df-mnd 18783  df-mhm 18831  df-submnd 18832  df-grp 18993  df-minusg 18994  df-mulg 19125  df-subg 19180  df-ghm 19275  df-cntz 19378  df-cmn 19843  df-abl 19844  df-mgp 20208  df-rng 20222  df-ur 20255  df-ring 20308  df-cring 20309  df-rhm 20545  df-subrng 20622  df-subrg 20646  df-cnfld 21483  df-zring 21557  df-zrh 21613  df-psr 22019  df-mvr 22020  df-mpl 22021  df-extv 33837  df-esply 33865

This theorem is referenced by:  esplyindfv  33883