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

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
esplyfvn.2 ⊢ + = ( +g ‘ 𝑅 )
esplyfvn.3 ⊢ · = ( .r ‘ 𝑅 )
esplyfvn.4 ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
esplyfvn.5 ⊢ 𝑂 = ( 𝐽 eval 𝑅 )
esplyfvn.6 ⊢ 𝐸 = ( 𝐼 eSymPoly 𝑅 )
esplyfvn.7 ⊢ 𝐹 = ( 𝐽 eSymPoly 𝑅 )
esplyfvn.8 ⊢ 𝐻 = ( ♯ ‘ 𝐼 )
esplyfvn.9 ⊢ 𝐾 = ( ♯ ‘ 𝐽 )
esplyfvn.10 ⊢ 𝐽 = ( 𝐼 ∖ { 𝑌 } )
esplyfvn.11 ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplyfvn.12 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
esplyfvn.13 ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
esplyfvn.14 ⊢ ( 𝜑 → 𝑍 : 𝐼 ⟶ 𝐵 )
Assertion esplyfvn ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐻 ) ) ‘ 𝑍 ) = ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )

Proof

Step Hyp Ref Expression
1 esplyfvn.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 esplyfvn.2 ⊢ + = ( +g ‘ 𝑅 )
3 esplyfvn.3 ⊢ · = ( .r ‘ 𝑅 )
4 esplyfvn.4 ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
5 esplyfvn.5 ⊢ 𝑂 = ( 𝐽 eval 𝑅 )
6 esplyfvn.6 ⊢ 𝐸 = ( 𝐼 eSymPoly 𝑅 )
7 esplyfvn.7 ⊢ 𝐹 = ( 𝐽 eSymPoly 𝑅 )
8 esplyfvn.8 ⊢ 𝐻 = ( ♯ ‘ 𝐼 )
9 esplyfvn.9 ⊢ 𝐾 = ( ♯ ‘ 𝐽 )
10 esplyfvn.10 ⊢ 𝐽 = ( 𝐼 ∖ { 𝑌 } )
11 esplyfvn.11 ⊢ ( 𝜑 → 𝐼 ∈ Fin )
12 esplyfvn.12 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
13 esplyfvn.13 ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
14 esplyfvn.14 ⊢ ( 𝜑 → 𝑍 : 𝐼 ⟶ 𝐵 )
15 hashdifsn ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑌 ∈ 𝐼 ) → ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) ) = ( ( ♯ ‘ 𝐼 ) − 1 ) )
16 11 13 15 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) ) = ( ( ♯ ‘ 𝐼 ) − 1 ) )
17 10 fveq2i ⊢ ( ♯ ‘ 𝐽 ) = ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) )
18 9 17 eqtri ⊢ 𝐾 = ( ♯ ‘ ( 𝐼 ∖ { 𝑌 } ) )
19 8 oveq1i ⊢ ( 𝐻 − 1 ) = ( ( ♯ ‘ 𝐼 ) − 1 )
20 16 18 19 3eqtr4g ⊢ ( 𝜑 → 𝐾 = ( 𝐻 − 1 ) )
21 20 oveq1d ⊢ ( 𝜑 → ( 𝐾 + 1 ) = ( ( 𝐻 − 1 ) + 1 ) )
22 hashcl ⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
23 11 22 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
24 8 23 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
25 24 nn0cnd ⊢ ( 𝜑 → 𝐻 ∈ ℂ )
26 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
27 25 26 npcand ⊢ ( 𝜑 → ( ( 𝐻 − 1 ) + 1 ) = 𝐻 )
28 21 27 eqtr2d ⊢ ( 𝜑 → 𝐻 = ( 𝐾 + 1 ) )
29 28 fveq2d ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐻 ) = ( 𝐸 ‘ ( 𝐾 + 1 ) ) )
30 29 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐸 ‘ 𝐻 ) ) = ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) )
31 30 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐻 ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ‘ 𝑍 ) )
32 difssd ⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑌 } ) ⊆ 𝐼 )
33 10 32 eqsstrid ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
34 11 33 ssfid ⊢ ( 𝜑 → 𝐽 ∈ Fin )
35 hashcl ⊢ ( 𝐽 ∈ Fin → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
36 34 35 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
37 9 36 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
38 nn0fz0 ⊢ ( 𝐾 ∈ ℕ0 ↔ 𝐾 ∈ ( 0 ... 𝐾 ) )
39 37 38 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... 𝐾 ) )
40 9 oveq2i ⊢ ( 0 ... 𝐾 ) = ( 0 ... ( ♯ ‘ 𝐽 ) )
41 39 40 eleqtrdi ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
42 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 }
43 6 fveq1i ⊢ ( 𝐸 ‘ ( 𝐾 + 1 ) ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) )
44 3 11 12 13 10 7 41 42 43 1 4 5 2 14 esplyindfv ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ‘ 𝑍 ) = ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )
45 7 fveq1i ⊢ ( 𝐹 ‘ ( 𝐾 + 1 ) ) = ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) )
46 12 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
47 28 24 eqeltrrd ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ0 )
48 fzp1nel ⊢ ¬ ( 𝐾 + 1 ) ∈ ( 0 ... 𝐾 )
49 48 a1i ⊢ ( 𝜑 → ¬ ( 𝐾 + 1 ) ∈ ( 0 ... 𝐾 ) )
50 40 eleq2i ⊢ ( ( 𝐾 + 1 ) ∈ ( 0 ... 𝐾 ) ↔ ( 𝐾 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
51 49 50 sylnib ⊢ ( 𝜑 → ¬ ( 𝐾 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
52 47 51 eldifd ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ( ℕ0 ∖ ( 0 ... ( ♯ ‘ 𝐽 ) ) ) )
53 eqid ⊢ ( 0g ‘ ( 𝐽 mPoly 𝑅 ) ) = ( 0g ‘ ( 𝐽 mPoly 𝑅 ) )
54 42 34 46 52 53 esplyfval2 ⊢ ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) ) = ( 0g ‘ ( 𝐽 mPoly 𝑅 ) ) )
55 45 54 eqtrid ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐾 + 1 ) ) = ( 0g ‘ ( 𝐽 mPoly 𝑅 ) ) )
56 eqid ⊢ ( 𝐽 mPoly 𝑅 ) = ( 𝐽 mPoly 𝑅 )
57 eqid ⊢ ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) = ( algSc ‘ ( 𝐽 mPoly 𝑅 ) )
58 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
59 56 57 58 53 34 46 mplascl0 ⊢ ( 𝜑 → ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ ( 𝐽 mPoly 𝑅 ) ) )
60 55 59 eqtr4d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐾 + 1 ) ) = ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 0g ‘ 𝑅 ) ) )
61 60 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) = ( 𝑂 ‘ ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 0g ‘ 𝑅 ) ) ) )
62 61 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) = ( ( 𝑂 ‘ ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 0g ‘ 𝑅 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) )
63 12 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
64 1 58 grpidcl ⊢ ( 𝑅 ∈ Grp → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
65 63 64 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
66 14 33 fssresd ⊢ ( 𝜑 → ( 𝑍 ↾ 𝐽 ) : 𝐽 ⟶ 𝐵 )
67 5 56 1 57 34 12 65 66 evlscaval ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ ( 𝐽 mPoly 𝑅 ) ) ‘ ( 0g ‘ 𝑅 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) = ( 0g ‘ 𝑅 ) )
68 62 67 eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) = ( 0g ‘ 𝑅 ) )
69 68 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) = ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( 0g ‘ 𝑅 ) ) )
70 14 13 ffvelcdmd ⊢ ( 𝜑 → ( 𝑍 ‘ 𝑌 ) ∈ 𝐵 )
71 eqid ⊢ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
72 7 fveq1i ⊢ ( 𝐹 ‘ 𝐾 ) = ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝐾 )
73 42 34 46 37 71 esplympl ⊢ ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
74 72 73 eqeltrid ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
75 1 fvexi ⊢ 𝐵 ∈ V
76 75 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
77 76 34 66 elmapdd ⊢ ( 𝜑 → ( 𝑍 ↾ 𝐽 ) ∈ ( 𝐵 ↑m 𝐽 ) )
78 5 56 71 1 34 12 74 77 evlcl ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ∈ 𝐵 )
79 1 3 46 70 78 ringcld ⊢ ( 𝜑 → ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) ∈ 𝐵 )
80 1 2 58 63 79 grpridd ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( 0g ‘ 𝑅 ) ) = ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )
81 69 80 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( ( 𝑂 ‘ ( 𝐹 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) = ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )
82 31 44 81 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐸 ‘ 𝐻 ) ) ‘ 𝑍 ) = ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐹 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )