Theorem esplyfvn

Description: Express the last elementary symmetric polynomial, evaluated at a given set of points Z , in terms of the last elementary symmetric polynomial with one less variable. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	esplyfvn.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	esplyfvn.2	⊢ + = ( +g ‘ 𝑅 )
	esplyfvn.3	⊢ · = ( .r ‘ 𝑅 )
	esplyfvn.4	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
	esplyfvn.5	⊢ 𝑂 = ( 𝐽 eval 𝑅 )
	esplyfvn.6	⊢ 𝐸 = ( 𝐼 eSymPoly 𝑅 )
	esplyfvn.7	⊢ 𝐹 = ( 𝐽 eSymPoly 𝑅 )
	esplyfvn.8	⊢ 𝐻 = ( ♯ ‘ 𝐼 )
	esplyfvn.9	⊢ 𝐾 = ( ♯ ‘ 𝐽 )
	esplyfvn.10	⊢ 𝐽 = ( 𝐼 ∖ { 𝑌 } )
	esplyfvn.11	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	esplyfvn.12	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	esplyfvn.13	⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
	esplyfvn.14	⊢ ( 𝜑 → 𝑍 : 𝐼 ⟶ 𝐵 )
Assertion	esplyfvn	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐻 ) ) ‘ 𝑍 ) = ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		esplyfvn.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		esplyfvn.2	⊢ + = ( +g ‘ 𝑅 )
3		esplyfvn.3	⊢ · = ( .r ‘ 𝑅 )
4		esplyfvn.4	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
5		esplyfvn.5	⊢ 𝑂 = ( 𝐽 eval 𝑅 )
6		esplyfvn.6	⊢ 𝐸 = ( 𝐼 eSymPoly 𝑅 )
7		esplyfvn.7	⊢ 𝐹 = ( 𝐽 eSymPoly 𝑅 )
8		esplyfvn.8	⊢ 𝐻 = ( ♯ ‘ 𝐼 )
9		esplyfvn.9	⊢ 𝐾 = ( ♯ ‘ 𝐽 )
10		esplyfvn.10	⊢ 𝐽 = ( 𝐼 ∖ { 𝑌 } )
11		esplyfvn.11	⊢ ( 𝜑 → 𝐼 ∈ Fin )
12		esplyfvn.12	⊢ ( 𝜑 → 𝑅 ∈ CRing )
13		esplyfvn.13	⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
14		esplyfvn.14	⊢ ( 𝜑 → 𝑍 : 𝐼 ⟶ 𝐵 )
15		hashdifsn	⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ∈ 𝐼 ) → ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) ) = ( ( ♯ ‘ 𝐼 ) − 1 ) )
16	11 13 15	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) ) = ( ( ♯ ‘ 𝐼 ) − 1 ) )
17	10	fveq2i	⊢ ( ♯ ‘ 𝐽 ) = ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) )
18	9 17	eqtri	⊢ 𝐾 = ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) )
19	8	oveq1i	⊢ ( 𝐻 − 1 ) = ( ( ♯ ‘ 𝐼 ) − 1 )
20	16 18 19	3eqtr4g	⊢ ( 𝜑 → 𝐾 = ( 𝐻 − 1 ) )
21	20	oveq1d	⊢ ( 𝜑 → ( 𝐾 + 1 ) = ( ( 𝐻 − 1 ) + 1 ) )
22		hashcl	⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
23	11 22	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
24	8 23	eqeltrid	⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
25	24	nn0cnd	⊢ ( 𝜑 → 𝐻 ∈ ℂ )
26		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
27	25 26	npcand	⊢ ( 𝜑 → ( ( 𝐻 − 1 ) + 1 ) = 𝐻 )
28	21 27	eqtr2d	⊢ ( 𝜑 → 𝐻 = ( 𝐾 + 1 ) )
29	28	fveq2d	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ ( 𝐾 + 1 ) ) )
30	29	fveq2d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐸 ‘ 𝐻 ) ) = ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) )
31	30	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐻 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ‘ 𝑍 ) )
32		difssd	⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑌 } ) ⊆ 𝐼 )
33	10 32	eqsstrid	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
34	11 33	ssfid	⊢ ( 𝜑 → 𝐽 ∈ Fin )
35		hashcl	⊢ ( 𝐽 ∈ Fin → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
36	34 35	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
37	9 36	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
38		nn0fz0	⊢ ( 𝐾 ∈ ℕ0 ↔ 𝐾 ∈ ( 0 ... 𝐾 ) )
39	37 38	sylib	⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... 𝐾 ) )
40	9	oveq2i	⊢ ( 0 ... 𝐾 ) = ( 0 ... ( ♯ ‘ 𝐽 ) )
41	39 40	eleqtrdi	⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
42		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 }
43	6	fveq1i	⊢ ( 𝐸 ‘ ( 𝐾 + 1 ) ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) )
44	3 11 12 13 10 7 41 42 43 1 4 5 2 14	esplyindfv	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ‘ 𝑍 ) = ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )
45	7	fveq1i	⊢ ( 𝐹 ‘ ( 𝐾 + 1 ) ) = ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) )
46	12	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
47	28 24	eqeltrrd	⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ0 )
48		fzp1nel	⊢ ¬ ( 𝐾 + 1 ) ∈ ( 0 ... 𝐾 )
49	48	a1i	⊢ ( 𝜑 → ¬ ( 𝐾 + 1 ) ∈ ( 0 ... 𝐾 ) )
50	40	eleq2i	⊢ ( ( 𝐾 + 1 ) ∈ ( 0 ... 𝐾 ) ↔ ( 𝐾 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
51	49 50	sylnib	⊢ ( 𝜑 → ¬ ( 𝐾 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
52	47 51	eldifd	⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ( ℕ0 ∖ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) )
53		eqid	⊢ ( 0g ‘ ( 𝐽 mPoly 𝑅 ) ) = ( 0g ‘ ( 𝐽 mPoly 𝑅 ) )
54	42 34 46 52 53	esplyfval2	⊢ ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) ) = ( 0g ‘ ( 𝐽 mPoly 𝑅 ) ) )
55	45 54	eqtrid	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐾 + 1 ) ) = ( 0g ‘ ( 𝐽 mPoly 𝑅 ) ) )
56		eqid	⊢ ( 𝐽 mPoly 𝑅 ) = ( 𝐽 mPoly 𝑅 )
57		eqid	⊢ ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) = ( algSc ‘ ( 𝐽 mPoly 𝑅 ) )
58		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
59	56 57 58 53 34 46	mplascl0	⊢ ( 𝜑 → ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ ( 𝐽 mPoly 𝑅 ) ) )
60	55 59	eqtr4d	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐾 + 1 ) ) = ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 0g ‘ 𝑅 ) ) )
61	60	fveq2d	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) = ( 𝑂 ‘ ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 0g ‘ 𝑅 ) ) ) )
62	61	fveq1d	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) = ( ( 𝑂 ‘ ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 0g ‘ 𝑅 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) )
63	12	crnggrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
64	1 58	grpidcl	⊢ ( 𝑅 ∈ Grp → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
65	63 64	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
66	14 33	fssresd	⊢ ( 𝜑 → ( 𝑍 ↾ 𝐽 ) : 𝐽 ⟶ 𝐵 )
67	5 56 1 57 34 12 65 66	evlscaval	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 0g ‘ 𝑅 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) = ( 0g ‘ 𝑅 ) )
68	62 67	eqtrd	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) = ( 0g ‘ 𝑅 ) )
69	68	oveq2d	⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) = ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( 0g ‘ 𝑅 ) ) )
70	14 13	ffvelcdmd	⊢ ( 𝜑 → ( 𝑍 ‘ 𝑌 ) ∈ 𝐵 )
71		eqid	⊢ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
72	7	fveq1i	⊢ ( 𝐹 ‘ 𝐾 ) = ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝐾 )
73	42 34 46 37 71	esplympl	⊢ ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
74	72 73	eqeltrid	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
75	1	fvexi	⊢ 𝐵 ∈ V
76	75	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
77	76 34 66	elmapdd	⊢ ( 𝜑 → ( 𝑍 ↾ 𝐽 ) ∈ ( 𝐵 ↑m 𝐽 ) )
78	5 56 71 1 34 12 74 77	evlcl	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ∈ 𝐵 )
79	1 3 46 70 78	ringcld	⊢ ( 𝜑 → ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) ∈ 𝐵 )
80	1 2 58 63 79	grpridd	⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( 0g ‘ 𝑅 ) ) = ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )
81	69 80	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) = ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )
82	31 44 81	3eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐻 ) ) ‘ 𝑍 ) = ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )