Definition df-sply

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csply	⊢ SymPoly
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		vr	⊢ 𝑟
4		cbs	⊢ Base
5	1	cv	⊢ 𝑖
6		cmpl	⊢ mPoly
7	3	cv	⊢ 𝑟
8	5 7 6	co	⊢ ( 𝑖 mPoly 𝑟 )
9	8 4	cfv	⊢ ( Base ‘ ( 𝑖 mPoly 𝑟 ) )
10		cfxp	⊢ FixPts
11		vd	⊢ 𝑑
12		csymg	⊢ SymGrp
13	5 12	cfv	⊢ ( SymGrp ‘ 𝑖 )
14	13 4	cfv	⊢ ( Base ‘ ( SymGrp ‘ 𝑖 ) )
15		vf	⊢ 𝑓
16		vx	⊢ 𝑥
17		vh	⊢ ℎ
18		cn0	⊢ ℕ0
19		cmap	⊢ ↑m
20	18 5 19	co	⊢ ( ℕ0 ↑m 𝑖 )
21	17	cv	⊢ ℎ
22		cfsupp	⊢ finSupp
23		cc0	⊢ 0
24	21 23 22	wbr	⊢ ℎ finSupp 0
25	24 17 20	crab	⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 }
26	15	cv	⊢ 𝑓
27	16	cv	⊢ 𝑥
28	11	cv	⊢ 𝑑
29	27 28	ccom	⊢ ( 𝑥 ∘ 𝑑 )
30	29 26	cfv	⊢ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) )
31	16 25 30	cmpt	⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) )
32	11 15 14 9 31	cmpo	⊢ ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑖 ) ) , 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
33	9 32 10	co	⊢ ( ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) FixPts ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑖 ) ) , 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) )
34	1 3 2 2 33	cmpo	⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) FixPts ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑖 ) ) , 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) ) )
35	0 34	wceq	⊢ SymPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) FixPts ( 𝑑 ∈ ( Base ‘ ( SymGrp ‘ 𝑖 ) ) , 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) ) )