Theorem esplyfval

Description: The K -th elementary polynomial for a given index I of variables and base ring R . (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	esplyval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
	esplyval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	esplyval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
	esplyfval.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion	esplyfval	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		esplyval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2		esplyval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		esplyval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
4		esplyfval.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
5		eqeq2	⊢ ( 𝑘 = 𝐾 → ( ( ♯ ‘ 𝑐 ) = 𝑘 ↔ ( ♯ ‘ 𝑐 ) = 𝐾 ) )
6	5	rabbidv	⊢ ( 𝑘 = 𝐾 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } = { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } )
7	6	imaeq2d	⊢ ( 𝑘 = 𝐾 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) = ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
8	7	fveq2d	⊢ ( 𝑘 = 𝐾 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) = ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) )
9	8	coeq2d	⊢ ( 𝑘 = 𝐾 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )
10	1 2 3	esplyval	⊢ ( 𝜑 → ( 𝐼 eSymPoly 𝑅 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )
11		fvexd	⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) ∈ V )
12		fvexd	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∈ V )
13	11 12	coexd	⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) ∈ V )
14	9 10 4 13	fvmptd4	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )