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 ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
esplyfv.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplyfv.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
esplyfv.k ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) )
esplyfv.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
esplyfv.0 ⊢ 0 = ( 0g ‘ 𝑅 )
esplyfv.1 ⊢ 1 = ( 1r ‘ 𝑅 )
esplyfv1.1 ⊢ ( 𝜑 → ran 𝐹 ⊆ { 0 , 1 } )
Assertion esplyfv1 ( 𝜑 → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 esplyfv.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 esplyfv.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
3 esplyfv.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 esplyfv.k ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) )
5 esplyfv.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
6 esplyfv.0 ⊢ 0 = ( 0g ‘ 𝑅 )
7 esplyfv.1 ⊢ 1 = ( 1r ‘ 𝑅 )
8 esplyfv1.1 ⊢ ( 𝜑 → ran 𝐹 ⊆ { 0 , 1 } )
9 elfznn0 ⊢ ( 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) → 𝐾 ∈ ℕ0 )
10 4 9 syl ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
11 1 2 3 10 esplyfval ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )
12 11 fveq1d ⊢ ( 𝜑 → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) ‘ 𝐹 ) )
13 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
14 1 ssrab3 ⊢ 𝐷 ⊆ ( ℕ0 ↑m 𝐼 )
15 13 14 ssexi ⊢ 𝐷 ∈ V
16 15 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
17 nfv ⊢ Ⅎ 𝑑 𝜑
18 indf1o ⊢ ( 𝐼 ∈ Fin → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) )
19 f1of ⊢ ( ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
20 2 18 19 3syl ⊢ ( 𝜑 → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
21 20 ffund ⊢ ( 𝜑 → Fun ( 𝟭 ‘ 𝐼 ) )
22 breq1 ⊢ ( ℎ = ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) → ( ℎ finSupp 0 ↔ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) finSupp 0 ) )
23 nn0ex ⊢ ℕ0 ∈ V
24 23 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ℕ0 ∈ V )
25 2 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝐼 ∈ Fin )
26 ssrab2 ⊢ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼
27 26 a1i ⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼 )
28 27 sselda ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑑 ∈ 𝒫 𝐼 )
29 28 elpwid ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑑 ⊆ 𝐼 )
30 indf ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑑 ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ { 0 , 1 } )
31 25 29 30 syl2anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ { 0 , 1 } )
32 0nn0 ⊢ 0 ∈ ℕ0
33 32 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 0 ∈ ℕ0 )
34 1nn0 ⊢ 1 ∈ ℕ0
35 34 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 1 ∈ ℕ0 )
36 33 35 prssd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → { 0 , 1 } ⊆ ℕ0 )
37 31 36 fssd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ ℕ0 )
38 24 25 37 elmapdd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) ∈ ( ℕ0 ↑m 𝐼 ) )
39 31 25 33 fidmfisupp ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) finSupp 0 )
40 22 38 39 elrabd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
41 40 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) ∈ 𝐷 )
42 17 21 41 funimassd ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )
43 indf ⊢ ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
44 16 42 43 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
45 44 5 fvco3d ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) ‘ 𝐹 ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) ) )
46 indfval ⊢ ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ∧ 𝐹 ∈ 𝐷 ) → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) = if ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) , 1 , 0 ) )
47 15 42 5 46 mp3an2i ⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) = if ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) , 1 , 0 ) )
48 47 fveq2d ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) ) = ( ( ℤRHom ‘ 𝑅 ) ‘ if ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) , 1 , 0 ) ) )
49 fvif ⊢ ( ( ℤRHom ‘ 𝑅 ) ‘ if ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) , 1 , 0 ) ) = if ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) )
50 49 a1i ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ if ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) , 1 , 0 ) ) = if ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) ) )
51 simpr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 )
52 51 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) supp 0 ) = ( 𝐹 supp 0 ) )
53 indsupp ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑑 ⊆ 𝐼 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) supp 0 ) = 𝑑 )
54 25 29 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) supp 0 ) = 𝑑 )
55 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) supp 0 ) = 𝑑 )
56 52 55 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ( 𝐹 supp 0 ) = 𝑑 )
57 56 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) = ( ♯ ‘ 𝑑 ) )
58 fveqeq2 ⊢ ( 𝑐 = 𝑑 → ( ( ♯ ‘ 𝑐 ) = 𝐾 ↔ ( ♯ ‘ 𝑑 ) = 𝐾 ) )
59 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } )
60 58 59 elrabrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → ( ♯ ‘ 𝑑 ) = 𝐾 )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ( ♯ ‘ 𝑑 ) = 𝐾 )
62 57 61 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 )
63 62 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 )
64 20 ffnd ⊢ ( 𝜑 → ( 𝟭 ‘ 𝐼 ) Fn 𝒫 𝐼 )
65 64 27 fvelimabd ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ↔ ∃ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) )
66 65 biimpa ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → ∃ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 )
67 63 66 r19.29a ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 )
68 fveqeq2 ⊢ ( 𝑑 = ( 𝐹 supp 0 ) → ( ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ↔ ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐹 supp 0 ) ) = 𝐹 ) )
69 fveqeq2 ⊢ ( 𝑐 = ( 𝐹 supp 0 ) → ( ( ♯ ‘ 𝑐 ) = 𝐾 ↔ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) )
70 2 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → 𝐼 ∈ Fin )
71 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
72 14 5 sselid ⊢ ( 𝜑 → 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) )
73 72 elmaprd ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ℕ0 )
74 71 73 fssdm ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐼 )
75 74 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ( 𝐹 supp 0 ) ⊆ 𝐼 )
76 70 75 sselpwd ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ( 𝐹 supp 0 ) ∈ 𝒫 𝐼 )
77 simpr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 )
78 69 76 77 elrabd ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ( 𝐹 supp 0 ) ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } )
79 73 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐼 )
80 df-f ⊢ ( 𝐹 : 𝐼 ⟶ { 0 , 1 } ↔ ( 𝐹 Fn 𝐼 ∧ ran 𝐹 ⊆ { 0 , 1 } ) )
81 79 8 80 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ { 0 , 1 } )
82 2 81 indfsid ⊢ ( 𝜑 → 𝐹 = ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐹 supp 0 ) ) )
83 82 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → 𝐹 = ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐹 supp 0 ) ) )
84 83 eqcomd ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐹 supp 0 ) ) = 𝐹 )
85 68 78 84 rspcedvdw ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ∃ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 )
86 65 biimpar ⊢ ( ( 𝜑 ∧ ∃ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
87 85 86 syldan ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
88 67 87 impbida ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ↔ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) )
89 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
90 89 7 zrh1 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = 1 )
91 3 90 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = 1 )
92 89 6 zrh0 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = 0 )
93 3 92 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = 0 )
94 88 91 93 ifbieq12d ⊢ ( 𝜑 → if ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) ) = if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) )
95 48 50 94 3eqtrd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) ) = if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) )
96 12 45 95 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) )