Metamath Proof Explorer

Theorem esplyfv1

Description: Coefficient for the K -th elementary symmetric polynomial and a bag of variables F where variables are not raised to a power. (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses esplyfv.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
esplyfv.i ⊢ φ → I ∈ Fin
esplyfv.r ⊢ φ → R ∈ Ring
esplyfv.k ⊢ φ → K ∈ 0 … I
esplyfv.f ⊢ φ → F ∈ D
esplyfv.0 ⊢ 0 ˙ = 0 R
esplyfv.1 ⊢ 1 ˙ = 1 R
esplyfv1.1 ⊢ φ → ran ⁡ F ⊆ 0 1
Assertion esplyfv1 Could not format assertion : No typesetting found for |- ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 esplyfv.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
2 esplyfv.i ⊢ φ → I ∈ Fin
3 esplyfv.r ⊢ φ → R ∈ Ring
4 esplyfv.k ⊢ φ → K ∈ 0 … I
5 esplyfv.f ⊢ φ → F ∈ D
6 esplyfv.0 ⊢ 0 ˙ = 0 R
7 esplyfv.1 ⊢ 1 ˙ = 1 R
8 esplyfv1.1 ⊢ φ → ran ⁡ F ⊆ 0 1
9 elfznn0 ⊢ K ∈ 0 … I → K ∈ ℕ 0
10 4 9 syl ⊢ φ → K ∈ ℕ 0
11 1 2 3 10 esplyfval 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 |-
12 11 fveq1d Could not format ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` F ) ) : No typesetting found for |- ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` F ) ) with typecode |-
13 ovex ⊢ ℕ 0 I ∈ V
14 1 ssrab3 ⊢ D ⊆ ℕ 0 I
15 13 14 ssexi ⊢ D ∈ V
16 15 a1i ⊢ φ → D ∈ V
17 nfv ⊢ Ⅎ d φ
18 indf1o ⊢ I ∈ Fin → 𝟙 I : 𝒫 I ⟶ 1-1 onto 0 1 I
19 f1of ⊢ 𝟙 I : 𝒫 I ⟶ 1-1 onto 0 1 I → 𝟙 I : 𝒫 I ⟶ 0 1 I
20 2 18 19 3syl ⊢ φ → 𝟙 I : 𝒫 I ⟶ 0 1 I
21 20 ffund ⊢ φ → Fun ⁡ 𝟙 I
22 breq1 ⊢ h = 𝟙 I ⁡ d → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ 𝟙 I ⁡ d
23 nn0ex ⊢ ℕ 0 ∈ V
24 23 a1i ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → ℕ 0 ∈ V
25 2 adantr ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → I ∈ Fin
26 ssrab2 ⊢ c ∈ 𝒫 I | c = K ⊆ 𝒫 I
27 26 a1i ⊢ φ → c ∈ 𝒫 I | c = K ⊆ 𝒫 I
28 27 sselda ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → d ∈ 𝒫 I
29 28 elpwid ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → d ⊆ I
30 indf ⊢ I ∈ Fin ∧ d ⊆ I → 𝟙 I ⁡ d : I ⟶ 0 1
31 25 29 30 syl2anc ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d : I ⟶ 0 1
32 0nn0 ⊢ 0 ∈ ℕ 0
33 32 a1i ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 0 ∈ ℕ 0
34 1nn0 ⊢ 1 ∈ ℕ 0
35 34 a1i ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 1 ∈ ℕ 0
36 33 35 prssd ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 0 1 ⊆ ℕ 0
37 31 36 fssd ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d : I ⟶ ℕ 0
38 24 25 37 elmapdd ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d ∈ ℕ 0 I
39 31 25 33 fidmfisupp ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → finSupp 0 ⁡ 𝟙 I ⁡ d
40 22 38 39 elrabd ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h
41 40 1 eleqtrrdi ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d ∈ D
42 17 21 41 funimassd ⊢ φ → 𝟙 I c ∈ 𝒫 I | c = K ⊆ D
43 indf ⊢ D ∈ V ∧ 𝟙 I c ∈ 𝒫 I | c = K ⊆ D → 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K : D ⟶ 0 1
44 16 42 43 syl2anc ⊢ φ → 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K : D ⟶ 0 1
45 44 5 fvco3d ⊢ φ → ℤRHom ⁡ R ∘ 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K ⁡ F = ℤRHom ⁡ R ⁡ 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K ⁡ F
46 indfval ⊢ D ∈ V ∧ 𝟙 I c ∈ 𝒫 I | c = K ⊆ D ∧ F ∈ D → 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K ⁡ F = if F ∈ 𝟙 I c ∈ 𝒫 I | c = K 1 0
47 15 42 5 46 mp3an2i ⊢ φ → 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K ⁡ F = if F ∈ 𝟙 I c ∈ 𝒫 I | c = K 1 0
48 47 fveq2d ⊢ φ → ℤRHom ⁡ R ⁡ 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K ⁡ F = ℤRHom ⁡ R ⁡ if F ∈ 𝟙 I c ∈ 𝒫 I | c = K 1 0
49 fvif ⊢ ℤRHom ⁡ R ⁡ if F ∈ 𝟙 I c ∈ 𝒫 I | c = K 1 0 = if F ∈ 𝟙 I c ∈ 𝒫 I | c = K ℤRHom ⁡ R ⁡ 1 ℤRHom ⁡ R ⁡ 0
50 49 a1i ⊢ φ → ℤRHom ⁡ R ⁡ if F ∈ 𝟙 I c ∈ 𝒫 I | c = K 1 0 = if F ∈ 𝟙 I c ∈ 𝒫 I | c = K ℤRHom ⁡ R ⁡ 1 ℤRHom ⁡ R ⁡ 0
51 simpr ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K ∧ 𝟙 I ⁡ d = F → 𝟙 I ⁡ d = F
52 51 oveq1d ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K ∧ 𝟙 I ⁡ d = F → 𝟙 I ⁡ d supp 0 = F supp 0
53 indsupp ⊢ I ∈ Fin ∧ d ⊆ I → 𝟙 I ⁡ d supp 0 = d
54 25 29 53 syl2anc ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → 𝟙 I ⁡ d supp 0 = d
55 54 adantr ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K ∧ 𝟙 I ⁡ d = F → 𝟙 I ⁡ d supp 0 = d
56 52 55 eqtr3d ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K ∧ 𝟙 I ⁡ d = F → F supp 0 = d
57 56 fveq2d ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K ∧ 𝟙 I ⁡ d = F → F supp 0 = d
58 fveqeq2 ⊢ c = d → c = K ↔ d = K
59 simpr ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → d ∈ c ∈ 𝒫 I | c = K
60 58 59 elrabrd ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K → d = K
61 60 adantr ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K ∧ 𝟙 I ⁡ d = F → d = K
62 57 61 eqtrd ⊢ φ ∧ d ∈ c ∈ 𝒫 I | c = K ∧ 𝟙 I ⁡ d = F → F supp 0 = K
63 62 adantllr ⊢ φ ∧ F ∈ 𝟙 I c ∈ 𝒫 I | c = K ∧ d ∈ c ∈ 𝒫 I | c = K ∧ 𝟙 I ⁡ d = F → F supp 0 = K
64 20 ffnd ⊢ φ → 𝟙 I Fn 𝒫 I
65 64 27 fvelimabd ⊢ φ → F ∈ 𝟙 I c ∈ 𝒫 I | c = K ↔ ∃ d ∈ c ∈ 𝒫 I | c = K 𝟙 I ⁡ d = F
66 65 biimpa ⊢ φ ∧ F ∈ 𝟙 I c ∈ 𝒫 I | c = K → ∃ d ∈ c ∈ 𝒫 I | c = K 𝟙 I ⁡ d = F
67 63 66 r19.29a ⊢ φ ∧ F ∈ 𝟙 I c ∈ 𝒫 I | c = K → F supp 0 = K
68 fveqeq2 ⊢ d = F supp 0 → 𝟙 I ⁡ d = F ↔ 𝟙 I ⁡ F supp 0 = F
69 fveqeq2 ⊢ c = F supp 0 → c = K ↔ F supp 0 = K
70 2 adantr ⊢ φ ∧ F supp 0 = K → I ∈ Fin
71 suppssdm ⊢ F supp 0 ⊆ dom ⁡ F
72 23 a1i ⊢ φ → ℕ 0 ∈ V
73 14 5 sselid ⊢ φ → F ∈ ℕ 0 I
74 2 72 73 elmaprd ⊢ φ → F : I ⟶ ℕ 0
75 71 74 fssdm ⊢ φ → F supp 0 ⊆ I
76 75 adantr ⊢ φ ∧ F supp 0 = K → F supp 0 ⊆ I
77 70 76 sselpwd ⊢ φ ∧ F supp 0 = K → F supp 0 ∈ 𝒫 I
78 simpr ⊢ φ ∧ F supp 0 = K → F supp 0 = K
79 69 77 78 elrabd ⊢ φ ∧ F supp 0 = K → F supp 0 ∈ c ∈ 𝒫 I | c = K
80 74 ffnd ⊢ φ → F Fn I
81 df-f ⊢ F : I ⟶ 0 1 ↔ F Fn I ∧ ran ⁡ F ⊆ 0 1
82 80 8 81 sylanbrc ⊢ φ → F : I ⟶ 0 1
83 2 82 indfsid ⊢ φ → F = 𝟙 I ⁡ F supp 0
84 83 adantr ⊢ φ ∧ F supp 0 = K → F = 𝟙 I ⁡ F supp 0
85 84 eqcomd ⊢ φ ∧ F supp 0 = K → 𝟙 I ⁡ F supp 0 = F
86 68 79 85 rspcedvdw ⊢ φ ∧ F supp 0 = K → ∃ d ∈ c ∈ 𝒫 I | c = K 𝟙 I ⁡ d = F
87 65 biimpar ⊢ φ ∧ ∃ d ∈ c ∈ 𝒫 I | c = K 𝟙 I ⁡ d = F → F ∈ 𝟙 I c ∈ 𝒫 I | c = K
88 86 87 syldan ⊢ φ ∧ F supp 0 = K → F ∈ 𝟙 I c ∈ 𝒫 I | c = K
89 67 88 impbida ⊢ φ → F ∈ 𝟙 I c ∈ 𝒫 I | c = K ↔ F supp 0 = K
90 eqid ⊢ ℤRHom ⁡ R = ℤRHom ⁡ R
91 90 7 zrh1 ⊢ R ∈ Ring → ℤRHom ⁡ R ⁡ 1 = 1 ˙
92 3 91 syl ⊢ φ → ℤRHom ⁡ R ⁡ 1 = 1 ˙
93 90 6 zrh0 ⊢ R ∈ Ring → ℤRHom ⁡ R ⁡ 0 = 0 ˙
94 3 93 syl ⊢ φ → ℤRHom ⁡ R ⁡ 0 = 0 ˙
95 89 92 94 ifbieq12d ⊢ φ → if F ∈ 𝟙 I c ∈ 𝒫 I | c = K ℤRHom ⁡ R ⁡ 1 ℤRHom ⁡ R ⁡ 0 = if F supp 0 = K 1 ˙ 0 ˙
96 48 50 95 3eqtrd ⊢ φ → ℤRHom ⁡ R ⁡ 𝟙 D ⁡ 𝟙 I c ∈ 𝒫 I | c = K ⁡ F = if F supp 0 = K 1 ˙ 0 ˙
97 12 45 96 3eqtrd Could not format ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) ) : No typesetting found for |- ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) ) with typecode |-