Theorem esplyval

Description: The elementary polynomials 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	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
Assertion	esplyval	⊢ ( 𝜑 → ( 𝐼 eSymPoly 𝑅 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		esplyval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2		esplyval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		esplyval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
4		df-esply	⊢ eSymPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )
5	4	a1i	⊢ ( 𝜑 → eSymPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) ) )
6		fveq2	⊢ ( 𝑟 = 𝑅 → ( ℤRHom ‘ 𝑟 ) = ( ℤRHom ‘ 𝑅 ) )
7	6	adantl	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ℤRHom ‘ 𝑟 ) = ( ℤRHom ‘ 𝑅 ) )
8		oveq2	⊢ ( 𝑖 = 𝐼 → ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) )
9	8	rabeqdv	⊢ ( 𝑖 = 𝐼 → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
10	9 1	eqtr4di	⊢ ( 𝑖 = 𝐼 → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } = 𝐷 )
11	10	fveq2d	⊢ ( 𝑖 = 𝐼 → ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) = ( 𝟭 ‘ 𝐷 ) )
12	11	adantr	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) = ( 𝟭 ‘ 𝐷 ) )
13		fveq2	⊢ ( 𝑖 = 𝐼 → ( 𝟭 ‘ 𝑖 ) = ( 𝟭 ‘ 𝐼 ) )
14	13	adantr	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝟭 ‘ 𝑖 ) = ( 𝟭 ‘ 𝐼 ) )
15		pweq	⊢ ( 𝑖 = 𝐼 → 𝒫 𝑖 = 𝒫 𝐼 )
16	15	rabeqdv	⊢ ( 𝑖 = 𝐼 → { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } = { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } )
17	16	adantr	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } = { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } )
18	14 17	imaeq12d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) = ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) )
19	12 18	fveq12d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) = ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) )
20	7 19	coeq12d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) )
21	20	mpteq2dv	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )
22	21	adantl	⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )
23	2	elexd	⊢ ( 𝜑 → 𝐼 ∈ V )
24	3	elexd	⊢ ( 𝜑 → 𝑅 ∈ V )
25		nn0ex	⊢ ℕ0 ∈ V
26	25	mptex	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) ∈ V
27	26	a1i	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) ∈ V )
28	5 22 23 24 27	ovmpod	⊢ ( 𝜑 → ( 𝐼 eSymPoly 𝑅 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )