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 = ( 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 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csply 
 |-  SymPoly
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vr 
 |-  r
4 cbs 
 |-  Base
5 1 cv 
 |-  i
6 cmpl 
 |-  mPoly
7 3 cv 
 |-  r
8 5 7 6 co 
 |-  ( i mPoly r )
9 8 4 cfv 
 |-  ( Base ` ( i mPoly r ) )
10 cfxp 
 |-  FixPts
11 vd 
 |-  d
12 csymg 
 |-  SymGrp
13 5 12 cfv 
 |-  ( SymGrp ` i )
14 13 4 cfv 
 |-  ( Base ` ( SymGrp ` i ) )
15 vf 
 |-  f
16 vx 
 |-  x
17 vh 
 |-  h
18 cn0 
 |-  NN0
19 cmap 
 |-  ^m
20 18 5 19 co 
 |-  ( NN0 ^m i )
21 17 cv 
 |-  h
22 cfsupp 
 |-  finSupp
23 cc0 
 |-  0
24 21 23 22 wbr 
 |-  h finSupp 0
25 24 17 20 crab 
 |-  { h e. ( NN0 ^m i ) | h finSupp 0 }
26 15 cv 
 |-  f
27 16 cv 
 |-  x
28 11 cv 
 |-  d
29 27 28 ccom 
 |-  ( x o. d )
30 29 26 cfv 
 |-  ( f ` ( x o. d ) )
31 16 25 30 cmpt 
 |-  ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) )
32 11 15 14 9 31 cmpo 
 |-  ( 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 ) ) ) )
33 9 32 10 co 
 |-  ( ( 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 ) ) ) ) )
34 1 3 2 2 33 cmpo 
 |-  ( 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 ) ) ) ) ) )
35 0 34 wceq 
 |-  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 ) ) ) ) ) )