Theorem esplysply

Description: The K -th elementary symmetric polynomial is symmetric. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	esplyfv.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	esplyfv.i	$$⊢\phi \to I\in \mathrm{Fin}$$
	esplyfv.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	esplyfv.k	$$⊢\phi \to K\in \left(0\dots \left|I\right|\right)$$
Assertion	esplysply	Could not format assertion : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) e. ( I SymPoly R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		esplyfv.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
2		esplyfv.i	$$⊢\phi \to I\in \mathrm{Fin}$$
3		esplyfv.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		esplyfv.k	$$⊢\phi \to K\in \left(0\dots \left|I\right|\right)$$
5		eqid	$$⊢\mathrm{SymGrp}\left(I\right)=\mathrm{SymGrp}\left(I\right)$$
6		eqid	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}$$
7		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
8		elfznn0	$$⊢K\in \left(0\dots \left|I\right|\right)\to K\in {\mathbb{N}}_0$$
9	4 8	syl	$$⊢\phi \to K\in {\mathbb{N}}_0$$
10	1 2 3 9 7	esplympl	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPoly R ) ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPoly R ) ) ) with typecode |-
11	2	ad2antrr	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to I\in \mathrm{Fin}$$
12		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
13	12	a1i	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
14	1	ssrab3	$$⊢D\subseteq {{\mathbb{N}}_0}^I$$
15	14	a1i	$$⊢\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\to D\subseteq {{\mathbb{N}}_0}^I$$
16	15	sselda	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to x\in \left({{\mathbb{N}}_0}^I\right)$$
17	11 13 16	elmaprd	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to x:I⟶{\mathbb{N}}_0$$
18	17	fdmd	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \mathrm{dom}x=I$$
19		simplr	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}$$
20	5 6	symgbasf1o	$$⊢p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\to p:I\underset{1-1\; onto}{⟶}I$$
21	19 20	syl	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to p:I\underset{1-1\; onto}{⟶}I$$
22		f1ofo	$$⊢p:I\underset{1-1\; onto}{⟶}I\to p:I\underset{onto}{⟶}I$$
23		forn	$$⊢p:I\underset{onto}{⟶}I\to \mathrm{ran}p=I$$
24	21 22 23	3syl	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \mathrm{ran}p=I$$
25	18 24	eqtr4d	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \mathrm{dom}x=\mathrm{ran}p$$
26		rncoeq	$$⊢\mathrm{dom}x=\mathrm{ran}p\to \mathrm{ran}\left(x\circ p\right)=\mathrm{ran}x$$
27	25 26	syl	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \mathrm{ran}\left(x\circ p\right)=\mathrm{ran}x$$
28	27	sseq1d	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \left(\mathrm{ran}\left(x\circ p\right)\subseteq \left\{0,1\right\}\leftrightarrow \mathrm{ran}x\subseteq \left\{0,1\right\}\right)$$
29		f1ocnv	$$⊢p:I\underset{1-1\; onto}{⟶}I\to p^{-1}:I\underset{1-1\; onto}{⟶}I$$
30		f1of1	$$⊢p^{-1}:I\underset{1-1\; onto}{⟶}I\to p^{-1}:I\underset{1-1}{⟶}I$$
31	21 29 30	3syl	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to p^{-1}:I\underset{1-1}{⟶}I$$
32		cnvimass	$$⊢x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\subseteq \mathrm{dom}x$$
33	32 17	fssdm	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\subseteq I$$
34	31 33 11	hashimaf1	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \left|p^{-1}\left[x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right]\right|=\left|x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right|$$
35		c0ex	$$⊢0\in \mathrm{V}$$
36	35	a1i	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to 0\in \mathrm{V}$$
37		simpr	$$⊢\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\to p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}$$
38		f1of	$$⊢p:I\underset{1-1\; onto}{⟶}I\to p:I⟶I$$
39	37 20 38	3syl	$$⊢\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\to p:I⟶I$$
40	39	adantr	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to p:I⟶I$$
41	17 40	fcod	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \left(x\circ p\right):I⟶{\mathbb{N}}_0$$
42		fsuppeq	$$⊢\left(I\in \mathrm{Fin}\wedge 0\in \mathrm{V}\right)\to \left(\left(x\circ p\right):I⟶{\mathbb{N}}_0\to \left(x\circ p\right)\mathrm{supp}0={\left(x\circ p\right)}^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right)$$
43	42	imp	$$⊢\left(\left(I\in \mathrm{Fin}\wedge 0\in \mathrm{V}\right)\wedge \left(x\circ p\right):I⟶{\mathbb{N}}_0\right)\to \left(x\circ p\right)\mathrm{supp}0={\left(x\circ p\right)}^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]$$
44	11 36 41 43	syl21anc	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \left(x\circ p\right)\mathrm{supp}0={\left(x\circ p\right)}^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]$$
45		cnvco	$$⊢{\left(x\circ p\right)}^{-1}=p^{-1}\circ x^{-1}$$
46	45	imaeq1i	$$⊢{\left(x\circ p\right)}^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]=\left(p^{-1}\circ x^{-1}\right)\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]$$
47		imaco	$$⊢\left(p^{-1}\circ x^{-1}\right)\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]=p^{-1}\left[x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right]$$
48	46 47	eqtri	$$⊢{\left(x\circ p\right)}^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]=p^{-1}\left[x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right]$$
49	44 48	eqtrdi	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \left(x\circ p\right)\mathrm{supp}0=p^{-1}\left[x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right]$$
50	49	fveq2d	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \left|\left(x\circ p\right)\mathrm{supp}0\right|=\left|p^{-1}\left[x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right]\right|$$
51		fsuppeq	$$⊢\left(I\in \mathrm{Fin}\wedge 0\in \mathrm{V}\right)\to \left(x:I⟶{\mathbb{N}}_0\to x\mathrm{supp}0=x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right)$$
52	51	imp	$$⊢\left(\left(I\in \mathrm{Fin}\wedge 0\in \mathrm{V}\right)\wedge x:I⟶{\mathbb{N}}_0\right)\to x\mathrm{supp}0=x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]$$
53	11 36 17 52	syl21anc	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to x\mathrm{supp}0=x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]$$
54	53	fveq2d	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \left|x\mathrm{supp}0\right|=\left|x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\right|$$
55	34 50 54	3eqtr4d	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \left|\left(x\circ p\right)\mathrm{supp}0\right|=\left|x\mathrm{supp}0\right|$$
56	55	eqeq1d	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \left(\left|\left(x\circ p\right)\mathrm{supp}0\right|=K\leftrightarrow \left|x\mathrm{supp}0\right|=K\right)$$
57	28 56	anbi12d	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to \left(\left(\mathrm{ran}\left(x\circ p\right)\subseteq \left\{0,1\right\}\wedge \left|\left(x\circ p\right)\mathrm{supp}0\right|=K\right)\leftrightarrow \left(\mathrm{ran}x\subseteq \left\{0,1\right\}\wedge \left|x\mathrm{supp}0\right|=K\right)\right)$$
58	57	ifbid	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to if\left(\left(\mathrm{ran}\left(x\circ p\right)\subseteq \left\{0,1\right\}\wedge \left|\left(x\circ p\right)\mathrm{supp}0\right|=K\right),1_R,0_R\right)=if\left(\left(\mathrm{ran}x\subseteq \left\{0,1\right\}\wedge \left|x\mathrm{supp}0\right|=K\right),1_R,0_R\right)$$
59	3	ad2antrr	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to R\in \mathrm{Ring}$$
60	4	ad2antrr	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to K\in \left(0\dots \left|I\right|\right)$$
61		simpr	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to x\in D$$
62	61 1	eleqtrdi	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
63	5 6 11 19 62	mplvrpmlem	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to x\circ p\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
64	63 1	eleqtrrdi	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to x\circ p\in D$$
65		eqid	$$⊢0_R=0_R$$
66		eqid	$$⊢1_R=1_R$$
67	1 11 59 60 64 65 66	esplyfv	Could not format ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` ( x o. p ) ) = if ( ( ran ( x o. p ) C_ { 0 , 1 } /\ ( # ` ( ( x o. p ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) : No typesetting found for |- ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` ( x o. p ) ) = if ( ( ran ( x o. p ) C_ { 0 , 1 } /\ ( # ` ( ( x o. p ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) with typecode |-
68	1 11 59 60 61 65 66	esplyfv	Could not format ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` x ) = if ( ( ran x C_ { 0 , 1 } /\ ( # ` ( x supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) : No typesetting found for |- ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` x ) = if ( ( ran x C_ { 0 , 1 } /\ ( # ` ( x supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) with typecode |-
69	58 67 68	3eqtr4d	Could not format ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` ( x o. p ) ) = ( ( ( I eSymPoly R ) ` K ) ` x ) ) : No typesetting found for |- ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` ( x o. p ) ) = ( ( ( I eSymPoly R ) ` K ) ` x ) ) with typecode |-
70	5 6 7 1 2 3 10 69	issply	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) e. ( I SymPoly R ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) e. ( I SymPoly R ) ) with typecode |-