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 Could not format assertion : No typesetting found for |- SymPoly = ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 csply Could not format SymPoly : No typesetting found for class SymPoly with typecode class
1 vi setvar i
2 cvv class V
3 vr setvar r
4 cbs class Base
5 1 cv setvar i
6 cmpl class mPoly
7 3 cv setvar r
8 5 7 6 co class i mPoly r
9 8 4 cfv class Base i mPoly r
10 cfxp Could not format FixPts : No typesetting found for class FixPts with typecode class
11 vd setvar d
12 csymg class SymGrp
13 5 12 cfv class SymGrp ⁡ i
14 13 4 cfv class Base SymGrp ⁡ i
15 vf setvar f
16 vx setvar x
17 vh setvar h
18 cn0 class ℕ 0
19 cmap class ↑ 𝑚
20 18 5 19 co class ℕ 0 i
21 17 cv setvar h
22 cfsupp class finSupp
23 cc0 class 0
24 21 23 22 wbr wff finSupp 0 ⁡ h
25 24 17 20 crab class h ∈ ℕ 0 i | finSupp 0 ⁡ h
26 15 cv setvar f
27 16 cv setvar x
28 11 cv setvar d
29 27 28 ccom class x ∘ d
30 29 26 cfv class f ⁡ x ∘ d
31 16 25 30 cmpt class x ∈ h ∈ ℕ 0 i | finSupp 0 ⁡ h ⟼ f ⁡ x ∘ d
32 11 15 14 9 31 cmpo class d ∈ Base SymGrp ⁡ i , f ∈ Base i mPoly r ⟼ x ∈ h ∈ ℕ 0 i | finSupp 0 ⁡ h ⟼ f ⁡ x ∘ d
33 9 32 10 co Could not format ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) : No typesetting found for class ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) with typecode class
34 1 3 2 2 33 cmpo Could not format ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) : No typesetting found for class ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) with typecode class
35 0 34 wceq Could not format SymPoly = ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) : No typesetting found for wff SymPoly = ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) with typecode wff