Definition df-esply

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

	Ref	Expression
Assertion	df-esply	⊢ eSymPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cesply	⊢ eSymPoly
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		vr	⊢ 𝑟
4		vk	⊢ 𝑘
5		cn0	⊢ ℕ0
6		czrh	⊢ ℤRHom
7	3	cv	⊢ 𝑟
8	7 6	cfv	⊢ ( ℤRHom ‘ 𝑟 )
9		cind	⊢ 𝟭
10		vh	⊢ ℎ
11		cmap	⊢ ↑m
12	1	cv	⊢ 𝑖
13	5 12 11	co	⊢ ( ℕ0 ↑m 𝑖 )
14	10	cv	⊢ ℎ
15		cfsupp	⊢ finSupp
16		cc0	⊢ 0
17	14 16 15	wbr	⊢ ℎ finSupp 0
18	17 10 13	crab	⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 }
19	18 9	cfv	⊢ ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } )
20	12 9	cfv	⊢ ( 𝟭 ‘ 𝑖 )
21		vc	⊢ 𝑐
22	12	cpw	⊢ 𝒫 𝑖
23		chash	⊢ ♯
24	21	cv	⊢ 𝑐
25	24 23	cfv	⊢ ( ♯ ‘ 𝑐 )
26	4	cv	⊢ 𝑘
27	25 26	wceq	⊢ ( ♯ ‘ 𝑐 ) = 𝑘
28	27 21 22	crab	⊢ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 }
29	20 28	cima	⊢ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } )
30	29 19	cfv	⊢ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) )
31	8 30	ccom	⊢ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) )
32	4 5 31	cmpt	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) )
33	1 3 2 2 32	cmpo	⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )
34	0 33	wceq	⊢ eSymPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )