This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) ) )