Metamath Proof Explorer

Theorem esplyfval2

Description: When K is out-of-bounds, the K -th elementary symmetric polynomial is zero. (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses esplyfval2.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
esplyfval2.i 
|- ( ph -> I e. Fin )
esplyfval2.r 
|- ( ph -> R e. Ring )
esplyfval2.k 
|- ( ph -> K e. ( NN0 \ ( 0 ... ( # ` I ) ) ) )
esplyfval2.z 
|- Z = ( 0g ` ( I mPoly R ) )
Assertion esplyfval2 
|- ( ph -> ( ( I eSymPoly R ) ` K ) = Z )

Proof

Step Hyp Ref Expression
1 esplyfval2.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2 esplyfval2.i 
 |-  ( ph -> I e. Fin )
3 esplyfval2.r 
 |-  ( ph -> R e. Ring )
4 esplyfval2.k 
 |-  ( ph -> K e. ( NN0 \ ( 0 ... ( # ` I ) ) ) )
5 esplyfval2.z 
 |-  Z = ( 0g ` ( I mPoly R ) )
6 2 adantr 
 |-  ( ( ph /\ c e. ~P I ) -> I e. Fin )
7 elpwi 
 |-  ( c e. ~P I -> c C_ I )
8 7 adantl 
 |-  ( ( ph /\ c e. ~P I ) -> c C_ I )
9 6 8 ssfid 
 |-  ( ( ph /\ c e. ~P I ) -> c e. Fin )
10 hashcl 
 |-  ( c e. Fin -> ( # ` c ) e. NN0 )
11 9 10 syl 
 |-  ( ( ph /\ c e. ~P I ) -> ( # ` c ) e. NN0 )
12 11 nn0red 
 |-  ( ( ph /\ c e. ~P I ) -> ( # ` c ) e. RR )
13 hashcl 
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
14 2 13 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
15 14 nn0red 
 |-  ( ph -> ( # ` I ) e. RR )
16 15 adantr 
 |-  ( ( ph /\ c e. ~P I ) -> ( # ` I ) e. RR )
17 4 eldifad 
 |-  ( ph -> K e. NN0 )
18 17 nn0red 
 |-  ( ph -> K e. RR )
19 18 adantr 
 |-  ( ( ph /\ c e. ~P I ) -> K e. RR )
20 hashss 
 |-  ( ( I e. Fin /\ c C_ I ) -> ( # ` c ) <_ ( # ` I ) )
21 6 8 20 syl2anc 
 |-  ( ( ph /\ c e. ~P I ) -> ( # ` c ) <_ ( # ` I ) )
22 14 nn0zd 
 |-  ( ph -> ( # ` I ) e. ZZ )
23 nn0diffz0 
 |-  ( ( # ` I ) e. NN0 -> ( NN0 \ ( 0 ... ( # ` I ) ) ) = ( ZZ>= ` ( ( # ` I ) + 1 ) ) )
24 14 23 syl 
 |-  ( ph -> ( NN0 \ ( 0 ... ( # ` I ) ) ) = ( ZZ>= ` ( ( # ` I ) + 1 ) ) )
25 4 24 eleqtrd 
 |-  ( ph -> K e. ( ZZ>= ` ( ( # ` I ) + 1 ) ) )
26 eluzp1l 
 |-  ( ( ( # ` I ) e. ZZ /\ K e. ( ZZ>= ` ( ( # ` I ) + 1 ) ) ) -> ( # ` I ) < K )
27 22 25 26 syl2anc 
 |-  ( ph -> ( # ` I ) < K )
28 27 adantr 
 |-  ( ( ph /\ c e. ~P I ) -> ( # ` I ) < K )
29 12 16 19 21 28 lelttrd 
 |-  ( ( ph /\ c e. ~P I ) -> ( # ` c ) < K )
30 12 29 ltned 
 |-  ( ( ph /\ c e. ~P I ) -> ( # ` c ) =/= K )
31 30 neneqd 
 |-  ( ( ph /\ c e. ~P I ) -> -. ( # ` c ) = K )
32 31 ralrimiva 
 |-  ( ph -> A. c e. ~P I -. ( # ` c ) = K )
33 rabeq0 
 |-  ( { c e. ~P I | ( # ` c ) = K } = (/) <-> A. c e. ~P I -. ( # ` c ) = K )
34 32 33 sylibr 
 |-  ( ph -> { c e. ~P I | ( # ` c ) = K } = (/) )
35 34 imaeq2d 
 |-  ( ph -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) = ( ( _Ind ` I ) " (/) ) )
36 ima0 
 |-  ( ( _Ind ` I ) " (/) ) = (/)
37 35 36 eqtrdi 
 |-  ( ph -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) = (/) )
38 37 fveq2d 
 |-  ( ph -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) = ( ( _Ind ` D ) ` (/) ) )
39 ovex 
 |-  ( NN0 ^m I ) e. _V
40 1 39 rabex2 
 |-  D e. _V
41 indconst0 
 |-  ( D e. _V -> ( ( _Ind ` D ) ` (/) ) = ( D X. { 0 } ) )
42 40 41 mp1i 
 |-  ( ph -> ( ( _Ind ` D ) ` (/) ) = ( D X. { 0 } ) )
43 38 42 eqtrd 
 |-  ( ph -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) = ( D X. { 0 } ) )
44 43 coeq2d 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) = ( ( ZRHom ` R ) o. ( D X. { 0 } ) ) )
45 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
46 45 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
47 zringbas 
 |-  ZZ = ( Base ` ZZring )
48 eqid 
 |-  ( Base ` R ) = ( Base ` R )
49 47 48 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
50 3 46 49 3syl 
 |-  ( ph -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
51 50 ffnd 
 |-  ( ph -> ( ZRHom ` R ) Fn ZZ )
52 0zd 
 |-  ( ph -> 0 e. ZZ )
53 fcoconst 
 |-  ( ( ( ZRHom ` R ) Fn ZZ /\ 0 e. ZZ ) -> ( ( ZRHom ` R ) o. ( D X. { 0 } ) ) = ( D X. { ( ( ZRHom ` R ) ` 0 ) } ) )
54 51 52 53 syl2anc 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( D X. { 0 } ) ) = ( D X. { ( ( ZRHom ` R ) ` 0 ) } ) )
55 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
56 45 55 zrh0 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
57 3 56 syl 
 |-  ( ph -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
58 57 sneqd 
 |-  ( ph -> { ( ( ZRHom ` R ) ` 0 ) } = { ( 0g ` R ) } )
59 58 xpeq2d 
 |-  ( ph -> ( D X. { ( ( ZRHom ` R ) ` 0 ) } ) = ( D X. { ( 0g ` R ) } ) )
60 44 54 59 3eqtrd 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) = ( D X. { ( 0g ` R ) } ) )
61 1 2 3 17 esplyfval 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) )
62 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
63 1 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
64 3 ringgrpd 
 |-  ( ph -> R e. Grp )
65 62 63 55 5 2 64 mpl0 
 |-  ( ph -> Z = ( D X. { ( 0g ` R ) } ) )
66 60 61 65 3eqtr4d 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) = Z )