Definition df-sply

Description: Define symmetric polynomials. See splyval for a more readable expression. (Contributed by Thierry Arnoux, 11-Jan-2026)

	Ref	Expression
Assertion	df-sply	Could not format assertion : No typesetting found for |- SymPoly = ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csply	Could not format SymPoly : No typesetting found for class SymPoly with typecode class
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvari$$
6		cmpl	$$class\mathrm{mPoly}$$
7	3	cv	$$setvarr$$
8	5 7 6	co	$$class\left(i\mathrm{mPoly}r\right)$$
9	8 4	cfv	$$class{\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}$$
10		cfxp	Could not format FixPts : No typesetting found for class FixPts with typecode class
11		vd	$$setvard$$
12		csymg	$$class\mathrm{SymGrp}$$
13	5 12	cfv	$$class\mathrm{SymGrp}\left(i\right)$$
14	13 4	cfv	$$class{\mathrm{Base}}_{\mathrm{SymGrp}\left(i\right)}$$
15		vf	$$setvarf$$
16		vx	$$setvarx$$
17		vh	$$setvarh$$
18		cn0	$$class{\mathbb{N}}_0$$
19		cmap	$$class{\uparrow }_{𝑚}$$
20	18 5 19	co	$$class\left({{\mathbb{N}}_0}^i\right)$$
21	17	cv	$$setvarh$$
22		cfsupp	$$class\mathrm{finSupp}$$
23		cc0	$$class0$$
24	21 23 22	wbr	$$wff{finSupp}_0\left(h\right)$$
25	24 17 20	crab	$$class\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}$$
26	15	cv	$$setvarf$$
27	16	cv	$$setvarx$$
28	11	cv	$$setvard$$
29	27 28	ccom	$$class\left(x\circ d\right)$$
30	29 26	cfv	$$classf\left(x\circ d\right)$$
31	16 25 30	cmpt	$$class\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)$$
32	11 15 14 9 31	cmpo	$$class\left(d\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(i\right)},f\in {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\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)\right)$$
33	9 32 10	co	Could not format ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) : No typesetting found for class ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) with typecode class
34	1 3 2 2 33	cmpo	Could not format ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) : No typesetting found for class ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) with typecode class
35	0 34	wceq	Could not format SymPoly = ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) : No typesetting found for wff SymPoly = ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) with typecode wff