Metamath Proof Explorer

Theorem esplyindfv

Description: A recursive formula for the elementary symmetric polynomials, evaluated at a given set of points Z . (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses esplyindfv.m 
|- .x. = ( .r ` R )
esplyindfv.i 
|- ( ph -> I e. Fin )
esplyindfv.r 
|- ( ph -> R e. CRing )
esplyindfv.y 
|- ( ph -> Y e. I )
esplyindfv.j 
|- J = ( I \ { Y } )
esplyindfv.e 
|- E = ( J eSymPoly R )
esplyindfv.k 
|- ( ph -> K e. ( 0 ... ( # ` J ) ) )
esplyindfv.c 
|- C = { h e. ( NN0 ^m J ) | h finSupp 0 }
esplyindfv.f 
|- F = ( ( I eSymPoly R ) ` ( K + 1 ) )
esplyindfv.b 
|- B = ( Base ` R )
esplyindfv.q 
|- Q = ( I eval R )
esplyindfv.o 
|- O = ( J eval R )
esplyindfv.p 
|- .+ = ( +g ` R )
esplyindfv.z 
|- ( ph -> Z : I --> B )
Assertion esplyindfv 
|- ( ph -> ( ( Q ` F ) ` Z ) = ( ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) )

Proof

Step Hyp Ref Expression
1 esplyindfv.m 
 |-  .x. = ( .r ` R )
2 esplyindfv.i 
 |-  ( ph -> I e. Fin )
3 esplyindfv.r 
 |-  ( ph -> R e. CRing )
4 esplyindfv.y 
 |-  ( ph -> Y e. I )
5 esplyindfv.j 
 |-  J = ( I \ { Y } )
6 esplyindfv.e 
 |-  E = ( J eSymPoly R )
7 esplyindfv.k 
 |-  ( ph -> K e. ( 0 ... ( # ` J ) ) )
8 esplyindfv.c 
 |-  C = { h e. ( NN0 ^m J ) | h finSupp 0 }
9 esplyindfv.f 
 |-  F = ( ( I eSymPoly R ) ` ( K + 1 ) )
10 esplyindfv.b 
 |-  B = ( Base ` R )
11 esplyindfv.q 
 |-  Q = ( I eval R )
12 esplyindfv.o 
 |-  O = ( J eval R )
13 esplyindfv.p 
 |-  .+ = ( +g ` R )
14 esplyindfv.z 
 |-  ( ph -> Z : I --> B )
15 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
16 eqid 
 |-  ( I mVar R ) = ( I mVar R )
17 eqid 
 |-  ( +g ` ( I mPoly R ) ) = ( +g ` ( I mPoly R ) )
18 eqid 
 |-  ( .r ` ( I mPoly R ) ) = ( .r ` ( I mPoly R ) )
19 eqid 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 }
20 eqid 
 |-  ( ( I extendVars R ) ` Y ) = ( ( I extendVars R ) ` Y )
21 3 crngringd 
 |-  ( ph -> R e. Ring )
22 7 elfzelzd 
 |-  ( ph -> K e. ZZ )
23 hashcl 
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
24 2 23 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
25 24 nn0zd 
 |-  ( ph -> ( # ` I ) e. ZZ )
26 5 uneq1i 
 |-  ( J u. { Y } ) = ( ( I \ { Y } ) u. { Y } )
27 4 snssd 
 |-  ( ph -> { Y } C_ I )
28 undifr 
 |-  ( { Y } C_ I <-> ( ( I \ { Y } ) u. { Y } ) = I )
29 27 28 sylib 
 |-  ( ph -> ( ( I \ { Y } ) u. { Y } ) = I )
30 26 29 eqtrid 
 |-  ( ph -> ( J u. { Y } ) = I )
31 30 fveq2d 
 |-  ( ph -> ( # ` ( J u. { Y } ) ) = ( # ` I ) )
32 difssd 
 |-  ( ph -> ( I \ { Y } ) C_ I )
33 5 32 eqsstrid 
 |-  ( ph -> J C_ I )
34 2 33 ssfid 
 |-  ( ph -> J e. Fin )
35 neldifsnd 
 |-  ( ph -> -. Y e. ( I \ { Y } ) )
36 5 eleq2i 
 |-  ( Y e. J <-> Y e. ( I \ { Y } ) )
37 35 36 sylnibr 
 |-  ( ph -> -. Y e. J )
38 hashunsng 
 |-  ( Y e. I -> ( ( J e. Fin /\ -. Y e. J ) -> ( # ` ( J u. { Y } ) ) = ( ( # ` J ) + 1 ) ) )
39 38 imp 
 |-  ( ( Y e. I /\ ( J e. Fin /\ -. Y e. J ) ) -> ( # ` ( J u. { Y } ) ) = ( ( # ` J ) + 1 ) )
40 4 34 37 39 syl12anc 
 |-  ( ph -> ( # ` ( J u. { Y } ) ) = ( ( # ` J ) + 1 ) )
41 31 40 eqtr3d 
 |-  ( ph -> ( # ` I ) = ( ( # ` J ) + 1 ) )
42 41 oveq1d 
 |-  ( ph -> ( ( # ` I ) - 1 ) = ( ( ( # ` J ) + 1 ) - 1 ) )
43 hashcl 
 |-  ( J e. Fin -> ( # ` J ) e. NN0 )
44 34 43 syl 
 |-  ( ph -> ( # ` J ) e. NN0 )
45 44 nn0cnd 
 |-  ( ph -> ( # ` J ) e. CC )
46 1cnd 
 |-  ( ph -> 1 e. CC )
47 45 46 pncand 
 |-  ( ph -> ( ( ( # ` J ) + 1 ) - 1 ) = ( # ` J ) )
48 42 47 eqtr2d 
 |-  ( ph -> ( # ` J ) = ( ( # ` I ) - 1 ) )
49 48 oveq2d 
 |-  ( ph -> ( 0 ... ( # ` J ) ) = ( 0 ... ( ( # ` I ) - 1 ) ) )
50 7 49 eleqtrd 
 |-  ( ph -> K e. ( 0 ... ( ( # ` I ) - 1 ) ) )
51 elfzp1b 
 |-  ( ( K e. ZZ /\ ( # ` I ) e. ZZ ) -> ( K e. ( 0 ... ( ( # ` I ) - 1 ) ) <-> ( K + 1 ) e. ( 1 ... ( # ` I ) ) ) )
52 51 biimpa 
 |-  ( ( ( K e. ZZ /\ ( # ` I ) e. ZZ ) /\ K e. ( 0 ... ( ( # ` I ) - 1 ) ) ) -> ( K + 1 ) e. ( 1 ... ( # ` I ) ) )
53 22 25 50 52 syl21anc 
 |-  ( ph -> ( K + 1 ) e. ( 1 ... ( # ` I ) ) )
54 15 16 17 18 19 20 2 21 4 5 6 53 8 esplyind 
 |-  ( ph -> ( ( I eSymPoly R ) ` ( K + 1 ) ) = ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) )
55 9 54 eqtrid 
 |-  ( ph -> F = ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) )
56 55 fveq2d 
 |-  ( ph -> ( Q ` F ) = ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) )
57 56 fveq1d 
 |-  ( ph -> ( ( Q ` F ) ` Z ) = ( ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ` Z ) )
58 eqid 
 |-  ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
59 10 fvexi 
 |-  B e. _V
60 59 a1i 
 |-  ( ph -> B e. _V )
61 60 2 14 elmapdd 
 |-  ( ph -> Z e. ( B ^m I ) )
62 11 15 10 58 18 1 2 3 61 16 4 evlvarval 
 |-  ( ph -> ( ( ( I mVar R ) ` Y ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( I mVar R ) ` Y ) ) ` Z ) = ( Z ` Y ) ) )
63 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
64 eqid 
 |-  ( Base ` ( J mPoly R ) ) = ( Base ` ( J mPoly R ) )
65 22 zcnd 
 |-  ( ph -> K e. CC )
66 65 46 pncand 
 |-  ( ph -> ( ( K + 1 ) - 1 ) = K )
67 66 fveq2d 
 |-  ( ph -> ( E ` ( ( K + 1 ) - 1 ) ) = ( E ` K ) )
68 6 fveq1i 
 |-  ( E ` K ) = ( ( J eSymPoly R ) ` K )
69 fz0ssnn0 
 |-  ( 0 ... ( # ` J ) ) C_ NN0
70 69 7 sselid 
 |-  ( ph -> K e. NN0 )
71 8 34 21 70 64 esplympl 
 |-  ( ph -> ( ( J eSymPoly R ) ` K ) e. ( Base ` ( J mPoly R ) ) )
72 68 71 eqeltrid 
 |-  ( ph -> ( E ` K ) e. ( Base ` ( J mPoly R ) ) )
73 67 72 eqeltrd 
 |-  ( ph -> ( E ` ( ( K + 1 ) - 1 ) ) e. ( Base ` ( J mPoly R ) ) )
74 19 63 2 21 10 5 64 4 73 58 extvfvcl 
 |-  ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) e. ( Base ` ( I mPoly R ) ) )
75 67 fveq2d 
 |-  ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) = ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) )
76 75 fveq2d 
 |-  ( ph -> ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) = ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) )
77 76 fveq1d 
 |-  ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ` Z ) = ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) ` Z ) )
78 eqid 
 |-  ( I extendVars R ) = ( I extendVars R )
79 11 12 5 64 10 78 3 2 4 72 14 evlextv 
 |-  ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) ` Z ) = ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) )
80 77 79 eqtrd 
 |-  ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) )
81 74 80 jca 
 |-  ( ph -> ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) )
82 11 15 10 58 18 1 2 3 61 62 81 evlmulval 
 |-  ( ph -> ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ) ` Z ) = ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) ) )
83 6 fveq1i 
 |-  ( E ` ( K + 1 ) ) = ( ( J eSymPoly R ) ` ( K + 1 ) )
84 peano2nn0 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN0 )
85 70 84 syl 
 |-  ( ph -> ( K + 1 ) e. NN0 )
86 8 34 21 85 64 esplympl 
 |-  ( ph -> ( ( J eSymPoly R ) ` ( K + 1 ) ) e. ( Base ` ( J mPoly R ) ) )
87 83 86 eqeltrid 
 |-  ( ph -> ( E ` ( K + 1 ) ) e. ( Base ` ( J mPoly R ) ) )
88 19 63 2 21 10 5 64 4 87 58 extvfvcl 
 |-  ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) e. ( Base ` ( I mPoly R ) ) )
89 11 12 5 64 10 78 3 2 4 87 14 evlextv 
 |-  ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) )
90 88 89 jca 
 |-  ( ph -> ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) )
91 11 15 10 58 17 13 2 3 61 82 90 evladdval 
 |-  ( ph -> ( ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ` Z ) = ( ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) ) )
92 91 simprd 
 |-  ( ph -> ( ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ` Z ) = ( ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) )
93 57 92 eqtrd 
 |-  ( ph -> ( ( Q ` F ) ` Z ) = ( ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) )