Definition df-esply 33549

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 33547	. 2 class eSymPoly
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3433	. . 3 class V
5		vk	. . . 4 setvar 𝑘
6		cn0 12372	. . . 4 class ℕ0
7	3	cv 1539	. . . . . 6 class 𝑟
8		czrh 21390	. . . . . 6 class ℤRHom
9	7, 8	cfv 6476	. . . . 5 class (ℤRHom‘𝑟)
10	2	cv 1539	. . . . . . . 8 class 𝑖
11		cind 32786	. . . . . . . 8 class 𝟭
12	10, 11	cfv 6476	. . . . . . 7 class (𝟭‘𝑖)
13		vc	. . . . . . . . . . 11 setvar 𝑐
14	13	cv 1539	. . . . . . . . . 10 class 𝑐
15		chash 14225	. . . . . . . . . 10 class ♯
16	14, 15	cfv 6476	. . . . . . . . 9 class (♯‘𝑐)
17	5	cv 1539	. . . . . . . . 9 class 𝑘
18	16, 17	wceq 1540	. . . . . . . 8 wff (♯‘𝑐) = 𝑘
19	10	cpw 4547	. . . . . . . 8 class 𝒫 𝑖
20	18, 13, 19	crab 3392	. . . . . . 7 class {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘}
21	12, 20	cima 5616	. . . . . 6 class ((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})
22		vh	. . . . . . . . . 10 setvar ℎ
23	22	cv 1539	. . . . . . . . 9 class ℎ
24		cc0 10997	. . . . . . . . 9 class 0
25		cfsupp 9239	. . . . . . . . 9 class finSupp
26	23, 24, 25	wbr 5088	. . . . . . . 8 wff ℎ finSupp 0
27		cmap 8744	. . . . . . . . 9 class ↑m
28	6, 10, 27	co 7340	. . . . . . . 8 class (ℕ0 ↑m 𝑖)
29	26, 22, 28	crab 3392	. . . . . . 7 class {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0}
30	29, 11	cfv 6476	. . . . . 6 class (𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})
31	21, 30	cfv 6476	. . . . 5 class ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘}))
32	9, 31	ccom 5617	. . . 4 class ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))
33	5, 6, 32	cmpt 5169	. . 3 class (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘}))))
34	2, 3, 4, 4, 33	cmpo 7342	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))))
35	1, 34	wceq 1540	1 wff eSymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))))

This definition is referenced by:  esplyval  33553