This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )