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 𝑅 ) ‘ 𝐾 ) = 𝑍 )