Theorem issply

Description: Conditions for being a symmetric polynomial. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	issply.s	$$⊢S=\mathrm{SymGrp}\left(I\right)$$
	issply.p	$$⊢P={\mathrm{Base}}_S$$
	issply.m	$$⊢M={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
	issply.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	issply.i	$$⊢\phi \to I\in V$$
	issply.r	$$⊢\phi \to R\in W$$
	issply.f	$$⊢\phi \to F\in M$$
	issply.1	$$⊢\left(\left(\phi \wedge p\in P\right)\wedge x\in D\right)\to F\left(x\circ p\right)=F\left(x\right)$$
Assertion	issply	Could not format assertion : No typesetting found for |- ( ph -> F e. ( I SymPoly R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		issply.s	$$⊢S=\mathrm{SymGrp}\left(I\right)$$
2		issply.p	$$⊢P={\mathrm{Base}}_S$$
3		issply.m	$$⊢M={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
4		issply.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
5		issply.i	$$⊢\phi \to I\in V$$
6		issply.r	$$⊢\phi \to R\in W$$
7		issply.f	$$⊢\phi \to F\in M$$
8		issply.1	$$⊢\left(\left(\phi \wedge p\in P\right)\wedge x\in D\right)\to F\left(x\circ p\right)=F\left(x\right)$$
9	8	mpteq2dva	$$⊢\left(\phi \wedge p\in P\right)\to \left(x\in D⟼F\left(x\circ p\right)\right)=\left(x\in D⟼F\left(x\right)\right)$$
10		coeq2	$$⊢c=d\to y\circ c=y\circ d$$
11	10	fveq2d	$$⊢c=d\to e\left(y\circ c\right)=e\left(y\circ d\right)$$
12	11	mpteq2dv	$$⊢c=d\to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼e\left(y\circ c\right)\right)=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼e\left(y\circ d\right)\right)$$
13		fveq1	$$⊢e=f\to e\left(y\circ d\right)=f\left(y\circ d\right)$$
14	13	mpteq2dv	$$⊢e=f\to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼e\left(y\circ d\right)\right)=\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(y\circ d\right)\right)$$
15	12 14	cbvmpov	$$⊢\left(c\in P,e\in M⟼\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼e\left(y\circ c\right)\right)\right)=\left(d\in P,f\in M⟼\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(y\circ d\right)\right)\right)$$
16		coeq1	$$⊢y=x\to y\circ d=x\circ d$$
17	16	fveq2d	$$⊢y=x\to f\left(y\circ d\right)=f\left(x\circ d\right)$$
18	17	cbvmptv	$$⊢\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(y\circ d\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)$$
19	18	a1i	$$⊢\left(d\in P\wedge f\in M\right)\to \left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(y\circ d\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)$$
20	19	mpoeq3ia	$$⊢\left(d\in P,f\in M⟼\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(y\circ d\right)\right)\right)=\left(d\in P,f\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)\right)$$
21	15 20	eqtri	$$⊢\left(c\in P,e\in M⟼\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼e\left(y\circ c\right)\right)\right)=\left(d\in P,f\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)\right)$$
22	21	a1i	$$⊢\left(\phi \wedge p\in P\right)\to \left(c\in P,e\in M⟼\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼e\left(y\circ c\right)\right)\right)=\left(d\in P,f\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)\right)$$
23	4	eqcomi	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}=D$$
24	23	a1i	$$⊢\left(d=p\wedge f=F\right)\to \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}=D$$
25		simpr	$$⊢\left(d=p\wedge f=F\right)\to f=F$$
26		coeq2	$$⊢d=p\to x\circ d=x\circ p$$
27	26	adantr	$$⊢\left(d=p\wedge f=F\right)\to x\circ d=x\circ p$$
28	25 27	fveq12d	$$⊢\left(d=p\wedge f=F\right)\to f\left(x\circ d\right)=F\left(x\circ p\right)$$
29	24 28	mpteq12dv	$$⊢\left(d=p\wedge f=F\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)=\left(x\in D⟼F\left(x\circ p\right)\right)$$
30	29	adantl	$$⊢\left(\left(\phi \wedge p\in P\right)\wedge \left(d=p\wedge f=F\right)\right)\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)=\left(x\in D⟼F\left(x\circ p\right)\right)$$
31		simpr	$$⊢\left(\phi \wedge p\in P\right)\to p\in P$$
32	7	adantr	$$⊢\left(\phi \wedge p\in P\right)\to F\in M$$
33		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
34	4 33	rabex2	$$⊢D\in \mathrm{V}$$
35	34	a1i	$$⊢\left(\phi \wedge p\in P\right)\to D\in \mathrm{V}$$
36	35	mptexd	$$⊢\left(\phi \wedge p\in P\right)\to \left(x\in D⟼F\left(x\circ p\right)\right)\in \mathrm{V}$$
37	22 30 31 32 36	ovmpod	$$⊢\left(\phi \wedge p\in P\right)\to p\left(c\in P,e\in M⟼\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼e\left(y\circ c\right)\right)\right)F=\left(x\in D⟼F\left(x\circ p\right)\right)$$
38		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
39		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
40	4	psrbasfsupp	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
41	38 39 3 40 32	mplelf	$$⊢\left(\phi \wedge p\in P\right)\to F:D⟶{\mathrm{Base}}_R$$
42	41	feqmptd	$$⊢\left(\phi \wedge p\in P\right)\to F=\left(x\in D⟼F\left(x\right)\right)$$
43	9 37 42	3eqtr4d	$$⊢\left(\phi \wedge p\in P\right)\to p\left(c\in P,e\in M⟼\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼e\left(y\circ c\right)\right)\right)F=F$$
44	43	ralrimiva	$$⊢\phi \to \forall p\in Pp\left(c\in P,e\in M⟼\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼e\left(y\circ c\right)\right)\right)F=F$$
45	1 2 3 21 5	mplvrpmga	$$⊢\phi \to \left(c\in P,e\in M⟼\left(y\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼e\left(y\circ c\right)\right)\right)\in \left(S\mathrm{GrpAct}M\right)$$
46	2 45 7	isfxp	Could not format ( ph -> ( F e. ( M FixPts ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) ) <-> A. p e. P ( p ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) F ) = F ) ) : No typesetting found for |- ( ph -> ( F e. ( M FixPts ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) ) <-> A. p e. P ( p ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) F ) = F ) ) with typecode |-
47	44 46	mpbird	Could not format ( ph -> F e. ( M FixPts ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) ) ) : No typesetting found for |- ( ph -> F e. ( M FixPts ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) ) ) with typecode |-
48	1 2 3 21 5 6	splyval	Could not format ( ph -> ( I SymPoly R ) = ( M FixPts ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( I SymPoly R ) = ( M FixPts ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) ) ) with typecode |-
49	47 48	eleqtrrd	Could not format ( ph -> F e. ( I SymPoly R ) ) : No typesetting found for |- ( ph -> F e. ( I SymPoly R ) ) with typecode |-