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	$$⊢B={\mathrm{Base}}_R$$
	esplyfvn.2	$$⊢\underset{\dot{}}{+}={+}_R$$
	esplyfvn.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	esplyfvn.4	$$⊢Q=I\mathrm{eval}R$$
	esplyfvn.5	$$⊢O=J\mathrm{eval}R$$
	esplyfvn.6	No typesetting found for |- E = ( I eSymPoly R ) with typecode |-
	esplyfvn.7	No typesetting found for |- F = ( J eSymPoly R ) with typecode |-
	esplyfvn.8	$$⊢H=\left|I\right|$$
	esplyfvn.9	$$⊢K=\left|J\right|$$
	esplyfvn.10	$$⊢J=I\setminus \left\{Y\right\}$$
	esplyfvn.11	$$⊢\phi \to I\in \mathrm{Fin}$$
	esplyfvn.12	$$⊢\phi \to R\in \mathrm{CRing}$$
	esplyfvn.13	$$⊢\phi \to Y\in I$$
	esplyfvn.14	$$⊢\phi \to Z:I⟶B$$
Assertion	esplyfvn	$$⊢\phi \to Q\left(E\left(H\right)\right)\left(Z\right)=Z\left(Y\right)\underset{\dot{}}{·}O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)$$

Proof

Step	Hyp	Ref	Expression
1		esplyfvn.1	$$⊢B={\mathrm{Base}}_R$$
2		esplyfvn.2	$$⊢\underset{\dot{}}{+}={+}_R$$
3		esplyfvn.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		esplyfvn.4	$$⊢Q=I\mathrm{eval}R$$
5		esplyfvn.5	$$⊢O=J\mathrm{eval}R$$
6		esplyfvn.6	Could not format E = ( I eSymPoly R ) : No typesetting found for |- E = ( I eSymPoly R ) with typecode |-
7		esplyfvn.7	Could not format F = ( J eSymPoly R ) : No typesetting found for |- F = ( J eSymPoly R ) with typecode |-
8		esplyfvn.8	$$⊢H=\left|I\right|$$
9		esplyfvn.9	$$⊢K=\left|J\right|$$
10		esplyfvn.10	$$⊢J=I\setminus \left\{Y\right\}$$
11		esplyfvn.11	$$⊢\phi \to I\in \mathrm{Fin}$$
12		esplyfvn.12	$$⊢\phi \to R\in \mathrm{CRing}$$
13		esplyfvn.13	$$⊢\phi \to Y\in I$$
14		esplyfvn.14	$$⊢\phi \to Z:I⟶B$$
15		hashdifsn	$$⊢\left(I\in \mathrm{Fin}\wedge Y\in I\right)\to \left|I\setminus \left\{Y\right\}\right|=\left|I\right|-1$$
16	11 13 15	syl2anc	$$⊢\phi \to \left|I\setminus \left\{Y\right\}\right|=\left|I\right|-1$$
17	10	fveq2i	$$⊢\left|J\right|=\left|I\setminus \left\{Y\right\}\right|$$
18	9 17	eqtri	$$⊢K=\left|I\setminus \left\{Y\right\}\right|$$
19	8	oveq1i	$$⊢H-1=\left|I\right|-1$$
20	16 18 19	3eqtr4g	$$⊢\phi \to K=H-1$$
21	20	oveq1d	$$⊢\phi \to K+1=H-1+1$$
22		hashcl	$$⊢I\in \mathrm{Fin}\to \left|I\right|\in {\mathbb{N}}_0$$
23	11 22	syl	$$⊢\phi \to \left|I\right|\in {\mathbb{N}}_0$$
24	8 23	eqeltrid	$$⊢\phi \to H\in {\mathbb{N}}_0$$
25	24	nn0cnd	$$⊢\phi \to H\in ℂ$$
26		1cnd	$$⊢\phi \to 1\in ℂ$$
27	25 26	npcand	$$⊢\phi \to H-1+1=H$$
28	21 27	eqtr2d	$$⊢\phi \to H=K+1$$
29	28	fveq2d	$$⊢\phi \to E\left(H\right)=E\left(K+1\right)$$
30	29	fveq2d	$$⊢\phi \to Q\left(E\left(H\right)\right)=Q\left(E\left(K+1\right)\right)$$
31	30	fveq1d	$$⊢\phi \to Q\left(E\left(H\right)\right)\left(Z\right)=Q\left(E\left(K+1\right)\right)\left(Z\right)$$
32		difssd	$$⊢\phi \to I\setminus \left\{Y\right\}\subseteq I$$
33	10 32	eqsstrid	$$⊢\phi \to J\subseteq I$$
34	11 33	ssfid	$$⊢\phi \to J\in \mathrm{Fin}$$
35		hashcl	$$⊢J\in \mathrm{Fin}\to \left|J\right|\in {\mathbb{N}}_0$$
36	34 35	syl	$$⊢\phi \to \left|J\right|\in {\mathbb{N}}_0$$
37	9 36	eqeltrid	$$⊢\phi \to K\in {\mathbb{N}}_0$$
38		nn0fz0	$$⊢K\in {\mathbb{N}}_0\leftrightarrow K\in \left(0\dots K\right)$$
39	37 38	sylib	$$⊢\phi \to K\in \left(0\dots K\right)$$
40	9	oveq2i	$$⊢\left(0\dots K\right)=\left(0\dots \left|J\right|\right)$$
41	39 40	eleqtrdi	$$⊢\phi \to K\in \left(0\dots \left|J\right|\right)$$
42		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}$$
43	6	fveq1i	Could not format ( E ` ( K + 1 ) ) = ( ( I eSymPoly R ) ` ( K + 1 ) ) : No typesetting found for |- ( E ` ( K + 1 ) ) = ( ( I eSymPoly R ) ` ( K + 1 ) ) with typecode |-
44	3 11 12 13 10 7 41 42 43 1 4 5 2 14	esplyindfv	$$⊢\phi \to Q\left(E\left(K+1\right)\right)\left(Z\right)=\left(Z\left(Y\right)\underset{\dot{}}{·}O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)\right)\underset{\dot{}}{+}O\left(F\left(K+1\right)\right)\left({Z\upharpoonright }_J\right)$$
45	7	fveq1i	Could not format ( F ` ( K + 1 ) ) = ( ( J eSymPoly R ) ` ( K + 1 ) ) : No typesetting found for |- ( F ` ( K + 1 ) ) = ( ( J eSymPoly R ) ` ( K + 1 ) ) with typecode |-
46	12	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
47	28 24	eqeltrrd	$$⊢\phi \to K+1\in {\mathbb{N}}_0$$
48		fzp1nel	$$⊢\neg K+1\in \left(0\dots K\right)$$
49	48	a1i	$$⊢\phi \to \neg K+1\in \left(0\dots K\right)$$
50	40	eleq2i	$$⊢K+1\in \left(0\dots K\right)\leftrightarrow K+1\in \left(0\dots \left|J\right|\right)$$
51	49 50	sylnib	$$⊢\phi \to \neg K+1\in \left(0\dots \left|J\right|\right)$$
52	47 51	eldifd	$$⊢\phi \to K+1\in \left({\mathbb{N}}_0\setminus \left(0\dots \left|J\right|\right)\right)$$
53		eqid	$$⊢0_{\left(J\mathrm{mPoly}R\right)}=0_{\left(J\mathrm{mPoly}R\right)}$$
54	42 34 46 52 53	esplyfval2	Could not format ( ph -> ( ( J eSymPoly R ) ` ( K + 1 ) ) = ( 0g ` ( J mPoly R ) ) ) : No typesetting found for |- ( ph -> ( ( J eSymPoly R ) ` ( K + 1 ) ) = ( 0g ` ( J mPoly R ) ) ) with typecode |-
55	45 54	eqtrid	$$⊢\phi \to F\left(K+1\right)=0_{\left(J\mathrm{mPoly}R\right)}$$
56		eqid	$$⊢J\mathrm{mPoly}R=J\mathrm{mPoly}R$$
57		eqid	$$⊢\mathrm{algSc}\left(J\mathrm{mPoly}R\right)=\mathrm{algSc}\left(J\mathrm{mPoly}R\right)$$
58		eqid	$$⊢0_R=0_R$$
59	56 57 58 53 34 46	mplascl0	$$⊢\phi \to \mathrm{algSc}\left(J\mathrm{mPoly}R\right)\left(0_R\right)=0_{\left(J\mathrm{mPoly}R\right)}$$
60	55 59	eqtr4d	$$⊢\phi \to F\left(K+1\right)=\mathrm{algSc}\left(J\mathrm{mPoly}R\right)\left(0_R\right)$$
61	60	fveq2d	$$⊢\phi \to O\left(F\left(K+1\right)\right)=O\left(\mathrm{algSc}\left(J\mathrm{mPoly}R\right)\left(0_R\right)\right)$$
62	61	fveq1d	$$⊢\phi \to O\left(F\left(K+1\right)\right)\left({Z\upharpoonright }_J\right)=O\left(\mathrm{algSc}\left(J\mathrm{mPoly}R\right)\left(0_R\right)\right)\left({Z\upharpoonright }_J\right)$$
63	12	crnggrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
64	1 58	grpidcl	$$⊢R\in \mathrm{Grp}\to 0_R\in B$$
65	63 64	syl	$$⊢\phi \to 0_R\in B$$
66	14 33	fssresd	$$⊢\phi \to \left({Z\upharpoonright }_J\right):J⟶B$$
67	5 56 1 57 34 12 65 66	evlscaval	$$⊢\phi \to O\left(\mathrm{algSc}\left(J\mathrm{mPoly}R\right)\left(0_R\right)\right)\left({Z\upharpoonright }_J\right)=0_R$$
68	62 67	eqtrd	$$⊢\phi \to O\left(F\left(K+1\right)\right)\left({Z\upharpoonright }_J\right)=0_R$$
69	68	oveq2d	$$⊢\phi \to \left(Z\left(Y\right)\underset{\dot{}}{·}O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)\right)\underset{\dot{}}{+}O\left(F\left(K+1\right)\right)\left({Z\upharpoonright }_J\right)=\left(Z\left(Y\right)\underset{\dot{}}{·}O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)\right)\underset{\dot{}}{+}{0}_R$$
70	14 13	ffvelcdmd	$$⊢\phi \to Z\left(Y\right)\in B$$
71		eqid	$$⊢{\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
72	7	fveq1i	Could not format ( F ` K ) = ( ( J eSymPoly R ) ` K ) : No typesetting found for |- ( F ` K ) = ( ( J eSymPoly R ) ` K ) with typecode |-
73	42 34 46 37 71	esplympl	Could not format ( ph -> ( ( J eSymPoly R ) ` K ) e. ( Base ` ( J mPoly R ) ) ) : No typesetting found for |- ( ph -> ( ( J eSymPoly R ) ` K ) e. ( Base ` ( J mPoly R ) ) ) with typecode |-
74	72 73	eqeltrid	$$⊢\phi \to F\left(K\right)\in {\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
75	1	fvexi	$$⊢B\in \mathrm{V}$$
76	75	a1i	$$⊢\phi \to B\in \mathrm{V}$$
77	76 34 66	elmapdd	$$⊢\phi \to {Z\upharpoonright }_J\in \left(B^J\right)$$
78	5 56 71 1 34 12 74 77	evlcl	$$⊢\phi \to O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)\in B$$
79	1 3 46 70 78	ringcld	$$⊢\phi \to Z\left(Y\right)\underset{\dot{}}{·}O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)\in B$$
80	1 2 58 63 79	grpridd	$$⊢\phi \to \left(Z\left(Y\right)\underset{\dot{}}{·}O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)\right)\underset{\dot{}}{+}{0}_R=Z\left(Y\right)\underset{\dot{}}{·}O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)$$
81	69 80	eqtrd	$$⊢\phi \to \left(Z\left(Y\right)\underset{\dot{}}{·}O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)\right)\underset{\dot{}}{+}O\left(F\left(K+1\right)\right)\left({Z\upharpoonright }_J\right)=Z\left(Y\right)\underset{\dot{}}{·}O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)$$
82	31 44 81	3eqtrd	$$⊢\phi \to Q\left(E\left(H\right)\right)\left(Z\right)=Z\left(Y\right)\underset{\dot{}}{·}O\left(F\left(K\right)\right)\left({Z\upharpoonright }_J\right)$$