Definition df-esply 34123

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

Assertion

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

Distinct variable group:   𝑖,𝑟,𝑘,ℎ,𝑐

Detailed syntax breakdown of Definition df-esply

Step	Hyp	Ref	Expression
1		cesply 34121	. 2 class eSymPoly
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3450	. . 3 class V
5		vk	. . . 4 setvar 𝑘
6		cn0 12575	. . . 4 class ℕ0
7	3	cv 1569	. . . . . 6 class 𝑟
8		czrh 21766	. . . . . 6 class ℤRHom
9	7, 8	cfv 6527	. . . . 5 class (ℤRHom‘𝑟)
10	2	cv 1569	. . . . . . . 8 class 𝑖
11		cind 12289	. . . . . . . 8 class 𝟭
12	10, 11	cfv 6527	. . . . . . 7 class (𝟭‘𝑖)
13		vc	. . . . . . . . . . 11 setvar 𝑐
14	13	cv 1569	. . . . . . . . . 10 class 𝑐
15		chash 14441	. . . . . . . . . 10 class ♯
16	14, 15	cfv 6527	. . . . . . . . 9 class (♯‘𝑐)
17	5	cv 1569	. . . . . . . . 9 class 𝑘
18	16, 17	wceq 1570	. . . . . . . 8 wff (♯‘𝑐) = 𝑘
19	10	cpw 4556	. . . . . . . 8 class 𝒫 𝑖
20	18, 13, 19	crab 3412	. . . . . . 7 class {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘}
21	12, 20	cima 5650	. . . . . 6 class ((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})
22		vh	. . . . . . . . . 10 setvar ℎ
23	22	cv 1569	. . . . . . . . 9 class ℎ
24		cc0 11171	. . . . . . . . 9 class 0
25		cfsupp 9331	. . . . . . . . 9 class finSupp
26	23, 24, 25	wbr 5102	. . . . . . . 8 wff ℎ finSupp 0
27		cmap 8825	. . . . . . . . 9 class ↑m
28	6, 10, 27	co 7408	. . . . . . . 8 class (ℕ0 ↑m 𝑖)
29	26, 22, 28	crab 3412	. . . . . . 7 class {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0}
30	29, 11	cfv 6527	. . . . . 6 class (𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})
31	21, 30	cfv 6527	. . . . 5 class ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘}))
32	9, 31	ccom 5651	. . . 4 class ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))
33	5, 6, 32	cmpt 5185	. . 3 class (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘}))))
34	2, 3, 4, 4, 33	cmpo 7410	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))))
35	1, 34	wceq 1570	1 wff eSymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))))

This definition is used by:  esplyval  34127