Definition df-esply

Description: Define elementary symmetric polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Assertion	df-esply	Could not format assertion : No typesetting found for |- eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cesply	Could not format eSymPoly : No typesetting found for class eSymPoly with typecode class
1		vi	$$setvari$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		vk	$$setvark$$
5		cn0	$$class{\mathbb{N}}_0$$
6		czrh	$$class\mathrm{\mathbb{Z}RHom}$$
7	3	cv	$$setvarr$$
8	7 6	cfv	$$class\mathrm{\mathbb{Z}RHom}\left(r\right)$$
9		cind	$$class𝟙$$
10		vh	$$setvarh$$
11		cmap	$$class{\uparrow }_{𝑚}$$
12	1	cv	$$setvari$$
13	5 12 11	co	$$class\left({{\mathbb{N}}_0}^i\right)$$
14	10	cv	$$setvarh$$
15		cfsupp	$$class\mathrm{finSupp}$$
16		cc0	$$class0$$
17	14 16 15	wbr	$$wff{finSupp}_0\left(h\right)$$
18	17 10 13	crab	$$class\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}$$
19	18 9	cfv	$$class{𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}$$
20	12 9	cfv	$$class{𝟙}_i$$
21		vc	$$setvarc$$
22	12	cpw	$$class𝒫i$$
23		chash	$$class\left|.\right|$$
24	21	cv	$$setvarc$$
25	24 23	cfv	$$class\left|c\right|$$
26	4	cv	$$setvark$$
27	25 26	wceq	$$wff\left|c\right|=k$$
28	27 21 22	crab	$$class\left\{c\in 𝒫i|\left|c\right|=k\right\}$$
29	20 28	cima	$$class{𝟙}_i\left[\left\{c\in 𝒫i|\left|c\right|=k\right\}\right]$$
30	29 19	cfv	$$class{𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}\left({𝟙}_i\left[\left\{c\in 𝒫i|\left|c\right|=k\right\}\right]\right)$$
31	8 30	ccom	$$class\left(\mathrm{\mathbb{Z}RHom}\left(r\right)\circ {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}\left({𝟙}_i\left[\left\{c\in 𝒫i|\left|c\right|=k\right\}\right]\right)\right)$$
32	4 5 31	cmpt	$$class\left(k\in {\mathbb{N}}_0⟼\mathrm{\mathbb{Z}RHom}\left(r\right)\circ {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}\left({𝟙}_i\left[\left\{c\in 𝒫i|\left|c\right|=k\right\}\right]\right)\right)$$
33	1 3 2 2 32	cmpo	$$class\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(k\in {\mathbb{N}}_0⟼\mathrm{\mathbb{Z}RHom}\left(r\right)\circ {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}\left({𝟙}_i\left[\left\{c\in 𝒫i|\left|c\right|=k\right\}\right]\right)\right)\right)$$
34	0 33	wceq	Could not format eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) ) : No typesetting found for wff eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) ) with typecode wff