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 ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
esplyfval2.i ⊢ φ → I ∈ Fin
esplyfval2.r ⊢ φ → R ∈ Ring
esplyfval2.k ⊢ φ → K ∈ ℕ 0 ∖ 0 … I
esplyfval2.z ⊢ Z = 0 I mPoly R
Assertion esplyfval2 Could not format assertion : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) = Z ) with typecode |-

Proof

Step Hyp Ref Expression
1 esplyfval2.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
2 esplyfval2.i ⊢ φ → I ∈ Fin
3 esplyfval2.r ⊢ φ → R ∈ Ring
4 esplyfval2.k ⊢ φ → K ∈ ℕ 0 ∖ 0 … I
5 esplyfval2.z ⊢ Z = 0 I mPoly R
6 2 adantr ⊢ φ ∧ c ∈ 𝒫 I → I ∈ Fin
7 elpwi ⊢ c ∈ 𝒫 I → c ⊆ I
8 7 adantl ⊢ φ ∧ c ∈ 𝒫 I → c ⊆ I
9 6 8 ssfid ⊢ φ ∧ c ∈ 𝒫 I → c ∈ Fin
10 hashcl ⊢ c ∈ Fin → c ∈ ℕ 0
11 9 10 syl ⊢ φ ∧ c ∈ 𝒫 I → c ∈ ℕ 0
12 11 nn0red ⊢ φ ∧ c ∈ 𝒫 I → c ∈ ℝ
13 hashcl ⊢ I ∈ Fin → I ∈ ℕ 0
14 2 13 syl ⊢ φ → I ∈ ℕ 0
15 14 nn0red ⊢ φ → I ∈ ℝ
16 15 adantr ⊢ φ ∧ c ∈ 𝒫 I → I ∈ ℝ
17 4 eldifad ⊢ φ → K ∈ ℕ 0
18 17 nn0red ⊢ φ → K ∈ ℝ
19 18 adantr ⊢ φ ∧ c ∈ 𝒫 I → K ∈ ℝ
20 hashss ⊢ I ∈ Fin ∧ c ⊆ I → c ≤ I
21 6 8 20 syl2anc ⊢ φ ∧ c ∈ 𝒫 I → c ≤ I
22 14 nn0zd ⊢ φ → I ∈ ℤ
23 nn0diffz0 ⊢ I ∈ ℕ 0 → ℕ 0 ∖ 0 … I = ℤ ≥ I + 1
24 14 23 syl ⊢ φ → ℕ 0 ∖ 0 … I = ℤ ≥ I + 1
25 4 24 eleqtrd ⊢ φ → K ∈ ℤ ≥ I + 1
26 eluzp1l ⊢ I ∈ ℤ ∧ K ∈ ℤ ≥ I + 1 → I < K
27 22 25 26 syl2anc ⊢ φ → I < K
28 27 adantr ⊢ φ ∧ c ∈ 𝒫 I → I < K
29 12 16 19 21 28 lelttrd ⊢ φ ∧ c ∈ 𝒫 I → c < K
30 12 29 ltned ⊢ φ ∧ c ∈ 𝒫 I → c ≠ K
31 30 neneqd ⊢ φ ∧ c ∈ 𝒫 I → ¬ c = K
32 31 ralrimiva ⊢ φ → ∀ c ∈ 𝒫 I ¬ c = K
33 rabeq0 ⊢ c ∈ 𝒫 I | c = K = ∅ ↔ ∀ c ∈ 𝒫 I ¬ c = K
34 32 33 sylibr ⊢ φ → c ∈ 𝒫 I | c = K = ∅
35 34 imaeq2d ⊢ φ → 𝟙 I c ∈ 𝒫 I | c = K = 𝟙 I ∅
36 ima0 ⊢ 𝟙 I ∅ = ∅
37 35 36 eqtrdi ⊢ φ → 𝟙 I c ∈ 𝒫 I | c = K = ∅
38 37 fveq2d ⊢ φ → 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K = 𝟙 D ⁡ ∅
39 ovex ⊢ ℕ 0 I ∈ V
40 1 39 rabex2 ⊢ D ∈ V
41 indconst0 ⊢ D ∈ V → 𝟙 D ⁡ ∅ = D × 0
42 40 41 mp1i ⊢ φ → 𝟙 D ⁡ ∅ = D × 0
43 38 42 eqtrd ⊢ φ → 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K = D × 0
44 43 coeq2d ⊢ φ → ℤRHom ⁡ R ∘ 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K = ℤRHom ⁡ R ∘ D × 0
45 eqid ⊢ ℤRHom ⁡ R = ℤRHom ⁡ R
46 45 zrhrhm ⊢ R ∈ Ring → ℤRHom ⁡ R ∈ ℤ ring RingHom R
47 zringbas ⊢ ℤ = Base ℤ ring
48 eqid ⊢ Base R = Base R
49 47 48 rhmf ⊢ ℤRHom ⁡ R ∈ ℤ ring RingHom R → ℤRHom ⁡ R : ℤ ⟶ Base R
50 3 46 49 3syl ⊢ φ → ℤRHom ⁡ R : ℤ ⟶ Base R
51 50 ffnd ⊢ φ → ℤRHom ⁡ R Fn ℤ
52 0zd ⊢ φ → 0 ∈ ℤ
53 fcoconst ⊢ ℤRHom ⁡ R Fn ℤ ∧ 0 ∈ ℤ → ℤRHom ⁡ R ∘ D × 0 = D × ℤRHom ⁡ R ⁡ 0
54 51 52 53 syl2anc ⊢ φ → ℤRHom ⁡ R ∘ D × 0 = D × ℤRHom ⁡ R ⁡ 0
55 eqid ⊢ 0 R = 0 R
56 45 55 zrh0 ⊢ R ∈ Ring → ℤRHom ⁡ R ⁡ 0 = 0 R
57 3 56 syl ⊢ φ → ℤRHom ⁡ R ⁡ 0 = 0 R
58 57 sneqd ⊢ φ → ℤRHom ⁡ R ⁡ 0 = 0 R
59 58 xpeq2d ⊢ φ → D × ℤRHom ⁡ R ⁡ 0 = D × 0 R
60 44 54 59 3eqtrd ⊢ φ → ℤRHom ⁡ R ∘ 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K = D × 0 R
61 1 2 3 17 esplyfval Could not format ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) with typecode |-
62 eqid ⊢ I mPoly R = I mPoly R
63 1 psrbasfsupp ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
64 3 ringgrpd ⊢ φ → R ∈ Grp
65 62 63 55 5 2 64 mpl0 ⊢ φ → Z = D × 0 R
66 60 61 65 3eqtr4d Could not format ( ph -> ( ( I eSymPoly R ) ` K ) = Z ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) = Z ) with typecode |-