Theorem esplyind 34253

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 7520	. . . 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 2760	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		eqid 2760	. . . . . . 7 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2760	. . . . . . 7 ⊢ (0g‘𝑅) = (0g‘𝑅)
5		esplyind.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Ring)
6	5	ringgrpd 20474	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
7	6	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → 𝑅 ∈ Grp)
8		eqid 2760	. . . . . . . . . . 11 ⊢ (1r‘𝑅) = (1r‘𝑅)
9	2, 8, 5	ringidcld 20500	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅))
10	9	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (1r‘𝑅) ∈ (Base‘𝑅))
11		ringgrp 20469	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
12	2, 4	grpidcl 19181	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Grp → (0g‘𝑅) ∈ (Base‘𝑅))
13	5, 11, 12	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
14	13	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (0g‘𝑅) ∈ (Base‘𝑅))
15	10, 14	ifcld 4528	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) ∈ (Base‘𝑅))
16	15	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) ∈ (Base‘𝑅))
17	2, 3, 4, 7, 16	grplidd 19185	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((0g‘𝑅)(+g‘𝑅)if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))) = if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
18		snsspr1 4769	. . . . . . . . . . 11 ⊢ {0} ⊆ {0, 1}
19	18	biantru 539	. . . . . . . . . 10 ⊢ (ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ↔ (ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ {0} ⊆ {0, 1}))
20		unss 4188	. . . . . . . . . 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.d	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
23	22	ssrab3 4007	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐷 ⊆ (ℕ0 ↑m 𝐼)
24	23	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ⊆ (ℕ0 ↑m 𝐼))
25	24	sselda 3908	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ (ℕ0 ↑m 𝐼))
26	25	elmaprd 8873	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓:𝐼⟶ℕ0)
27	26	freld 6716	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → Rel 𝑓)
28	26	ffnd 6710	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 Fn 𝐼)
29	28	fndmd 6644	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → dom 𝑓 = 𝐼)
30		esplyind.j	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐽 = (𝐼 ∖ {𝑌})
31	30	uneq1i 4163	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 ∪ {𝑌}) = ((𝐼 ∖ {𝑌}) ∪ {𝑌})
32		esplyind.y	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑌 ∈ 𝐼)
33	32	snssd 4743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝑌} ⊆ 𝐼)
34		undifr 4438	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑌} ⊆ 𝐼 ↔ ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
35	33, 34	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
36	31, 35	eqtr2id 2808	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐼 = (𝐽 ∪ {𝑌}))
37	36	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝐼 = (𝐽 ∪ {𝑌}))
38	29, 37	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → dom 𝑓 = (𝐽 ∪ {𝑌}))
39		reldmun 6022	. . . . . . . . . . . . . . . 16 ⊢ ((Rel 𝑓 ∧ dom 𝑓 = (𝐽 ∪ {𝑌})) → 𝑓 = ((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})))
40	27, 38, 39	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 = ((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})))
41	40	rneqd 5919	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ran 𝑓 = ran ((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})))
42		rnun 6135	. . . . . . . . . . . . . 14 ⊢ ran ((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})) = (ran (𝑓 ↾ 𝐽) ∪ ran (𝑓 ↾ {𝑌}))
43	41, 42	eqtr2di 2812	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (ran (𝑓 ↾ 𝐽) ∪ ran (𝑓 ↾ {𝑌})) = ran 𝑓)
44	28	fnfund 6640	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → Fun 𝑓)
45	32	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑌 ∈ 𝐼)
46	45, 29	eleqtrrd 2863	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑌 ∈ dom 𝑓)
47		rnressnsn 33318	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝑓 ∧ 𝑌 ∈ dom 𝑓) → ran (𝑓 ↾ {𝑌}) = {(𝑓‘𝑌)})
48	44, 46, 47	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ran (𝑓 ↾ {𝑌}) = {(𝑓‘𝑌)})
49	48	uneq2d 4167	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (ran (𝑓 ↾ 𝐽) ∪ ran (𝑓 ↾ {𝑌})) = (ran (𝑓 ↾ 𝐽) ∪ {(𝑓‘𝑌)}))
50	43, 49	eqtr3d 2797	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ran 𝑓 = (ran (𝑓 ↾ 𝐽) ∪ {(𝑓‘𝑌)}))
51	50	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ran 𝑓 = (ran (𝑓 ↾ 𝐽) ∪ {(𝑓‘𝑌)}))
52		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓‘𝑌) = 0)
53	52	sneqd 4592	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → {(𝑓‘𝑌)} = {0})
54	53	uneq2d 4167	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (ran (𝑓 ↾ 𝐽) ∪ {(𝑓‘𝑌)}) = (ran (𝑓 ↾ 𝐽) ∪ {0}))
55	51, 54	eqtrd 2795	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ran 𝑓 = (ran (𝑓 ↾ 𝐽) ∪ {0}))
56	55	sseq1d 3939	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (ran 𝑓 ⊆ {0, 1} ↔ (ran (𝑓 ↾ 𝐽) ∪ {0}) ⊆ {0, 1}))
57	21, 56	bitr4id 293	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ↔ ran 𝑓 ⊆ {0, 1}))
58	40	oveq1d 7435	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 supp 0) = (((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})) supp 0))
59	25	resexd 6016	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 ↾ 𝐽) ∈ V)
60	25	resexd 6016	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 ↾ {𝑌}) ∈ V)
61		0nn0 12624	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
62	61	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 0 ∈ ℕ0)
63	59, 60, 62	suppun2 33324	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (((𝑓 ↾ 𝐽) ∪ (𝑓 ↾ {𝑌})) supp 0) = (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)))
64	58, 63	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 supp 0) = (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)))
65	64	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 supp 0) = (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)))
66		fnressn 7162	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 Fn 𝐼 ∧ 𝑌 ∈ 𝐼) → (𝑓 ↾ {𝑌}) = {⟨𝑌, (𝑓‘𝑌)⟩})
67	28, 45, 66	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 ↾ {𝑌}) = {⟨𝑌, (𝑓‘𝑌)⟩})
68	67	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ((𝑓 ↾ {𝑌}) supp 0) = ({⟨𝑌, (𝑓‘𝑌)⟩} supp 0))
69	26, 45	ffvelcdmd 7085	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓‘𝑌) ∈ ℕ0)
70		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑌, (𝑓‘𝑌)⟩} = {⟨𝑌, (𝑓‘𝑌)⟩}
71	70	suppsnop 8198	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ 𝐼 ∧ (𝑓‘𝑌) ∈ ℕ0 ∧ 0 ∈ ℕ0) → ({⟨𝑌, (𝑓‘𝑌)⟩} supp 0) = if((𝑓‘𝑌) = 0, ∅, {𝑌}))
72	45, 69, 62, 71	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ({⟨𝑌, (𝑓‘𝑌)⟩} supp 0) = if((𝑓‘𝑌) = 0, ∅, {𝑌}))
73	68, 72	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ((𝑓 ↾ {𝑌}) supp 0) = if((𝑓‘𝑌) = 0, ∅, {𝑌}))
74	73	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((𝑓 ↾ {𝑌}) supp 0) = if((𝑓‘𝑌) = 0, ∅, {𝑌}))
75	52	iftrued 4489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → if((𝑓‘𝑌) = 0, ∅, {𝑌}) = ∅)
76	74, 75	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((𝑓 ↾ {𝑌}) supp 0) = ∅)
77	76	uneq2d 4167	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)) = (((𝑓 ↾ 𝐽) supp 0) ∪ ∅))
78		un0 4343	. . . . . . . . . . 11 ⊢ (((𝑓 ↾ 𝐽) supp 0) ∪ ∅) = ((𝑓 ↾ 𝐽) supp 0)
79	77, 78	eqtrdi 2811	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)) = ((𝑓 ↾ 𝐽) supp 0))
80	65, 79	eqtr2d 2796	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((𝑓 ↾ 𝐽) supp 0) = (𝑓 supp 0))
81	80	fveqeq2d 6893	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾 ↔ (♯‘(𝑓 supp 0)) = 𝐾))
82	57, 81	anbi12d 644	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾) ↔ (ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾)))
83	82	ifbid 4505	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
84	17, 83	eqtrd 2795	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((0g‘𝑅)(+g‘𝑅)if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
85	6	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑅 ∈ Grp)
86		esplyind.w	. . . . . . . . . 10 ⊢ 𝑊 = (𝐼 mPoly 𝑅)
87		eqid 2760	. . . . . . . . . 10 ⊢ (Base‘𝑊) = (Base‘𝑊)
88	22	psrbasfsupp 34189	. . . . . . . . . 10 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
89		esplyind.g	. . . . . . . . . . . 12 ⊢ 𝐺 = ((𝐼extendVars𝑅)‘𝑌)
90	89	fveq1i 6886	. . . . . . . . . . 11 ⊢ (𝐺‘(𝐸‘(𝐾 − 1))) = (((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘(𝐾 − 1)))
91		esplyind.i	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ∈ Fin)
92		eqid 2760	. . . . . . . . . . . . 13 ⊢ (Base‘(𝐽 mPoly 𝑅)) = (Base‘(𝐽 mPoly 𝑅))
93	86	fveq2i 6888	. . . . . . . . . . . . 13 ⊢ (Base‘𝑊) = (Base‘(𝐼 mPoly 𝑅))
94	22, 4, 91, 5, 2, 30, 92, 32, 93	extvfvalf 34215	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐼extendVars𝑅)‘𝑌):(Base‘(𝐽 mPoly 𝑅))⟶(Base‘𝑊))
95		esplyind.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝐽eSymPoly𝑅)
96	95	fveq1i 6886	. . . . . . . . . . . . 13 ⊢ (𝐸‘(𝐾 − 1)) = ((𝐽eSymPoly𝑅)‘(𝐾 − 1))
97		esplyind.1	. . . . . . . . . . . . . 14 ⊢ 𝐶 = {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}
98		difssd 4073	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 ∖ {𝑌}) ⊆ 𝐼)
99	30, 98	eqsstrid 3946	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐽 ⊆ 𝐼)
100	91, 99	ssfid 9263	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐽 ∈ Fin)
101		esplyind.k	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ (1...(♯‘𝐼)))
102		elfznn 13690	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...(♯‘𝐼)) → 𝐾 ∈ ℕ)
103		nnm1nn0 12650	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ0)
104	101, 102, 103	3syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾 − 1) ∈ ℕ0)
105	97, 100, 5, 104, 92	esplympl 34245	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘(𝐾 − 1)) ∈ (Base‘(𝐽 mPoly 𝑅)))
106	96, 105	eqeltrid 2864	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘(𝐾 − 1)) ∈ (Base‘(𝐽 mPoly 𝑅)))
107	94, 106	ffvelcdmd 7085	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘(𝐾 − 1))) ∈ (Base‘𝑊))
108	90, 107	eqeltrid 2864	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘(𝐸‘(𝐾 − 1))) ∈ (Base‘𝑊))
109	86, 2, 87, 88, 108	mplelf 22310	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘(𝐸‘(𝐾 − 1))):𝐷⟶(Base‘𝑅))
110	109	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (𝐺‘(𝐸‘(𝐾 − 1))):𝐷⟶(Base‘𝑅))
111		simplr 781	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑓 ∈ 𝐷)
112		indf 12329	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ Fin ∧ {𝑌} ⊆ 𝐼) → ((𝟭‘𝐼)‘{𝑌}):𝐼⟶{0, 1})
113	91, 33, 112	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝟭‘𝐼)‘{𝑌}):𝐼⟶{0, 1})
114	61	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℕ0)
115		1nn0 12625	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
116	115	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℕ0)
117	114, 116	prssd 4777	. . . . . . . . . . 11 ⊢ (𝜑 → {0, 1} ⊆ ℕ0)
118	113, 117	fssd 6727	. . . . . . . . . 10 ⊢ (𝜑 → ((𝟭‘𝐼)‘{𝑌}):𝐼⟶ℕ0)
119	118	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝟭‘𝐼)‘{𝑌}):𝐼⟶ℕ0)
120	91	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝐼 ∈ Fin)
121	120	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 𝐼 ∈ Fin)
122	33	ad4antr 745	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → {𝑌} ⊆ 𝐼)
123		velsn 4596	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑌} ↔ 𝑥 = 𝑌)
124	123	bilanri 512	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 𝑥 ∈ {𝑌})
125		ind1 12332	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ Fin ∧ {𝑌} ⊆ 𝐼 ∧ 𝑥 ∈ {𝑌}) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = 1)
126	121, 122, 124, 125	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = 1)
127	26	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 𝑓:𝐼⟶ℕ0)
128		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 𝑥 ∈ 𝐼)
129	127, 128	ffvelcdmd 7085	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (𝑓‘𝑥) ∈ ℕ0)
130		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 𝑥 = 𝑌)
131	130	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (𝑓‘𝑥) = (𝑓‘𝑌))
132		simpllr 788	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → ¬ (𝑓‘𝑌) = 0)
133	132	neqned 2962	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (𝑓‘𝑌) ≠ 0)
134	131, 133	eqnetrd 3022	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (𝑓‘𝑥) ≠ 0)
135		elnnne0 12623	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑥) ∈ ℕ ↔ ((𝑓‘𝑥) ∈ ℕ0 ∧ (𝑓‘𝑥) ≠ 0))
136	129, 134, 135	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (𝑓‘𝑥) ∈ ℕ)
137	136	nnge1d 12389	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → 1 ≤ (𝑓‘𝑥))
138	126, 137	eqbrtrd 5126	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 = 𝑌) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) ≤ (𝑓‘𝑥))
139	120	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → 𝐼 ∈ Fin)
140	33	ad4antr 745	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → {𝑌} ⊆ 𝐼)
141		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → 𝑥 ∈ 𝐼)
142		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → 𝑥 ≠ 𝑌)
143	141, 142	eldifsnd 4746	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → 𝑥 ∈ (𝐼 ∖ {𝑌}))
144		ind0 12333	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ Fin ∧ {𝑌} ⊆ 𝐼 ∧ 𝑥 ∈ (𝐼 ∖ {𝑌})) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = 0)
145	139, 140, 143, 144	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = 0)
146	26	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑓:𝐼⟶ℕ0)
147	146	ffvelcdmda 7084	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) ∈ ℕ0)
148	147	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → (𝑓‘𝑥) ∈ ℕ0)
149	148	nn0ge0d 12673	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → 0 ≤ (𝑓‘𝑥))
150	145, 149	eqbrtrd 5126	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) ∧ 𝑥 ≠ 𝑌) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) ≤ (𝑓‘𝑥))
151	138, 150	pm2.61dane 3042	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) ≤ (𝑓‘𝑥))
152	151	ralrimiva 3154	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ∀𝑥 ∈ 𝐼 (((𝟭‘𝐼)‘{𝑌})‘𝑥) ≤ (𝑓‘𝑥))
153	119	ffnd 6710	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
154	28	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑓 Fn 𝐼)
155		inidm 4123	. . . . . . . . . . 11 ⊢ (𝐼 ∩ 𝐼) = 𝐼
156		eqidd 2761	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = (((𝟭‘𝐼)‘{𝑌})‘𝑥))
157		eqidd 2761	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ 𝑥 ∈ 𝐼) → (𝑓‘𝑥) = (𝑓‘𝑥))
158	153, 154, 120, 120, 155, 156, 157	ofrfval 7703	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (((𝟭‘𝐼)‘{𝑌}) ∘r ≤ 𝑓 ↔ ∀𝑥 ∈ 𝐼 (((𝟭‘𝐼)‘{𝑌})‘𝑥) ≤ (𝑓‘𝑥)))
159	152, 158	mpbird 260	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝟭‘𝐼)‘{𝑌}) ∘r ≤ 𝑓)
160	88	psrbagcon 22238	. . . . . . . . . 10 ⊢ ((𝑓 ∈ 𝐷 ∧ ((𝟭‘𝐼)‘{𝑌}):𝐼⟶ℕ0 ∧ ((𝟭‘𝐼)‘{𝑌}) ∘r ≤ 𝑓) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ 𝐷 ∧ (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∘r ≤ 𝑓))
161	160	simpld 500	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝐷 ∧ ((𝟭‘𝐼)‘{𝑌}):𝐼⟶ℕ0 ∧ ((𝟭‘𝐼)‘{𝑌}) ∘r ≤ 𝑓) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ 𝐷)
162	111, 119, 159, 161	syl3anc 1398	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ 𝐷)
163	110, 162	ffvelcdmd 7085	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) ∈ (Base‘𝑅))
164	2, 3, 4, 85, 163	grpridd 19186	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))(+g‘𝑅)(0g‘𝑅)) = ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))
165	90	fveq1i 6886	. . . . . . . 8 ⊢ ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) = ((((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))
166	165	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) = ((((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))
167	5	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑅 ∈ Ring)
168	32	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → 𝑌 ∈ 𝐼)
169	106	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (𝐸‘(𝐾 − 1)) ∈ (Base‘(𝐽 mPoly 𝑅)))
170	22, 4, 120, 167, 168, 30, 92, 169, 162	extvfvv 34212	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) = if(((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0, ((𝐸‘(𝐾 − 1))‘((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)), (0g‘𝑅)))
171	97, 100, 5, 104, 4, 8	esplyfval3 34250	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘(𝐾 − 1)) = (𝑧 ∈ 𝐶 ↦ if((ran 𝑧 ⊆ {0, 1} ∧ (♯‘(𝑧 supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅))))
172	96, 171	eqtrid 2807	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘(𝐾 − 1)) = (𝑧 ∈ 𝐶 ↦ if((ran 𝑧 ⊆ {0, 1} ∧ (♯‘(𝑧 supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅))))
173	172	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝐸‘(𝐾 − 1)) = (𝑧 ∈ 𝐶 ↦ if((ran 𝑧 ⊆ {0, 1} ∧ (♯‘(𝑧 supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅))))
174	43	ad4antr 745	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → (ran (𝑓 ↾ 𝐽) ∪ ran (𝑓 ↾ {𝑌})) = ran 𝑓)
175		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽))
176	113	ffnd 6710	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
177	176	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
178	91	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝐼 ∈ Fin)
179	28, 177, 178, 178, 155	offn 7706	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) Fn 𝐼)
180	179	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) Fn 𝐼)
181	99	ad4antr 745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → 𝐽 ⊆ 𝐼)
182	180, 181	fnssresd 6663	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) Fn 𝐽)
183		fneq1 6630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) → (𝑧 Fn 𝐽 ↔ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) Fn 𝐽))
184	183	biimpar 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) Fn 𝐽) → 𝑧 Fn 𝐽)
185	175, 182, 184	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → 𝑧 Fn 𝐽)
186	28	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 𝑓 Fn 𝐼)
187	99	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 𝐽 ⊆ 𝐼)
188	186, 187	fnssresd 6663	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ↾ 𝐽) Fn 𝐽)
189	188	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → (𝑓 ↾ 𝐽) Fn 𝐽)
190		simplr 781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽))
191	190	fveq1d 6887	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (𝑧‘𝑥) = (((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)‘𝑥))
192		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐽)
193	192	fvresd 6905	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)‘𝑥) = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑥))
194	186	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑓 Fn 𝐼)
195	153	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
196	195	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
197	178	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 𝐼 ∈ Fin)
198	197	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝐼 ∈ Fin)
199	181	sselda 3908	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐼)
200		fnfvof 7710	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 Fn 𝐼 ∧ ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼) ∧ (𝐼 ∈ Fin ∧ 𝑥 ∈ 𝐼)) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑥) = ((𝑓‘𝑥) − (((𝟭‘𝐼)‘{𝑌})‘𝑥)))
201	194, 196, 198, 199, 200	syl22anc 852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑥) = ((𝑓‘𝑥) − (((𝟭‘𝐼)‘{𝑌})‘𝑥)))
202	33	ad5antr 747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → {𝑌} ⊆ 𝐼)
203	192, 30	eleqtrdi 2870	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ (𝐼 ∖ {𝑌}))
204	198, 202, 203, 144	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (((𝟭‘𝐼)‘{𝑌})‘𝑥) = 0)
205	204	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓‘𝑥) − (((𝟭‘𝐼)‘{𝑌})‘𝑥)) = ((𝑓‘𝑥) − 0))
206	146	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → 𝑓:𝐼⟶ℕ0)
207	206, 199	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (𝑓‘𝑥) ∈ ℕ0)
208	207	nn0cnd 12672	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (𝑓‘𝑥) ∈ ℂ)
209	208	subid1d 11661	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓‘𝑥) − 0) = (𝑓‘𝑥))
210	192	fvresd 6905	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓 ↾ 𝐽)‘𝑥) = (𝑓‘𝑥))
211	209, 210	eqtr4d 2798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓‘𝑥) − 0) = ((𝑓 ↾ 𝐽)‘𝑥))
212	201, 205, 211	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑥) = ((𝑓 ↾ 𝐽)‘𝑥))
213	191, 193, 212	3eqtrd 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ 𝑥 ∈ 𝐽) → (𝑧‘𝑥) = ((𝑓 ↾ 𝐽)‘𝑥))
214	185, 189, 213	eqfnfvd 7032	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → 𝑧 = (𝑓 ↾ 𝐽))
215	214	rneqd 5919	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → ran 𝑧 = ran (𝑓 ↾ 𝐽))
216	215	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran 𝑧 = ran (𝑓 ↾ 𝐽))
217		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran 𝑧 ⊆ {0, 1})
218	216, 217	eqsstrrd 3943	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran (𝑓 ↾ 𝐽) ⊆ {0, 1})
219	44	ad4antr 745	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → Fun 𝑓)
220	46	ad4antr 745	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → 𝑌 ∈ dom 𝑓)
221	219, 220, 47	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran (𝑓 ↾ {𝑌}) = {(𝑓‘𝑌)})
222	69	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓‘𝑌) ∈ ℕ0)
223	222	nn0cnd 12672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓‘𝑌) ∈ ℂ)
224	113, 32	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((𝟭‘𝐼)‘{𝑌})‘𝑌) ∈ {0, 1})
225	117, 224	sseldd 3909	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝟭‘𝐼)‘{𝑌})‘𝑌) ∈ ℕ0)
226	225	nn0cnd 12672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝟭‘𝐼)‘{𝑌})‘𝑌) ∈ ℂ)
227	226	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (((𝟭‘𝐼)‘{𝑌})‘𝑌) ∈ ℂ)
228	168	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 𝑌 ∈ 𝐼)
229		fnfvof 7710	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓 Fn 𝐼 ∧ ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼) ∧ (𝐼 ∈ Fin ∧ 𝑌 ∈ 𝐼)) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = ((𝑓‘𝑌) − (((𝟭‘𝐼)‘{𝑌})‘𝑌)))
230	186, 195, 197, 228, 229	syl22anc 852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = ((𝑓‘𝑌) − (((𝟭‘𝐼)‘{𝑌})‘𝑌)))
231		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0)
232	230, 231	eqtr3d 2797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓‘𝑌) − (((𝟭‘𝐼)‘{𝑌})‘𝑌)) = 0)
233	223, 227, 232	subeq0d 11681	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓‘𝑌) = (((𝟭‘𝐼)‘{𝑌})‘𝑌))
234		snidg 4617	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑌 ∈ 𝐼 → 𝑌 ∈ {𝑌})
235	32, 234	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑌 ∈ {𝑌})
236		ind1 12332	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ Fin ∧ {𝑌} ⊆ 𝐼 ∧ 𝑌 ∈ {𝑌}) → (((𝟭‘𝐼)‘{𝑌})‘𝑌) = 1)
237	91, 33, 235, 236	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝟭‘𝐼)‘{𝑌})‘𝑌) = 1)
238	237	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (((𝟭‘𝐼)‘{𝑌})‘𝑌) = 1)
239	233, 238	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓‘𝑌) = 1)
240	239	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → (𝑓‘𝑌) = 1)
241	240	sneqd 4592	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → {(𝑓‘𝑌)} = {1})
242	221, 241	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran (𝑓 ↾ {𝑌}) = {1})
243		snsspr2 4770	. . . . . . . . . . . . . . . 16 ⊢ {1} ⊆ {0, 1}
244	242, 243	eqsstrdi 3952	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran (𝑓 ↾ {𝑌}) ⊆ {0, 1})
245	218, 244	unssd 4190	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → (ran (𝑓 ↾ 𝐽) ∪ ran (𝑓 ↾ {𝑌})) ⊆ {0, 1})
246	174, 245	eqsstrrd 3943	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑧 ⊆ {0, 1}) → ran 𝑓 ⊆ {0, 1})
247	214	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑓 ⊆ {0, 1}) → 𝑧 = (𝑓 ↾ 𝐽))
248	247	rneqd 5919	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑓 ⊆ {0, 1}) → ran 𝑧 = ran (𝑓 ↾ 𝐽))
249		rnresss 6005	. . . . . . . . . . . . . . 15 ⊢ ran (𝑓 ↾ 𝐽) ⊆ ran 𝑓
250		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑓 ⊆ {0, 1}) → ran 𝑓 ⊆ {0, 1})
251	249, 250	sstrid 3919	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑓 ⊆ {0, 1}) → ran (𝑓 ↾ 𝐽) ⊆ {0, 1})
252	248, 251	eqsstrd 3942	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) ∧ ran 𝑓 ⊆ {0, 1}) → ran 𝑧 ⊆ {0, 1})
253	246, 252	impbida 813	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → (ran 𝑧 ⊆ {0, 1} ↔ ran 𝑓 ⊆ {0, 1}))
254	214	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → (𝑧 supp 0) = ((𝑓 ↾ 𝐽) supp 0))
255	254	fveqeq2d 6893	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → ((♯‘(𝑧 supp 0)) = (𝐾 − 1) ↔ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)))
256	253, 255	anbi12d 644	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → ((ran 𝑧 ⊆ {0, 1} ∧ (♯‘(𝑧 supp 0)) = (𝐾 − 1)) ↔ (ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1))))
257	256	ifbid 4505	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ 𝑧 = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) → if((ran 𝑧 ⊆ {0, 1} ∧ (♯‘(𝑧 supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅)))
258		breq1 5105	. . . . . . . . . . . 12 ⊢ (ℎ = ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) → (ℎ finSupp 0 ↔ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) finSupp 0))
259	23, 162	sselid 3906	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ (ℕ0 ↑m 𝐼))
260	259	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ (ℕ0 ↑m 𝐼))
261	260, 187	elmapssresd 8898	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽))
262		breq1 5105	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) → (ℎ finSupp 0 ↔ (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) finSupp 0))
263	162	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ 𝐷)
264	263, 22	eleqtrdi 2870	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
265	262, 264	elrabrd 3647	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) finSupp 0)
266	61	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 0 ∈ ℕ0)
267	265, 266	fsuppres 9388	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) finSupp 0)
268	258, 261, 267	elrabd 3646	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0})
269	268, 97	eleqtrrdi 2871	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽) ∈ 𝐶)
270	10	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (1r‘𝑅) ∈ (Base‘𝑅))
271	14	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (0g‘𝑅) ∈ (Base‘𝑅))
272	270, 271	ifcld 4528	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅)) ∈ (Base‘𝑅))
273	173, 257, 269, 272	fvmptd 7001	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝐸‘(𝐾 − 1))‘((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅)))
274		eqcom 2767	. . . . . . . . . . . . 13 ⊢ ((𝐾 − 1) = (♯‘((𝑓 ↾ 𝐽) supp 0)) ↔ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1))
275		fz1ssfz0 13760	. . . . . . . . . . . . . . . . . 18 ⊢ (1...(♯‘𝐼)) ⊆ (0...(♯‘𝐼))
276		fz0ssnn0 13759	. . . . . . . . . . . . . . . . . 18 ⊢ (0...(♯‘𝐼)) ⊆ ℕ0
277	275, 276	sstri 3917	. . . . . . . . . . . . . . . . 17 ⊢ (1...(♯‘𝐼)) ⊆ ℕ0
278	277, 101	sselid 3906	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
279	278	nn0cnd 12672	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ ℂ)
280	279	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 𝐾 ∈ ℂ)
281		1cnd 11305	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → 1 ∈ ℂ)
282		c0ex 11303	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ V
283	282	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 0 ∈ V)
284	26, 178, 283	fidmfisupp 9367	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 finSupp 0)
285	284, 283	fsuppres 9388	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓 ↾ 𝐽) finSupp 0)
286	285	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 ↾ 𝐽) finSupp 0)
287	286	fsuppimpd 9364	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ↾ 𝐽) supp 0) ∈ Fin)
288		hashcl 14503	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ↾ 𝐽) supp 0) ∈ Fin → (♯‘((𝑓 ↾ 𝐽) supp 0)) ∈ ℕ0)
289	287, 288	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (♯‘((𝑓 ↾ 𝐽) supp 0)) ∈ ℕ0)
290	289	nn0cnd 12672	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (♯‘((𝑓 ↾ 𝐽) supp 0)) ∈ ℂ)
291	280, 281, 290	subadd2d 11691	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝐾 − 1) = (♯‘((𝑓 ↾ 𝐽) supp 0)) ↔ ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1) = 𝐾))
292	274, 291	bitr3id 288	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1) ↔ ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1) = 𝐾))
293	64	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 supp 0) = (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)))
294	73	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ↾ {𝑌}) supp 0) = if((𝑓‘𝑌) = 0, ∅, {𝑌}))
295		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ¬ (𝑓‘𝑌) = 0)
296	295	iffalsed 4492	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → if((𝑓‘𝑌) = 0, ∅, {𝑌}) = {𝑌})
297	294, 296	eqtrd 2795	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ↾ {𝑌}) supp 0) = {𝑌})
298	297	uneq2d 4167	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (((𝑓 ↾ 𝐽) supp 0) ∪ ((𝑓 ↾ {𝑌}) supp 0)) = (((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌}))
299	293, 298	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (𝑓 supp 0) = (((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌}))
300	299	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (♯‘(𝑓 supp 0)) = (♯‘(((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌})))
301		suppssdm 8197	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ↾ 𝐽) supp 0) ⊆ dom (𝑓 ↾ 𝐽)
302		resdmss 6236	. . . . . . . . . . . . . . . . . 18 ⊢ dom (𝑓 ↾ 𝐽) ⊆ 𝐽
303	301, 302	sstri 3917	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ↾ 𝐽) supp 0) ⊆ 𝐽
304	303	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝑓 ↾ 𝐽) supp 0) ⊆ 𝐽)
305	30	eqimssi 3968	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐽 ⊆ (𝐼 ∖ {𝑌})
306		ssdifsn 4747	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 ⊆ (𝐼 ∖ {𝑌}) ↔ (𝐽 ⊆ 𝐼 ∧ ¬ 𝑌 ∈ 𝐽))
307	305, 306	mpbi 233	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ⊆ 𝐼 ∧ ¬ 𝑌 ∈ 𝐽)
308	307	simpri 491	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 𝑌 ∈ 𝐽
309	308	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ¬ 𝑌 ∈ 𝐽)
310	304, 309	ssneldd 3911	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ¬ 𝑌 ∈ ((𝑓 ↾ 𝐽) supp 0))
311		hashunsng 14539	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ∈ 𝐼 → ((((𝑓 ↾ 𝐽) supp 0) ∈ Fin ∧ ¬ 𝑌 ∈ ((𝑓 ↾ 𝐽) supp 0)) → (♯‘(((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌})) = ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1)))
312	311	imp 412	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 ∈ 𝐼 ∧ (((𝑓 ↾ 𝐽) supp 0) ∈ Fin ∧ ¬ 𝑌 ∈ ((𝑓 ↾ 𝐽) supp 0))) → (♯‘(((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌})) = ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1))
313	228, 287, 310, 312	syl12anc 850	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (♯‘(((𝑓 ↾ 𝐽) supp 0) ∪ {𝑌})) = ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1))
314	300, 313	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (♯‘(𝑓 supp 0)) = ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1))
315	314	eqeq1d 2762	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((♯‘(𝑓 supp 0)) = 𝐾 ↔ ((♯‘((𝑓 ↾ 𝐽) supp 0)) + 1) = 𝐾))
316	292, 315	bitr4d 285	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1) ↔ (♯‘(𝑓 supp 0)) = 𝐾))
317	316	anbi2d 642	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)) ↔ (ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾)))
318	317	ifbid 4505	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = (𝐾 − 1)), (1r‘𝑅), (0g‘𝑅)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
319	273, 318	eqtrd 2795	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ((𝐸‘(𝐾 − 1))‘((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
320		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ran 𝑓 ⊆ {0, 1})
321	154	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → 𝑓 Fn 𝐼)
322	168	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → 𝑌 ∈ 𝐼)
323	321, 322	fnfvelrnd 7082	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓‘𝑌) ∈ ran 𝑓)
324	320, 323	sseldd 3909	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓‘𝑌) ∈ {0, 1})
325		simpllr 788	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ¬ (𝑓‘𝑌) = 0)
326	325	neqned 2962	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓‘𝑌) ≠ 0)
327	69	nn0cnd 12672	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓‘𝑌) ∈ ℂ)
328	327	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓‘𝑌) ∈ ℂ)
329		1cnd 11305	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → 1 ∈ ℂ)
330		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0)
331	153	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ((𝟭‘𝐼)‘{𝑌}) Fn 𝐼)
332	120	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → 𝐼 ∈ Fin)
333	321, 331, 332, 322, 229	syl22anc 852	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = ((𝑓‘𝑌) − (((𝟭‘𝐼)‘{𝑌})‘𝑌)))
334	237	ad4antr 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (((𝟭‘𝐼)‘{𝑌})‘𝑌) = 1)
335	334	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ((𝑓‘𝑌) − (((𝟭‘𝐼)‘{𝑌})‘𝑌)) = ((𝑓‘𝑌) − 1))
336	333, 335	eqtrd 2795	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = ((𝑓‘𝑌) − 1))
337	336	eqeq1d 2762	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0 ↔ ((𝑓‘𝑌) − 1) = 0))
338	330, 337	mtbid 327	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ¬ ((𝑓‘𝑌) − 1) = 0)
339		subeq0 11587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓‘𝑌) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑓‘𝑌) − 1) = 0 ↔ (𝑓‘𝑌) = 1))
340	339	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑌) ∈ ℂ ∧ 1 ∈ ℂ) → (¬ ((𝑓‘𝑌) − 1) = 0 ↔ ¬ (𝑓‘𝑌) = 1))
341	340	biimpa 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝑓‘𝑌) ∈ ℂ ∧ 1 ∈ ℂ) ∧ ¬ ((𝑓‘𝑌) − 1) = 0) → ¬ (𝑓‘𝑌) = 1)
342	328, 329, 338, 341	syl21anc 851	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ¬ (𝑓‘𝑌) = 1)
343	342	neqned 2962	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓‘𝑌) ≠ 1)
344	326, 343	nelprd 4614	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) ∧ ran 𝑓 ⊆ {0, 1}) → ¬ (𝑓‘𝑌) ∈ {0, 1})
345	324, 344	pm2.65da 829	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ¬ ran 𝑓 ⊆ {0, 1})
346	345	intnanrd 495	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → ¬ (ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾))
347	346	iffalsed 4492	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) = (0g‘𝑅))
348	347	eqcomd 2766	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) ∧ ¬ ((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0) → (0g‘𝑅) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
349	319, 348	ifeqda 4518	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → if(((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))‘𝑌) = 0, ((𝐸‘(𝐾 − 1))‘((𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})) ↾ 𝐽)), (0g‘𝑅)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
350	166, 170, 349	3eqtrd 2799	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
351	164, 350	eqtrd 2795	. . . . 5 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ ¬ (𝑓‘𝑌) = 0) → (((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))(+g‘𝑅)(0g‘𝑅)) = if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
352	84, 351	ifeqda 4518	. . . 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‘𝑅)))
353	1, 352	eqtrid 2807	. . 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‘𝑅)))
354	353	mpteq2dva 5197	. 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‘𝑅))))
355		esplyind.p	. . . 4 ⊢ + = (+g‘𝑊)
356		esplyind.m	. . . . 5 ⊢ · = (.r‘𝑊)
357	86, 91, 5	mplringd 22335	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Ring)
358		esplyind.v	. . . . . 6 ⊢ 𝑉 = (𝐼 mVar 𝑅)
359	86, 358, 87, 91, 5, 32	mvrcl 22304	. . . . 5 ⊢ (𝜑 → (𝑉‘𝑌) ∈ (Base‘𝑊))
360	87, 356, 357, 359, 108	ringcld 20489	. . . 4 ⊢ (𝜑 → ((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) ∈ (Base‘𝑊))
361	89	fveq1i 6886	. . . . 5 ⊢ (𝐺‘(𝐸‘𝐾)) = (((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘𝐾))
362	95	fveq1i 6886	. . . . . . 7 ⊢ (𝐸‘𝐾) = ((𝐽eSymPoly𝑅)‘𝐾)
363	97, 100, 5, 278, 92	esplympl 34245	. . . . . . 7 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘𝐾) ∈ (Base‘(𝐽 mPoly 𝑅)))
364	362, 363	eqeltrid 2864	. . . . . 6 ⊢ (𝜑 → (𝐸‘𝐾) ∈ (Base‘(𝐽 mPoly 𝑅)))
365	94, 364	ffvelcdmd 7085	. . . . 5 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝑌)‘(𝐸‘𝐾)) ∈ (Base‘𝑊))
366	361, 365	eqeltrid 2864	. . . 4 ⊢ (𝜑 → (𝐺‘(𝐸‘𝐾)) ∈ (Base‘𝑊))
367	86, 87, 3, 355, 360, 366	mpladd 22321	. . 3 ⊢ (𝜑 → (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) + (𝐺‘(𝐸‘𝐾))) = (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) ∘f (+g‘𝑅)(𝐺‘(𝐸‘𝐾))))
368	358	fveq1i 6886	. . . . 5 ⊢ (𝑉‘𝑌) = ((𝐼 mVar 𝑅)‘𝑌)
369		eqid 2760	. . . . 5 ⊢ ((𝟭‘𝐼)‘{𝑌}) = ((𝟭‘𝐼)‘{𝑌})
370	86, 368, 87, 356, 4, 22, 369, 91, 32, 5, 108	mplmulmvr 34217	. . . 4 ⊢ (𝜑 → ((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))))
371	89	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐺 = ((𝐼extendVars𝑅)‘𝑌))
372	97, 100, 5, 278, 4, 8	esplyfval3 34250	. . . . . . 7 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘𝐾) = (𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))))
373	362, 372	eqtrid 2807	. . . . . 6 ⊢ (𝜑 → (𝐸‘𝐾) = (𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))))
374	371, 373	fveq12d 6892	. . . . 5 ⊢ (𝜑 → (𝐺‘(𝐸‘𝐾)) = (((𝐼extendVars𝑅)‘𝑌)‘(𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))))
375	372, 363	eqeltrrd 2861	. . . . . 6 ⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘(𝐽 mPoly 𝑅)))
376	22, 4, 91, 5, 32, 30, 92, 375	extvfv 34211	. . . . 5 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝑌)‘(𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, ((𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))‘(𝑓 ↾ 𝐽)), (0g‘𝑅))))
377		rneq 5917	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → ran 𝑔 = ran (𝑓 ↾ 𝐽))
378	377	sseq1d 3939	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → (ran 𝑔 ⊆ {0, 1} ↔ ran (𝑓 ↾ 𝐽) ⊆ {0, 1}))
379		oveq1 7427	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → (𝑔 supp 0) = ((𝑓 ↾ 𝐽) supp 0))
380	379	fveqeq2d 6893	. . . . . . . . . 10 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → ((♯‘(𝑔 supp 0)) = 𝐾 ↔ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾))
381	378, 380	anbi12d 644	. . . . . . . . 9 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → ((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾) ↔ (ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾)))
382	381	ifbid 4505	. . . . . . . 8 ⊢ (𝑔 = (𝑓 ↾ 𝐽) → if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) = if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
383		eqidd 2761	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))) = (𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))))
384		breq1 5105	. . . . . . . . . 10 ⊢ (ℎ = (𝑓 ↾ 𝐽) → (ℎ finSupp 0 ↔ (𝑓 ↾ 𝐽) finSupp 0))
385		nn0ex 12615	. . . . . . . . . . . 12 ⊢ ℕ0 ∈ V
386	385	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ℕ0 ∈ V)
387	100	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → 𝐽 ∈ Fin)
388	26	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → 𝑓:𝐼⟶ℕ0)
389	99	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → 𝐽 ⊆ 𝐼)
390	388, 389	fssresd 6749	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 ↾ 𝐽):𝐽⟶ℕ0)
391	386, 387, 390	elmapdd 8864	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽))
392	285	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 ↾ 𝐽) finSupp 0)
393	384, 391, 392	elrabd 3646	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 ↾ 𝐽) ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0})
394	393, 97	eleqtrrdi 2871	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (𝑓 ↾ 𝐽) ∈ 𝐶)
395		fvexd 6900	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (1r‘𝑅) ∈ V)
396		fvexd 6900	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → (0g‘𝑅) ∈ V)
397	395, 396	ifcld 4528	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)) ∈ V)
398	382, 383, 394, 397	fvmptd4 7018	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ (𝑓‘𝑌) = 0) → ((𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))‘(𝑓 ↾ 𝐽)) = if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))
399	398	ifeq1da 4513	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → if((𝑓‘𝑌) = 0, ((𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))‘(𝑓 ↾ 𝐽)), (0g‘𝑅)) = if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))
400	399	mpteq2dva 5197	. . . . 5 ⊢ (𝜑 → (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, ((𝑔 ∈ 𝐶 ↦ if((ran 𝑔 ⊆ {0, 1} ∧ (♯‘(𝑔 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)))‘(𝑓 ↾ 𝐽)), (0g‘𝑅))) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))))
401	374, 376, 400	3eqtrd 2799	. . . 4 ⊢ (𝜑 → (𝐺‘(𝐸‘𝐾)) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))))
402	370, 401	oveq12d 7438	. . 3 ⊢ (𝜑 → (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) ∘f (+g‘𝑅)(𝐺‘(𝐸‘𝐾))) = ((𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))) ∘f (+g‘𝑅)(𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))))
403		ovex 7453	. . . . . 6 ⊢ (ℕ0 ↑m 𝐼) ∈ V
404	22, 403	rabex2 5301	. . . . 5 ⊢ 𝐷 ∈ V
405	404	a1i 11	. . . 4 ⊢ (𝜑 → 𝐷 ∈ V)
406		nfv 1946	. . . . 5 ⊢ Ⅎ𝑓𝜑
407		fvexd 6900	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))) ∈ V)
408	14, 407	ifexd 4530	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))) ∈ V)
409		eqid 2760	. . . . 5 ⊢ (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌})))))
410	406, 408, 409	fnmptd 6680	. . . 4 ⊢ (𝜑 → (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))) Fn 𝐷)
411	15, 14	ifcld 4528	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)) ∈ (Base‘𝑅))
412		eqid 2760	. . . . 5 ⊢ (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))) = (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))
413	406, 411, 412	fnmptd 6680	. . . 4 ⊢ (𝜑 → (𝑓 ∈ 𝐷 ↦ if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅))) Fn 𝐷)
414		ofmpteq 7716	. . . 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‘𝑅)))))
415	405, 410, 413, 414	syl3anc 1398	. . 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‘𝑅)))))
416	367, 402, 415	3eqtrd 2799	. 2 ⊢ (𝜑 → (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) + (𝐺‘(𝐸‘𝐾))) = (𝑓 ∈ 𝐷 ↦ (if((𝑓‘𝑌) = 0, (0g‘𝑅), ((𝐺‘(𝐸‘(𝐾 − 1)))‘(𝑓 ∘f − ((𝟭‘𝐼)‘{𝑌}))))(+g‘𝑅)if((𝑓‘𝑌) = 0, if((ran (𝑓 ↾ 𝐽) ⊆ {0, 1} ∧ (♯‘((𝑓 ↾ 𝐽) supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅)), (0g‘𝑅)))))
417	22, 91, 5, 278, 4, 8	esplyfval3 34250	. 2 ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = (𝑓 ∈ 𝐷 ↦ if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), (1r‘𝑅), (0g‘𝑅))))
418	354, 416, 417	3eqtr4rd 2806	1 ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) + (𝐺‘(𝐸‘𝐾))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  {crab 3412  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045   ∪ cun 4149  ∅c0 4278  ifcif 4481  {csn 4584  {cpr 4586  ⟨cop 4834   class class class wbr 5102   ↦ cmpt 5185  dom cdm 5650  ran crn 5651   ↾ cres 5652  Rel wrel 5655  Fun wfun 6532   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420   ∘_f cof 7691   ∘_r cofr 7692   supp csupp 8179   ↑_m cmap 8850  Fincfn 8976   finSupp cfsupp 9356  ℂcc 11201  0cc0 11203  1c1 11204   + caddc 11206   ≤ cle 11347   − cmin 11544  𝟭cind 12323  ℕcn 12338  ℕ₀cn0 12609  ...cfz 13642  ♯chash 14477  Basecbs 17392  +_gcplusg 17433  ._rcmulr 17434  0_gc0g 17615  Grpcgrp 19149  1_rcur 20412  Ringcrg 20464   mVar cmvr 22218   mPoly cmpl 22219  extendVarscextv 34207  eSymPolycesply 34234

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280  ax-addf 11282  ax-mulf 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7693  df-ofr 7694  df-om 7878  df-1st 8001  df-2nd 8002  df-supp 8180  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-2o 8480  df-oadd 8483  df-er 8720  df-map 8852  df-pm 8853  df-ixp 8929  df-en 8977  df-dom 8978  df-sdom 8979  df-fin 8980  df-fsupp 9357  df-sup 9437  df-oi 9507  df-dju 9985  df-card 10023  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-div 11977  df-ind 12324  df-nn 12339  df-2 12408  df-3 12409  df-4 12410  df-5 12411  df-6 12412  df-7 12413  df-8 12414  df-9 12415  df-n0 12610  df-xnn0 12683  df-z 12697  df-dec 12818  df-uz 12969  df-rp 13124  df-fz 13643  df-fzo 13792  df-seq 14148  df-fac 14421  df-bc 14450  df-hash 14478  df-struct 17330  df-sets 17347  df-slot 17365  df-ndx 17377  df-base 17393  df-ress 17414  df-plusg 17446  df-mulr 17447  df-starv 17448  df-sca 17449  df-vsca 17450  df-ip 17451  df-tset 17452  df-ple 17453  df-ds 17455  df-unif 17456  df-hom 17457  df-cco 17458  df-0g 17617  df-gsum 17618  df-prds 17623  df-pws 17625  df-mre 17761  df-mrc 17762  df-acs 17764  df-mgm 18821  df-sgrp 18913  df-mnd 18929  df-mhm 18983  df-submnd 18984  df-grp 19152  df-minusg 19153  df-mulg 19283  df-subg 19338  df-ghm 19433  df-cntz 19536  df-cmn 20001  df-abl 20002  df-mgp 20366  df-rng 20380  df-ur 20413  df-ring 20466  df-cring 20467  df-rhm 20707  df-subrng 20803  df-subrg 20827  df-cnfld 21684  df-zring 21758  df-zrh 21814  df-psr 22222  df-mvr 22223  df-mpl 22224  df-extv 34208  df-esply 34236

This theorem is used by:  esplyindfv  34254