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

Metamath Proof Explorer

Definition df-esply

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

Ref Expression
Assertion df-esply eSymPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cesply ⊢ eSymPoly
1 vi ⊢ 𝑖
2 cvv ⊢ V
3 vr ⊢ 𝑟
4 vk ⊢ 𝑘
5 cn0 ⊢ ℕ0
6 czrh ⊢ ℤRHom
7 3 cv ⊢ 𝑟
8 7 6 cfv ⊢ ( ℤRHom ‘ 𝑟 )
9 cind ⊢ 𝟭
10 vh ⊢ ℎ
11 cmap ⊢ ↑m
12 1 cv ⊢ 𝑖
13 5 12 11 co ⊢ ( ℕ0 ↑m 𝑖 )
14 10 cv ⊢ ℎ
15 cfsupp ⊢ finSupp
16 cc0 ⊢ 0
17 14 16 15 wbr ⊢ ℎ finSupp 0
18 17 10 13 crab ⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 }
19 18 9 cfv ⊢ ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } )
20 12 9 cfv ⊢ ( 𝟭 ‘ 𝑖 )
21 vc ⊢ 𝑐
22 12 cpw ⊢ 𝒫 𝑖
23 chash ⊢ ♯
24 21 cv ⊢ 𝑐
25 24 23 cfv ⊢ ( ♯ ‘ 𝑐 )
26 4 cv ⊢ 𝑘
27 25 26 wceq ⊢ ( ♯ ‘ 𝑐 ) = 𝑘
28 27 21 22 crab ⊢ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 }
29 20 28 cima ⊢ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } )
30 29 19 cfv ⊢ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) )
31 8 30 ccom ⊢ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) )
32 4 5 31 cmpt ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) )
33 1 3 2 2 32 cmpo ⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )
34 0 33 wceq ⊢ eSymPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( ℤRHom ‘ 𝑟 ) ∘ ( ( 𝟭 ‘ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ) ‘ ( ( 𝟭 ‘ 𝑖 ) “ { 𝑐 ∈ 𝒫 𝑖 ∣ ( ♯ ‘ 𝑐 ) = 𝑘 } ) ) ) ) )