This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem esplyfv1

Description: Coefficient for the K -th elementary symmetric polynomial and a bag of variables F where variables are not raised to a power. (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 )
esplyfv1.1 
|- ( ph -> ran F C_ { 0 , 1 } )
Assertion esplyfv1 
|- ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( 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 esplyfv1.1 
 |-  ( ph -> ran F C_ { 0 , 1 } )
9 elfznn0 
 |-  ( K e. ( 0 ... ( # ` I ) ) -> K e. NN0 )
10 4 9 syl 
 |-  ( ph -> K e. NN0 )
11 1 2 3 10 esplyfval 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) )
12 11 fveq1d 
 |-  ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` F ) )
13 ovex 
 |-  ( NN0 ^m I ) e. _V
14 1 ssrab3 
 |-  D C_ ( NN0 ^m I )
15 13 14 ssexi 
 |-  D e. _V
16 15 a1i 
 |-  ( ph -> D e. _V )
17 nfv 
 |-  F/ d ph
18 indf1o 
 |-  ( I e. Fin -> ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) )
19 f1of 
 |-  ( ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
20 2 18 19 3syl 
 |-  ( ph -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
21 20 ffund 
 |-  ( ph -> Fun ( _Ind ` I ) )
22 breq1 
 |-  ( h = ( ( _Ind ` I ) ` d ) -> ( h finSupp 0 <-> ( ( _Ind ` I ) ` d ) finSupp 0 ) )
23 nn0ex 
 |-  NN0 e. _V
24 23 a1i 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> NN0 e. _V )
25 2 adantr 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> I e. Fin )
26 ssrab2 
 |-  { c e. ~P I | ( # ` c ) = K } C_ ~P I
27 26 a1i 
 |-  ( ph -> { c e. ~P I | ( # ` c ) = K } C_ ~P I )
28 27 sselda 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> d e. ~P I )
29 28 elpwid 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> d C_ I )
30 indf 
 |-  ( ( I e. Fin /\ d C_ I ) -> ( ( _Ind ` I ) ` d ) : I --> { 0 , 1 } )
31 25 29 30 syl2anc 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) : I --> { 0 , 1 } )
32 0nn0 
 |-  0 e. NN0
33 32 a1i 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> 0 e. NN0 )
34 1nn0 
 |-  1 e. NN0
35 34 a1i 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> 1 e. NN0 )
36 33 35 prssd 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> { 0 , 1 } C_ NN0 )
37 31 36 fssd 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) : I --> NN0 )
38 24 25 37 elmapdd 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) e. ( NN0 ^m I ) )
39 31 25 33 fidmfisupp 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) finSupp 0 )
40 22 38 39 elrabd 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
41 40 1 eleqtrrdi 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( _Ind ` I ) ` d ) e. D )
42 17 21 41 funimassd 
 |-  ( ph -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D )
43 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 } )
44 16 42 43 syl2anc 
 |-  ( ph -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } )
45 44 5 fvco3d 
 |-  ( ph -> ( ( ( 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 ) ) )
46 indfval 
 |-  ( ( D e. _V /\ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D /\ F e. D ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` F ) = if ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) , 1 , 0 ) )
47 15 42 5 46 mp3an2i 
 |-  ( ph -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` F ) = if ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) , 1 , 0 ) )
48 47 fveq2d 
 |-  ( ph -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` F ) ) = ( ( ZRHom ` R ) ` if ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) , 1 , 0 ) ) )
49 fvif 
 |-  ( ( ZRHom ` R ) ` if ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) , 1 , 0 ) ) = if ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) , ( ( ZRHom ` R ) ` 1 ) , ( ( ZRHom ` R ) ` 0 ) )
50 49 a1i 
 |-  ( ph -> ( ( ZRHom ` R ) ` if ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) , 1 , 0 ) ) = if ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) , ( ( ZRHom ` R ) ` 1 ) , ( ( ZRHom ` R ) ` 0 ) ) )
51 simpr 
 |-  ( ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ( ( _Ind ` I ) ` d ) = F )
52 51 oveq1d 
 |-  ( ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ( ( ( _Ind ` I ) ` d ) supp 0 ) = ( F supp 0 ) )
53 indsupp 
 |-  ( ( I e. Fin /\ d C_ I ) -> ( ( ( _Ind ` I ) ` d ) supp 0 ) = d )
54 25 29 53 syl2anc 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( ( ( _Ind ` I ) ` d ) supp 0 ) = d )
55 54 adantr 
 |-  ( ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ( ( ( _Ind ` I ) ` d ) supp 0 ) = d )
56 52 55 eqtr3d 
 |-  ( ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ( F supp 0 ) = d )
57 56 fveq2d 
 |-  ( ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ( # ` ( F supp 0 ) ) = ( # ` d ) )
58 fveqeq2 
 |-  ( c = d -> ( ( # ` c ) = K <-> ( # ` d ) = K ) )
59 simpr 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> d e. { c e. ~P I | ( # ` c ) = K } )
60 58 59 elrabrd 
 |-  ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> ( # ` d ) = K )
61 60 adantr 
 |-  ( ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ( # ` d ) = K )
62 57 61 eqtrd 
 |-  ( ( ( ph /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ( # ` ( F supp 0 ) ) = K )
63 62 adantllr 
 |-  ( ( ( ( ph /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = F ) -> ( # ` ( F supp 0 ) ) = K )
64 20 ffnd 
 |-  ( ph -> ( _Ind ` I ) Fn ~P I )
65 64 27 fvelimabd 
 |-  ( ph -> ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) <-> E. d e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` d ) = F ) )
66 65 biimpa 
 |-  ( ( ph /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> E. d e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` d ) = F )
67 63 66 r19.29a 
 |-  ( ( ph /\ F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> ( # ` ( F supp 0 ) ) = K )
68 fveqeq2 
 |-  ( d = ( F supp 0 ) -> ( ( ( _Ind ` I ) ` d ) = F <-> ( ( _Ind ` I ) ` ( F supp 0 ) ) = F ) )
69 fveqeq2 
 |-  ( c = ( F supp 0 ) -> ( ( # ` c ) = K <-> ( # ` ( F supp 0 ) ) = K ) )
70 2 adantr 
 |-  ( ( ph /\ ( # ` ( F supp 0 ) ) = K ) -> I e. Fin )
71 suppssdm 
 |-  ( F supp 0 ) C_ dom F
72 23 a1i 
 |-  ( ph -> NN0 e. _V )
73 14 5 sselid 
 |-  ( ph -> F e. ( NN0 ^m I ) )
74 2 72 73 elmaprd 
 |-  ( ph -> F : I --> NN0 )
75 71 74 fssdm 
 |-  ( ph -> ( F supp 0 ) C_ I )
76 75 adantr 
 |-  ( ( ph /\ ( # ` ( F supp 0 ) ) = K ) -> ( F supp 0 ) C_ I )
77 70 76 sselpwd 
 |-  ( ( ph /\ ( # ` ( F supp 0 ) ) = K ) -> ( F supp 0 ) e. ~P I )
78 simpr 
 |-  ( ( ph /\ ( # ` ( F supp 0 ) ) = K ) -> ( # ` ( F supp 0 ) ) = K )
79 69 77 78 elrabd 
 |-  ( ( ph /\ ( # ` ( F supp 0 ) ) = K ) -> ( F supp 0 ) e. { c e. ~P I | ( # ` c ) = K } )
80 74 ffnd 
 |-  ( ph -> F Fn I )
81 df-f 
 |-  ( F : I --> { 0 , 1 } <-> ( F Fn I /\ ran F C_ { 0 , 1 } ) )
82 80 8 81 sylanbrc 
 |-  ( ph -> F : I --> { 0 , 1 } )
83 2 82 indfsid 
 |-  ( ph -> F = ( ( _Ind ` I ) ` ( F supp 0 ) ) )
84 83 adantr 
 |-  ( ( ph /\ ( # ` ( F supp 0 ) ) = K ) -> F = ( ( _Ind ` I ) ` ( F supp 0 ) ) )
85 84 eqcomd 
 |-  ( ( ph /\ ( # ` ( F supp 0 ) ) = K ) -> ( ( _Ind ` I ) ` ( F supp 0 ) ) = F )
86 68 79 85 rspcedvdw 
 |-  ( ( ph /\ ( # ` ( F supp 0 ) ) = K ) -> E. d e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` d ) = F )
87 65 biimpar 
 |-  ( ( ph /\ E. d e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` d ) = F ) -> F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) )
88 86 87 syldan 
 |-  ( ( ph /\ ( # ` ( F supp 0 ) ) = K ) -> F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) )
89 67 88 impbida 
 |-  ( ph -> ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) <-> ( # ` ( F supp 0 ) ) = K ) )
90 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
91 90 7 zrh1 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 1 ) = .1. )
92 3 91 syl 
 |-  ( ph -> ( ( ZRHom ` R ) ` 1 ) = .1. )
93 90 6 zrh0 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 0 ) = .0. )
94 3 93 syl 
 |-  ( ph -> ( ( ZRHom ` R ) ` 0 ) = .0. )
95 89 92 94 ifbieq12d 
 |-  ( ph -> if ( F e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) , ( ( ZRHom ` R ) ` 1 ) , ( ( ZRHom ` R ) ` 0 ) ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) )
96 48 50 95 3eqtrd 
 |-  ( ph -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` F ) ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) )
97 12 45 96 3eqtrd 
 |-  ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) )