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

Metamath Proof Explorer

Theorem esplyfval2

Description: When K is out-of-bounds, the K -th elementary symmetric polynomial is zero. (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses esplyfval2.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
esplyfval2.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplyfval2.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
esplyfval2.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℕ0 ∖ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) )
esplyfval2.z ⊢ 𝑍 = ( 0g ‘ ( 𝐼 mPoly 𝑅 ) )
Assertion esplyfval2 ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 esplyfval2.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 esplyfval2.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
3 esplyfval2.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 esplyfval2.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℕ0 ∖ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) )
5 esplyfval2.z ⊢ 𝑍 = ( 0g ‘ ( 𝐼 mPoly 𝑅 ) )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → 𝐼 ∈ Fin )
7 elpwi ⊢ ( 𝑐 ∈ 𝒫 𝐼 → 𝑐 ⊆ 𝐼 )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → 𝑐 ⊆ 𝐼 )
9 6 8 ssfid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → 𝑐 ∈ Fin )
10 hashcl ⊢ ( 𝑐 ∈ Fin → ( ♯ ‘ 𝑐 ) ∈ ℕ0 )
11 9 10 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → ( ♯ ‘ 𝑐 ) ∈ ℕ0 )
12 11 nn0red ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → ( ♯ ‘ 𝑐 ) ∈ ℝ )
13 hashcl ⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
14 2 13 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
15 14 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℝ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → ( ♯ ‘ 𝐼 ) ∈ ℝ )
17 4 eldifad ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
18 17 nn0red ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → 𝐾 ∈ ℝ )
20 hashss ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑐 ⊆ 𝐼 ) → ( ♯ ‘ 𝑐 ) ≤ ( ♯ ‘ 𝐼 ) )
21 6 8 20 syl2anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → ( ♯ ‘ 𝑐 ) ≤ ( ♯ ‘ 𝐼 ) )
22 14 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℤ )
23 nn0diffz0 ⊢ ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 → ( ℕ0 ∖ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) = ( ℤ≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
24 14 23 syl ⊢ ( 𝜑 → ( ℕ0 ∖ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) = ( ℤ≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
25 4 24 eleqtrd ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
26 eluzp1l ⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℤ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) ) → ( ♯ ‘ 𝐼 ) < 𝐾 )
27 22 25 26 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) < 𝐾 )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → ( ♯ ‘ 𝐼 ) < 𝐾 )
29 12 16 19 21 28 lelttrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → ( ♯ ‘ 𝑐 ) < 𝐾 )
30 12 29 ltned ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → ( ♯ ‘ 𝑐 ) ≠ 𝐾 )
31 30 neneqd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝒫 𝐼 ) → ¬ ( ♯ ‘ 𝑐 ) = 𝐾 )
32 31 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝒫 𝐼 ¬ ( ♯ ‘ 𝑐 ) = 𝐾 )
33 rabeq0 ⊢ ( { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } = ∅ ↔ ∀ 𝑐 ∈ 𝒫 𝐼 ¬ ( ♯ ‘ 𝑐 ) = 𝐾 )
34 32 33 sylibr ⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } = ∅ )
35 34 imaeq2d ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) = ( ( 𝟭 ‘ 𝐼 ) “ ∅ ) )
36 ima0 ⊢ ( ( 𝟭 ‘ 𝐼 ) “ ∅ ) = ∅
37 35 36 eqtrdi ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) = ∅ )
38 37 fveq2d ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) = ( ( 𝟭 ‘ 𝐷 ) ‘ ∅ ) )
39 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
40 1 39 rabex2 ⊢ 𝐷 ∈ V
41 indconst0 ⊢ ( 𝐷 ∈ V → ( ( 𝟭 ‘ 𝐷 ) ‘ ∅ ) = ( 𝐷 × { 0 } ) )
42 40 41 mp1i ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ∅ ) = ( 𝐷 × { 0 } ) )
43 38 42 eqtrd ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) = ( 𝐷 × { 0 } ) )
44 43 coeq2d ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( 𝐷 × { 0 } ) ) )
45 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
46 45 zrhrhm ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
47 zringbas ⊢ ℤ = ( Base ‘ ℤring )
48 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
49 47 48 rhmf ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
50 3 46 49 3syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
51 50 ffnd ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) Fn ℤ )
52 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
53 fcoconst ⊢ ( ( ( ℤRHom ‘ 𝑅 ) Fn ℤ ∧ 0 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( 𝐷 × { 0 } ) ) = ( 𝐷 × { ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) } ) )
54 51 52 53 syl2anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( 𝐷 × { 0 } ) ) = ( 𝐷 × { ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) } ) )
55 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
56 45 55 zrh0 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
57 3 56 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
58 57 sneqd ⊢ ( 𝜑 → { ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) } = { ( 0g ‘ 𝑅 ) } )
59 58 xpeq2d ⊢ ( 𝜑 → ( 𝐷 × { ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) } ) = ( 𝐷 × { ( 0g ‘ 𝑅 ) } ) )
60 44 54 59 3eqtrd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) = ( 𝐷 × { ( 0g ‘ 𝑅 ) } ) )
61 1 2 3 17 esplyfval ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )
62 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
63 1 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
64 3 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
65 62 63 55 5 2 64 mpl0 ⊢ ( 𝜑 → 𝑍 = ( 𝐷 × { ( 0g ‘ 𝑅 ) } ) )
66 60 61 65 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = 𝑍 )