Definition df-sply 33551

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

Assertion

Ref	Expression
df-sply	⊢ SymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ((Base‘(𝑖 mPoly 𝑟))FixPts(𝑑 ∈ (Base‘(SymGrp‘𝑖)), 𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))))

Distinct variable group:   𝑖,𝑟,𝑑,𝑓,𝑥,ℎ

Detailed syntax breakdown of Definition df-sply

Step	Hyp	Ref	Expression
1		csply 33550	. 2 class SymPoly
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3436	. . 3 class V
5	2	cv 1539	. . . . . 6 class 𝑖
6	3	cv 1539	. . . . . 6 class 𝑟
7		cmpl 21813	. . . . . 6 class mPoly
8	5, 6, 7	co 7349	. . . . 5 class (𝑖 mPoly 𝑟)
9		cbs 17120	. . . . 5 class Base
10	8, 9	cfv 6482	. . . 4 class (Base‘(𝑖 mPoly 𝑟))
11		vd	. . . . 5 setvar 𝑑
12		vf	. . . . 5 setvar 𝑓
13		csymg 19248	. . . . . . 7 class SymGrp
14	5, 13	cfv 6482	. . . . . 6 class (SymGrp‘𝑖)
15	14, 9	cfv 6482	. . . . 5 class (Base‘(SymGrp‘𝑖))
16		vx	. . . . . 6 setvar 𝑥
17		vh	. . . . . . . . 9 setvar ℎ
18	17	cv 1539	. . . . . . . 8 class ℎ
19		cc0 11009	. . . . . . . 8 class 0
20		cfsupp 9251	. . . . . . . 8 class finSupp
21	18, 19, 20	wbr 5092	. . . . . . 7 wff ℎ finSupp 0
22		cn0 12384	. . . . . . . 8 class ℕ0
23		cmap 8753	. . . . . . . 8 class ↑m
24	22, 5, 23	co 7349	. . . . . . 7 class (ℕ0 ↑m 𝑖)
25	21, 17, 24	crab 3394	. . . . . 6 class {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0}
26	16	cv 1539	. . . . . . . 8 class 𝑥
27	11	cv 1539	. . . . . . . 8 class 𝑑
28	26, 27	ccom 5623	. . . . . . 7 class (𝑥 ∘ 𝑑)
29	12	cv 1539	. . . . . . 7 class 𝑓
30	28, 29	cfv 6482	. . . . . 6 class (𝑓‘(𝑥 ∘ 𝑑))
31	16, 25, 30	cmpt 5173	. . . . 5 class (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))
32	11, 12, 15, 10, 31	cmpo 7351	. . . 4 class (𝑑 ∈ (Base‘(SymGrp‘𝑖)), 𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))
33		cfxp 33106	. . . 4 class FixPts
34	10, 32, 33	co 7349	. . 3 class ((Base‘(𝑖 mPoly 𝑟))FixPts(𝑑 ∈ (Base‘(SymGrp‘𝑖)), 𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
35	2, 3, 4, 4, 34	cmpo 7351	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ ((Base‘(𝑖 mPoly 𝑟))FixPts(𝑑 ∈ (Base‘(SymGrp‘𝑖)), 𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))))
36	1, 35	wceq 1540	1 wff SymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ((Base‘(𝑖 mPoly 𝑟))FixPts(𝑑 ∈ (Base‘(SymGrp‘𝑖)), 𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))))

This definition is referenced by:  splyval  33552