Metamath Proof Explorer

Definition df-esply

Description: Define elementary symmetric polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Assertion df-esply 
|- eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cesply 
 |-  eSymPoly
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vr 
 |-  r
4 vk 
 |-  k
5 cn0 
 |-  NN0
6 czrh 
 |-  ZRHom
7 3 cv 
 |-  r
8 7 6 cfv 
 |-  ( ZRHom ` r )
9 cind 
 |-  _Ind
10 vh 
 |-  h
11 cmap 
 |-  ^m
12 1 cv 
 |-  i
13 5 12 11 co 
 |-  ( NN0 ^m i )
14 10 cv 
 |-  h
15 cfsupp 
 |-  finSupp
16 cc0 
 |-  0
17 14 16 15 wbr 
 |-  h finSupp 0
18 17 10 13 crab 
 |-  { h e. ( NN0 ^m i ) | h finSupp 0 }
19 18 9 cfv 
 |-  ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } )
20 12 9 cfv 
 |-  ( _Ind ` i )
21 vc 
 |-  c
22 12 cpw 
 |-  ~P i
23 chash 
 |-  #
24 21 cv 
 |-  c
25 24 23 cfv 
 |-  ( # ` c )
26 4 cv 
 |-  k
27 25 26 wceq 
 |-  ( # ` c ) = k
28 27 21 22 crab 
 |-  { c e. ~P i | ( # ` c ) = k }
29 20 28 cima 
 |-  ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } )
30 29 19 cfv 
 |-  ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) )
31 8 30 ccom 
 |-  ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) )
32 4 5 31 cmpt 
 |-  ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) )
33 1 3 2 2 32 cmpo 
 |-  ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) )
34 0 33 wceq 
 |-  eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) )