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 Could not format assertion : No typesetting found for |- eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cesply Could not format eSymPoly : No typesetting found for class eSymPoly with typecode class
1 vi setvar i
2 cvv class V
3 vr setvar r
4 vk setvar k
5 cn0 class ℕ 0
6 czrh class ℤRHom
7 3 cv setvar r
8 7 6 cfv class ℤRHom ⁡ r
9 cind class 𝟙
10 vh setvar h
11 cmap class ↑ 𝑚
12 1 cv setvar i
13 5 12 11 co class ℕ 0 i
14 10 cv setvar h
15 cfsupp class finSupp
16 cc0 class 0
17 14 16 15 wbr wff finSupp 0 ⁡ h
18 17 10 13 crab class h ∈ ℕ 0 i | finSupp 0 ⁡ h
19 18 9 cfv class 𝟙 h ∈ ℕ 0 i | finSupp 0 ⁡ h
20 12 9 cfv class 𝟙 i
21 vc setvar c
22 12 cpw class 𝒫 i
23 chash class .
24 21 cv setvar c
25 24 23 cfv class c
26 4 cv setvar k
27 25 26 wceq wff c = k
28 27 21 22 crab class c ∈ 𝒫 i | c = k
29 20 28 cima class 𝟙 i c ∈ 𝒫 i | c = k
30 29 19 cfv class 𝟙 h ∈ ℕ 0 i | finSupp 0 ⁡ h ⁡ 𝟙 i c ∈ 𝒫 i | c = k
31 8 30 ccom class ℤRHom ⁡ r ∘ 𝟙 h ∈ ℕ 0 i | finSupp 0 ⁡ h ⁡ 𝟙 i c ∈ 𝒫 i | c = k
32 4 5 31 cmpt class k ∈ ℕ 0 ⟼ ℤRHom ⁡ r ∘ 𝟙 h ∈ ℕ 0 i | finSupp 0 ⁡ h ⁡ 𝟙 i c ∈ 𝒫 i | c = k
33 1 3 2 2 32 cmpo class i ∈ V , r ∈ V ⟼ k ∈ ℕ 0 ⟼ ℤRHom ⁡ r ∘ 𝟙 h ∈ ℕ 0 i | finSupp 0 ⁡ h ⁡ 𝟙 i c ∈ 𝒫 i | c = k
34 0 33 wceq Could not format eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) ) : No typesetting found for wff eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) ) with typecode wff