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

Metamath Proof Explorer

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 ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
esplyval.i ⊢ φ → I ∈ V
esplyval.r ⊢ φ → R ∈ W
esplyfval.k ⊢ φ → K ∈ ℕ 0
Assertion esplyfval Could not format assertion : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 esplyval.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
2 esplyval.i ⊢ φ → I ∈ V
3 esplyval.r ⊢ φ → R ∈ W
4 esplyfval.k ⊢ φ → K ∈ ℕ 0
5 eqeq2 ⊢ k = K → c = k ↔ c = K
6 5 rabbidv ⊢ k = K → c ∈ 𝒫 I | c = k = c ∈ 𝒫 I | c = K
7 6 imaeq2d ⊢ k = K → 𝟙 I c ∈ 𝒫 I | c = k = 𝟙 I c ∈ 𝒫 I | c = K
8 7 fveq2d ⊢ k = K → 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = k = 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K
9 8 coeq2d ⊢ k = K → ℤRHom ⁡ R ∘ 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = k = ℤRHom ⁡ R ∘ 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K
10 1 2 3 esplyval Could not format ( ph -> ( I eSymPoly R ) = ( k e. NN0 |-> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = k } ) ) ) ) ) : No typesetting found for |- ( ph -> ( I eSymPoly R ) = ( k e. NN0 |-> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = k } ) ) ) ) ) with typecode |-
11 fvexd ⊢ φ → ℤRHom ⁡ R ∈ V
12 fvexd ⊢ φ → 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K ∈ V
13 11 12 coexd ⊢ φ → ℤRHom ⁡ R ∘ 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K ∈ V
14 9 10 4 13 fvmptd4 Could not format ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) with typecode |-