Theorem esplympl

Description: Elementary symmetric polynomials are polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	esplympl.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
	esplympl.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	esplympl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	esplympl.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
	esplympl.1	⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
Assertion	esplympl	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		esplympl.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2		esplympl.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
3		esplympl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		esplympl.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
5		esplympl.1	⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
6		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
7		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
8	1 7	rabex2	⊢ 𝐷 ∈ V
9	8	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
10	1 2 3 4	esplyfval	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )
11	10	eqcomd	⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) )
12		eqid	⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
13	12	zrhrhm	⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
14		zringbas	⊢ ℤ = ( Base ‘ ℤring )
15		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16	14 15	rhmf	⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
17	3 13 16	3syl	⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
18	1 2 3 4	esplylem	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )
19		indf	⊢ ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
20	9 18 19	syl2anc	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
21		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
22		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
23	21 22	prssd	⊢ ( 𝜑 → { 0 , 1 } ⊆ ℤ )
24	20 23	fssd	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ ℤ )
25	17 24	fcod	⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
26	11 25	feq1dd	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
27	6 9 26	elmapdd	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
28		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
29	1	psrbasfsupp	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
30		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
31	28 15 29 30 2	psrbas	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
32	27 31	eleqtrrd	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
33		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
34		zex	⊢ ℤ ∈ V
35	34	a1i	⊢ ( 𝜑 → ℤ ∈ V )
36		indf1o	⊢ ( 𝐼 ∈ Fin → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) )
37		f1of	⊢ ( ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
38	2 36 37	3syl	⊢ ( 𝜑 → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
39	38	ffund	⊢ ( 𝜑 → Fun ( 𝟭 ‘ 𝐼 ) )
40	2	pwexd	⊢ ( 𝜑 → 𝒫 𝐼 ∈ V )
41		ssrab2	⊢ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼
42	41	a1i	⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼 )
43	40 42	ssexd	⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ V )
44		hashcl	⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
45	2 44	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
46	4	nn0zd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
47		bccl	⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( ♯ ‘ 𝐼 ) C 𝐾 ) ∈ ℕ0 )
48	45 46 47	syl2anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) C 𝐾 ) ∈ ℕ0 )
49		hashbc	⊢ ( ( 𝐼 ∈ Fin ∧ 𝐾 ∈ ℤ ) → ( ( ♯ ‘ 𝐼 ) C 𝐾 ) = ( ♯ ‘ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
50	2 46 49	syl2anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) C 𝐾 ) = ( ♯ ‘ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
51	50	eqcomd	⊢ ( 𝜑 → ( ♯ ‘ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) = ( ( ♯ ‘ 𝐼 ) C 𝐾 ) )
52		hashvnfin	⊢ ( ( { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ V ∧ ( ( ♯ ‘ 𝐼 ) C 𝐾 ) ∈ ℕ0 ) → ( ( ♯ ‘ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) = ( ( ♯ ‘ 𝐼 ) C 𝐾 ) → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ Fin ) )
53	52	imp	⊢ ( ( ( { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ V ∧ ( ( ♯ ‘ 𝐼 ) C 𝐾 ) ∈ ℕ0 ) ∧ ( ♯ ‘ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) = ( ( ♯ ‘ 𝐼 ) C 𝐾 ) ) → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ Fin )
54	43 48 51 53	syl21anc	⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ Fin )
55		imafi	⊢ ( ( Fun ( 𝟭 ‘ 𝐼 ) ∧ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ Fin ) → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∈ Fin )
56	39 54 55	syl2anc	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∈ Fin )
57	9 18 56	indfsd	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) finSupp 0 )
58		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
59	12 58	zrh0	⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
60	3 59	syl	⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
61	33 21 20 17 23 9 35 57 60	fsuppcor	⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) finSupp ( 0g ‘ 𝑅 ) )
62	10 61	eqbrtrd	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) finSupp ( 0g ‘ 𝑅 ) )
63		eqid	⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
64	63 28 30 58 5	mplelbas	⊢ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ 𝑀 ↔ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) finSupp ( 0g ‘ 𝑅 ) ) )
65	32 62 64	sylanbrc	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ 𝑀 )