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

Metamath Proof Explorer

Theorem esplyfv

Description: Coefficient for the K -th elementary symmetric polynomial and a bag of variables F : the coefficient is .1. for the bags of exactly K variables, having exponent at most 1 . (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 ‘ 𝑅 )
Assertion esplyfv ( 𝜑 → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = if ( ( ran 𝐹 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝐹 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 eqeq2 ⊢ ( if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) = if ( ran 𝐹 ⊆ { 0 , 1 } , if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) , 0 ) → ( ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) ↔ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = if ( ran 𝐹 ⊆ { 0 , 1 } , if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) , 0 ) ) )
9 eqeq2 ⊢ ( 0 = if ( ran 𝐹 ⊆ { 0 , 1 } , if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) , 0 ) → ( ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = 0 ↔ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = if ( ran 𝐹 ⊆ { 0 , 1 } , if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) , 0 ) ) )
10 2 adantr ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 , 1 } ) → 𝐼 ∈ Fin )
11 3 adantr ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 , 1 } ) → 𝑅 ∈ Ring )
12 4 adantr ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 , 1 } ) → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) )
13 5 adantr ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 , 1 } ) → 𝐹 ∈ 𝐷 )
14 simpr ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 , 1 } ) → ran 𝐹 ⊆ { 0 , 1 } )
15 1 10 11 12 13 6 7 14 esplyfv1 ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) )
16 2 adantr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → 𝐼 ∈ Fin )
17 3 adantr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → 𝑅 ∈ Ring )
18 elfznn0 ⊢ ( 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) → 𝐾 ∈ ℕ0 )
19 4 18 syl ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
20 19 adantr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → 𝐾 ∈ ℕ0 )
21 1 16 17 20 esplyfval ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )
22 21 fveq1d ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) ‘ 𝐹 ) )
23 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
24 1 23 rabex2 ⊢ 𝐷 ∈ V
25 24 a1i ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → 𝐷 ∈ V )
26 1 16 17 20 esplylem ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )
27 indf ⊢ ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
28 25 26 27 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
29 5 adantr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → 𝐹 ∈ 𝐷 )
30 28 29 fvco3d ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) ‘ 𝐹 ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) ) )
31 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 )
32 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → 𝐼 ∈ Fin )
33 ssrab2 ⊢ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼
34 33 a1i ⊢ ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼 )
35 34 sselda ⊢ ( ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑑 ∈ 𝒫 𝐼 )
36 35 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → 𝑑 ∈ 𝒫 𝐼 )
37 36 elpwid ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → 𝑑 ⊆ 𝐼 )
38 indf ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑑 ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ { 0 , 1 } )
39 32 37 38 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ { 0 , 1 } )
40 31 39 feq1dd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → 𝐹 : 𝐼 ⟶ { 0 , 1 } )
41 40 frnd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → ran 𝐹 ⊆ { 0 , 1 } )
42 indf1o ⊢ ( 𝐼 ∈ Fin → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) )
43 f1of ⊢ ( ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
44 16 42 43 3syl ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
45 44 ffnd ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( 𝟭 ‘ 𝐼 ) Fn 𝒫 𝐼 )
46 33 a1i ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼 )
47 45 46 fvelimabd ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ↔ ∃ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) )
48 47 biimpa ⊢ ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → ∃ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 )
49 41 48 r19.29a ⊢ ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → ran 𝐹 ⊆ { 0 , 1 } )
50 simplr ⊢ ( ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) ∧ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → ¬ ran 𝐹 ⊆ { 0 , 1 } )
51 49 50 pm2.65da ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ¬ 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
52 29 51 eldifd ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → 𝐹 ∈ ( 𝐷 ∖ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) )
53 ind0 ⊢ ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ∧ 𝐹 ∈ ( 𝐷 ∖ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) = 0 )
54 24 26 52 53 mp3an2i ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) = 0 )
55 54 fveq2d ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) ) = ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) )
56 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
57 56 6 zrh0 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = 0 )
58 3 57 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = 0 )
59 58 adantr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = 0 )
60 55 59 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) ) = 0 )
61 22 30 60 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ⊆ { 0 , 1 } ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = 0 )
62 8 9 15 61 ifbothda ⊢ ( 𝜑 → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = if ( ran 𝐹 ⊆ { 0 , 1 } , if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) , 0 ) )
63 ifan ⊢ if ( ( ran 𝐹 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) , 1 , 0 ) = if ( ran 𝐹 ⊆ { 0 , 1 } , if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) , 0 )
64 62 63 eqtr4di ⊢ ( 𝜑 → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = if ( ( ran 𝐹 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) , 1 , 0 ) )