Metamath Proof Explorer

Theorem esplyfv

Description: Coefficient for the K -th elementary symmetric polynomial and a bag of variables F : the coefficient is .1. for the bags of exactly K variables, having exponent at most 1 . (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses esplyfv.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
esplyfv.i 
|- ( ph -> I e. Fin )
esplyfv.r 
|- ( ph -> R e. Ring )
esplyfv.k 
|- ( ph -> K e. ( 0 ... ( # ` I ) ) )
esplyfv.f 
|- ( ph -> F e. D )
esplyfv.0 
|- .0. = ( 0g ` R )
esplyfv.1 
|- .1. = ( 1r ` R )
Assertion esplyfv 
|- ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( ran F C_ { 0 , 1 } /\ ( # ` ( F supp 0 ) ) = K ) , .1. , .0. ) )

Proof

Step Hyp Ref Expression
1 esplyfv.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2 esplyfv.i 
 |-  ( ph -> I e. Fin )
3 esplyfv.r 
 |-  ( ph -> R e. Ring )
4 esplyfv.k 
 |-  ( ph -> K e. ( 0 ... ( # ` I ) ) )
5 esplyfv.f 
 |-  ( ph -> F e. D )
6 esplyfv.0 
 |-  .0. = ( 0g ` R )
7 esplyfv.1 
 |-  .1. = ( 1r ` R )
8 eqeq2 
 |-  ( if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) -> ( ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) <-> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) ) )
9 eqeq2 
 |-  ( .0. = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) -> ( ( ( ( I eSymPoly R ) ` K ) ` F ) = .0. <-> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) ) )
10 2 adantr 
 |-  ( ( ph /\ ran F C_ { 0 , 1 } ) -> I e. Fin )
11 3 adantr 
 |-  ( ( ph /\ ran F C_ { 0 , 1 } ) -> R e. Ring )
12 4 adantr 
 |-  ( ( ph /\ ran F C_ { 0 , 1 } ) -> K e. ( 0 ... ( # ` I ) ) )
13 5 adantr 
 |-  ( ( ph /\ ran F C_ { 0 , 1 } ) -> F e. D )
14 simpr 
 |-  ( ( ph /\ ran F C_ { 0 , 1 } ) -> ran F C_ { 0 , 1 } )
15 1 10 11 12 13 6 7 14 esplyfv1 
 |-  ( ( ph /\ ran F C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) )
16 2 adantr 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> I e. Fin )
17 3 adantr 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> R e. Ring )
18 elfznn0 
 |-  ( K e. ( 0 ... ( # ` I ) ) -> K e. NN0 )
19 4 18 syl 
 |-  ( ph -> K e. NN0 )
20 19 adantr 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> K e. NN0 )
21 1 16 17 20 esplyfval 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) )
22 21 fveq1d 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` F ) = ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` F ) )
23 ovex 
 |-  ( NN0 ^m I ) e. _V
24 1 23 rabex2 
 |-  D e. _V
25 24 a1i 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> D e. _V )
26 1 16 17 20 esplylem 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D )
27 indf 
 |-  ( ( D e. _V /\ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } )
28 25 26 27 syl2anc 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } )
29 5 adantr 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> F e. D )
30 28 29 fvco3d 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` F ) = ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` F ) ) )
31 simpr 
 |-  ( ( ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ( ( _Ind ` I ) ` d ) = F )
32 2 ad4antr 
 |-  ( ( ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> I e. Fin )
33 ssrab2 
 |-  { c e. ~P I | ( # ` c ) = K } C_ ~P I
34 33 a1i 
 |-  ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> { c e. ~P I | ( # ` c ) = K } C_ ~P I )
35 34 sselda 
 |-  ( ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> d e. ~P I )
36 35 adantr 
 |-  ( ( ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> d e. ~P I )
37 36 elpwid 
 |-  ( ( ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> d C_ I )
38 indf 
 |-  ( ( I e. Fin /\ d C_ I ) -> ( ( _Ind ` I ) ` d ) : I --> { 0 , 1 } )
39 32 37 38 syl2anc 
 |-  ( ( ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ( ( _Ind ` I ) ` d ) : I --> { 0 , 1 } )
40 31 39 feq1dd 
 |-  ( ( ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> F : I --> { 0 , 1 } )
41 40 frnd 
 |-  ( ( ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ran F C_ { 0 , 1 } )
42 indf1o 
 |-  ( I e. Fin -> ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) )
43 f1of 
 |-  ( ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
44 16 42 43 3syl 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
45 44 ffnd 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( _Ind ` I ) Fn ~P I )
46 33 a1i 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> { c e. ~P I | ( # ` c ) = K } C_ ~P I )
47 45 46 fvelimabd 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) <-> E. d e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` d ) = F ) )
48 47 biimpa 
 |-  ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> E. d e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` d ) = F )
49 41 48 r19.29a 
 |-  ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> ran F C_ { 0 , 1 } )
50 simplr 
 |-  ( ( ( ph /\ -. ran F C_ { 0 , 1 } ) /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> -. ran F C_ { 0 , 1 } )
51 49 50 pm2.65da 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> -. F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) )
52 29 51 eldifd 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> F e. ( D \ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) )
53 ind0 
 |-  ( ( D e. _V /\ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D /\ F e. ( D \ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` F ) = 0 )
54 24 26 52 53 mp3an2i 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` F ) = 0 )
55 54 fveq2d 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` F ) ) = ( ( ZRHom ` R ) ` 0 ) )
56 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
57 56 6 zrh0 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 0 ) = .0. )
58 3 57 syl 
 |-  ( ph -> ( ( ZRHom ` R ) ` 0 ) = .0. )
59 58 adantr 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ZRHom ` R ) ` 0 ) = .0. )
60 55 59 eqtrd 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` F ) ) = .0. )
61 22 30 60 3eqtrd 
 |-  ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` F ) = .0. )
62 8 9 15 61 ifbothda 
 |-  ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) )
63 ifan 
 |-  if ( ( ran F C_ { 0 , 1 } /\ ( # ` ( F supp 0 ) ) = K ) , .1. , .0. ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. )
64 62 63 eqtr4di 
 |-  ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( ran F C_ { 0 , 1 } /\ ( # ` ( F supp 0 ) ) = K ) , .1. , .0. ) )