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	1	ssrab3	$$⊢D\subseteq {{\mathbb{N}}_0}^I$$
12	11	a1i	$$⊢\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\to D\subseteq {{\mathbb{N}}_0}^I$$
13	12	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)$$
14	13	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$$
15	14	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$$
16		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)}$$
17	5 6	symgbasf1o	$$⊢p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\to p:I\underset{1-1\; onto}{⟶}I$$
18	16 17	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$$
19		f1ofo	$$⊢p:I\underset{1-1\; onto}{⟶}I\to p:I\underset{onto}{⟶}I$$
20		forn	$$⊢p:I\underset{onto}{⟶}I\to \mathrm{ran}p=I$$
21	18 19 20	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$$
22	15 21	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$$
23		rncoeq	$$⊢\mathrm{dom}x=\mathrm{ran}p\to \mathrm{ran}\left(x\circ p\right)=\mathrm{ran}x$$
24	22 23	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$$
25	24	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)$$
26		f1ocnv	$$⊢p:I\underset{1-1\; onto}{⟶}I\to p^{-1}:I\underset{1-1\; onto}{⟶}I$$
27		f1of1	$$⊢p^{-1}:I\underset{1-1\; onto}{⟶}I\to p^{-1}:I\underset{1-1}{⟶}I$$
28	18 26 27	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$$
29		cnvimass	$$⊢x^{-1}\left[{\mathbb{N}}_0\setminus \left\{0\right\}\right]\subseteq \mathrm{dom}x$$
30	29 14	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$$
31	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}$$
32	28 30 31	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|$$
33		c0ex	$$⊢0\in \mathrm{V}$$
34	33	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}$$
35		simpr	$$⊢\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\to p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}$$
36		f1of	$$⊢p:I\underset{1-1\; onto}{⟶}I\to p:I⟶I$$
37	35 17 36	3syl	$$⊢\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\to p:I⟶I$$
38	37	adantr	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to p:I⟶I$$
39	14 38	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$$
40		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)$$
41	40	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]$$
42	31 34 39 41	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]$$
43		cnvco	$$⊢{\left(x\circ p\right)}^{-1}=p^{-1}\circ x^{-1}$$
44	43	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]$$
45		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]$$
46	44 45	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]$$
47	42 46	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]$$
48	47	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|$$
49		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)$$
50	49	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]$$
51	31 34 14 50	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]$$
52	51	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|$$
53	32 48 52	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|$$
54	53	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)$$
55	25 54	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)$$
56	55	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)$$
57	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}$$
58	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)$$
59		simpr	$$⊢\left(\left(\phi \wedge p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(I\right)}\right)\wedge x\in D\right)\to x\in D$$
60	59 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\}$$
61	5 6 31 16 60	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\}$$
62	61 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$$
63		eqid	$$⊢0_R=0_R$$
64		eqid	$$⊢1_R=1_R$$
65	1 31 57 58 62 63 64	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 |-
66	1 31 57 58 59 63 64	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 |-
67	56 65 66	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 |-
68	5 6 7 1 2 3 10 67	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 |-