Metamath Proof Explorer

Theorem esplyfvn

Description: Express the last elementary symmetric polynomial, evaluated at a given set of points Z , in terms of the last elementary symmetric polynomial with one less variable. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses esplyfvn.1 
|- B = ( Base ` R )
esplyfvn.2 
|- .+ = ( +g ` R )
esplyfvn.3 
|- .x. = ( .r ` R )
esplyfvn.4 
|- Q = ( I eval R )
esplyfvn.5 
|- O = ( J eval R )
esplyfvn.6 
|- E = ( I eSymPoly R )
esplyfvn.7 
|- F = ( J eSymPoly R )
esplyfvn.8 
|- H = ( # ` I )
esplyfvn.9 
|- K = ( # ` J )
esplyfvn.10 
|- J = ( I \ { Y } )
esplyfvn.11 
|- ( ph -> I e. Fin )
esplyfvn.12 
|- ( ph -> R e. CRing )
esplyfvn.13 
|- ( ph -> Y e. I )
esplyfvn.14 
|- ( ph -> Z : I --> B )
Assertion esplyfvn 
|- ( ph -> ( ( Q ` ( E ` H ) ) ` Z ) = ( ( Z ` Y ) .x. ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) ) )

Proof

Step Hyp Ref Expression
1 esplyfvn.1 
 |-  B = ( Base ` R )
2 esplyfvn.2 
 |-  .+ = ( +g ` R )
3 esplyfvn.3 
 |-  .x. = ( .r ` R )
4 esplyfvn.4 
 |-  Q = ( I eval R )
5 esplyfvn.5 
 |-  O = ( J eval R )
6 esplyfvn.6 
 |-  E = ( I eSymPoly R )
7 esplyfvn.7 
 |-  F = ( J eSymPoly R )
8 esplyfvn.8 
 |-  H = ( # ` I )
9 esplyfvn.9 
 |-  K = ( # ` J )
10 esplyfvn.10 
 |-  J = ( I \ { Y } )
11 esplyfvn.11 
 |-  ( ph -> I e. Fin )
12 esplyfvn.12 
 |-  ( ph -> R e. CRing )
13 esplyfvn.13 
 |-  ( ph -> Y e. I )
14 esplyfvn.14 
 |-  ( ph -> Z : I --> B )
15 hashdifsn 
 |-  ( ( I e. Fin /\ Y e. I ) -> ( # ` ( I \ { Y } ) ) = ( ( # ` I ) - 1 ) )
16 11 13 15 syl2anc 
 |-  ( ph -> ( # ` ( I \ { Y } ) ) = ( ( # ` I ) - 1 ) )
17 10 fveq2i 
 |-  ( # ` J ) = ( # ` ( I \ { Y } ) )
18 9 17 eqtri 
 |-  K = ( # ` ( I \ { Y } ) )
19 8 oveq1i 
 |-  ( H - 1 ) = ( ( # ` I ) - 1 )
20 16 18 19 3eqtr4g 
 |-  ( ph -> K = ( H - 1 ) )
21 20 oveq1d 
 |-  ( ph -> ( K + 1 ) = ( ( H - 1 ) + 1 ) )
22 hashcl 
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
23 11 22 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
24 8 23 eqeltrid 
 |-  ( ph -> H e. NN0 )
25 24 nn0cnd 
 |-  ( ph -> H e. CC )
26 1cnd 
 |-  ( ph -> 1 e. CC )
27 25 26 npcand 
 |-  ( ph -> ( ( H - 1 ) + 1 ) = H )
28 21 27 eqtr2d 
 |-  ( ph -> H = ( K + 1 ) )
29 28 fveq2d 
 |-  ( ph -> ( E ` H ) = ( E ` ( K + 1 ) ) )
30 29 fveq2d 
 |-  ( ph -> ( Q ` ( E ` H ) ) = ( Q ` ( E ` ( K + 1 ) ) ) )
31 30 fveq1d 
 |-  ( ph -> ( ( Q ` ( E ` H ) ) ` Z ) = ( ( Q ` ( E ` ( K + 1 ) ) ) ` Z ) )
32 difssd 
 |-  ( ph -> ( I \ { Y } ) C_ I )
33 10 32 eqsstrid 
 |-  ( ph -> J C_ I )
34 11 33 ssfid 
 |-  ( ph -> J e. Fin )
35 hashcl 
 |-  ( J e. Fin -> ( # ` J ) e. NN0 )
36 34 35 syl 
 |-  ( ph -> ( # ` J ) e. NN0 )
37 9 36 eqeltrid 
 |-  ( ph -> K e. NN0 )
38 nn0fz0 
 |-  ( K e. NN0 <-> K e. ( 0 ... K ) )
39 37 38 sylib 
 |-  ( ph -> K e. ( 0 ... K ) )
40 9 oveq2i 
 |-  ( 0 ... K ) = ( 0 ... ( # ` J ) )
41 39 40 eleqtrdi 
 |-  ( ph -> K e. ( 0 ... ( # ` J ) ) )
42 eqid 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } = { h e. ( NN0 ^m J ) | h finSupp 0 }
43 6 fveq1i 
 |-  ( E ` ( K + 1 ) ) = ( ( I eSymPoly R ) ` ( K + 1 ) )
44 3 11 12 13 10 7 41 42 43 1 4 5 2 14 esplyindfv 
 |-  ( ph -> ( ( Q ` ( E ` ( K + 1 ) ) ) ` Z ) = ( ( ( Z ` Y ) .x. ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( F ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) )
45 7 fveq1i 
 |-  ( F ` ( K + 1 ) ) = ( ( J eSymPoly R ) ` ( K + 1 ) )
46 12 crngringd 
 |-  ( ph -> R e. Ring )
47 28 24 eqeltrrd 
 |-  ( ph -> ( K + 1 ) e. NN0 )
48 fzp1nel 
 |-  -. ( K + 1 ) e. ( 0 ... K )
49 48 a1i 
 |-  ( ph -> -. ( K + 1 ) e. ( 0 ... K ) )
50 40 eleq2i 
 |-  ( ( K + 1 ) e. ( 0 ... K ) <-> ( K + 1 ) e. ( 0 ... ( # ` J ) ) )
51 49 50 sylnib 
 |-  ( ph -> -. ( K + 1 ) e. ( 0 ... ( # ` J ) ) )
52 47 51 eldifd 
 |-  ( ph -> ( K + 1 ) e. ( NN0 \ ( 0 ... ( # ` J ) ) ) )
53 eqid 
 |-  ( 0g ` ( J mPoly R ) ) = ( 0g ` ( J mPoly R ) )
54 42 34 46 52 53 esplyfval2 
 |-  ( ph -> ( ( J eSymPoly R ) ` ( K + 1 ) ) = ( 0g ` ( J mPoly R ) ) )
55 45 54 eqtrid 
 |-  ( ph -> ( F ` ( K + 1 ) ) = ( 0g ` ( J mPoly R ) ) )
56 eqid 
 |-  ( J mPoly R ) = ( J mPoly R )
57 eqid 
 |-  ( algSc ` ( J mPoly R ) ) = ( algSc ` ( J mPoly R ) )
58 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
59 56 57 58 53 34 46 mplascl0 
 |-  ( ph -> ( ( algSc ` ( J mPoly R ) ) ` ( 0g ` R ) ) = ( 0g ` ( J mPoly R ) ) )
60 55 59 eqtr4d 
 |-  ( ph -> ( F ` ( K + 1 ) ) = ( ( algSc ` ( J mPoly R ) ) ` ( 0g ` R ) ) )
61 60 fveq2d 
 |-  ( ph -> ( O ` ( F ` ( K + 1 ) ) ) = ( O ` ( ( algSc ` ( J mPoly R ) ) ` ( 0g ` R ) ) ) )
62 61 fveq1d 
 |-  ( ph -> ( ( O ` ( F ` ( K + 1 ) ) ) ` ( Z |` J ) ) = ( ( O ` ( ( algSc ` ( J mPoly R ) ) ` ( 0g ` R ) ) ) ` ( Z |` J ) ) )
63 12 crnggrpd 
 |-  ( ph -> R e. Grp )
64 1 58 grpidcl 
 |-  ( R e. Grp -> ( 0g ` R ) e. B )
65 63 64 syl 
 |-  ( ph -> ( 0g ` R ) e. B )
66 14 33 fssresd 
 |-  ( ph -> ( Z |` J ) : J --> B )
67 5 56 1 57 34 12 65 66 evlscaval 
 |-  ( ph -> ( ( O ` ( ( algSc ` ( J mPoly R ) ) ` ( 0g ` R ) ) ) ` ( Z |` J ) ) = ( 0g ` R ) )
68 62 67 eqtrd 
 |-  ( ph -> ( ( O ` ( F ` ( K + 1 ) ) ) ` ( Z |` J ) ) = ( 0g ` R ) )
69 68 oveq2d 
 |-  ( ph -> ( ( ( Z ` Y ) .x. ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( F ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) = ( ( ( Z ` Y ) .x. ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) ) .+ ( 0g ` R ) ) )
70 14 13 ffvelcdmd 
 |-  ( ph -> ( Z ` Y ) e. B )
71 eqid 
 |-  ( Base ` ( J mPoly R ) ) = ( Base ` ( J mPoly R ) )
72 7 fveq1i 
 |-  ( F ` K ) = ( ( J eSymPoly R ) ` K )
73 42 34 46 37 71 esplympl 
 |-  ( ph -> ( ( J eSymPoly R ) ` K ) e. ( Base ` ( J mPoly R ) ) )
74 72 73 eqeltrid 
 |-  ( ph -> ( F ` K ) e. ( Base ` ( J mPoly R ) ) )
75 1 fvexi 
 |-  B e. _V
76 75 a1i 
 |-  ( ph -> B e. _V )
77 76 34 66 elmapdd 
 |-  ( ph -> ( Z |` J ) e. ( B ^m J ) )
78 5 56 71 1 34 12 74 77 evlcl 
 |-  ( ph -> ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) e. B )
79 1 3 46 70 78 ringcld 
 |-  ( ph -> ( ( Z ` Y ) .x. ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) ) e. B )
80 1 2 58 63 79 grpridd 
 |-  ( ph -> ( ( ( Z ` Y ) .x. ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) ) .+ ( 0g ` R ) ) = ( ( Z ` Y ) .x. ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) ) )
81 69 80 eqtrd 
 |-  ( ph -> ( ( ( Z ` Y ) .x. ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( F ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) = ( ( Z ` Y ) .x. ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) ) )
82 31 44 81 3eqtrd 
 |-  ( ph -> ( ( Q ` ( E ` H ) ) ` Z ) = ( ( Z ` Y ) .x. ( ( O ` ( F ` K ) ) ` ( Z |` J ) ) ) )