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

Metamath Proof Explorer

Theorem esplyfval3

Description: Alternate expression for the value of the K -th elementary symmetric polynomial. (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses esplyfval3.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
esplyfval3.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplyfval3.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
esplyfval3.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
esplyfval3.1 ⊢ 0 = ( 0g ‘ 𝑅 )
esplyfval3.2 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion esplyfval3 ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 esplyfval3.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 esplyfval3.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
3 esplyfval3.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 esplyfval3.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
5 esplyfval3.1 ⊢ 0 = ( 0g ‘ 𝑅 )
6 esplyfval3.2 ⊢ 1 = ( 1r ‘ 𝑅 )
7 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
8 7 zrhrhm ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
9 zringbas ⊢ ℤ = ( Base ‘ ℤring )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 9 10 rhmf ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
12 3 8 11 3syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
13 12 ffnd ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) Fn ℤ )
14 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
15 1 14 rabex2 ⊢ 𝐷 ∈ V
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐷 ∈ V )
17 2 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐼 ∈ Fin )
18 3 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝑅 ∈ Ring )
19 4 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐾 ∈ ℕ0 )
20 1 17 18 19 esplylem ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )
21 indf ⊢ ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
22 16 20 21 syl2anc ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
23 0zd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 0 ∈ ℤ )
24 1zzd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 1 ∈ ℤ )
25 23 24 prssd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → { 0 , 1 } ⊆ ℤ )
26 22 25 fssd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ ℤ )
27 fnfco ⊢ ( ( ( ℤRHom ‘ 𝑅 ) Fn ℤ ∧ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ ℤ ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) Fn 𝐷 )
28 13 26 27 syl2an2r ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) Fn 𝐷 )
29 1 17 18 19 esplyfval ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )
30 29 fneq1d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) Fn 𝐷 ↔ ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) Fn 𝐷 ) )
31 28 30 mpbird ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) Fn 𝐷 )
32 dffn5 ⊢ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) Fn 𝐷 ↔ ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑓 ∈ 𝐷 ↦ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑓 ) ) )
33 31 32 sylib ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑓 ∈ 𝐷 ↦ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑓 ) ) )
34 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 ) ) )
35 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 ) ) )
36 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → 𝐼 ∈ Fin )
37 36 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝐼 ∈ Fin )
38 18 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑅 ∈ Ring )
39 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) )
40 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑓 ∈ 𝐷 )
41 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ran 𝑓 ⊆ { 0 , 1 } )
42 1 37 38 39 40 5 6 41 esplyfv1 ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑓 ) = if ( ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 , 1 , 0 ) )
43 29 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )
44 43 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑓 ) = ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) ‘ 𝑓 ) )
45 26 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ ℤ )
46 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑓 ∈ 𝐷 )
47 45 46 fvco3d ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) ‘ 𝑓 ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑓 ) ) )
48 20 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )
49 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝑓 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝑓 )
50 36 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝑓 ) → 𝐼 ∈ Fin )
51 ssrab2 ⊢ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼
52 51 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼 )
53 52 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) → 𝑑 ∈ 𝒫 𝐼 )
54 53 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝑓 ) → 𝑑 ∈ 𝒫 𝐼 )
55 54 elpwid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝑓 ) → 𝑑 ⊆ 𝐼 )
56 indf ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑑 ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ { 0 , 1 } )
57 50 55 56 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝑓 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) : 𝐼 ⟶ { 0 , 1 } )
58 49 57 feq1dd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ∧ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∧ ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝑓 ) → 𝑓 : 𝐼 ⟶ { 0 , 1 } )
59 indf1o ⊢ ( 𝐼 ∈ Fin → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) )
60 f1of ⊢ ( ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
61 36 59 60 3syl ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
62 61 ffnd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( 𝟭 ‘ 𝐼 ) Fn 𝒫 𝐼 )
63 51 a1i ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼 )
64 62 63 fvelimabd ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ↔ ∃ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝑓 ) )
65 64 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → ∃ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝑓 )
66 58 65 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → 𝑓 : 𝐼 ⟶ { 0 , 1 } )
67 66 frnd ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) → ran 𝑓 ⊆ { 0 , 1 } )
68 67 stoic1a ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ¬ 𝑓 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
69 46 68 eldifd ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → 𝑓 ∈ ( 𝐷 ∖ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) )
70 ind0 ⊢ ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ∧ 𝑓 ∈ ( 𝐷 ∖ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑓 ) = 0 )
71 15 48 69 70 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑓 ) = 0 )
72 71 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑓 ) ) = ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) )
73 7 5 zrh0 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = 0 )
74 3 73 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = 0 )
75 74 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = 0 )
76 72 75 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝑓 ) ) = 0 )
77 44 47 76 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) ∧ ¬ ran 𝑓 ⊆ { 0 , 1 } ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑓 ) = 0 )
78 34 35 42 77 ifbothda ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑓 ) = if ( ran 𝑓 ⊆ { 0 , 1 } , if ( ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 , 1 , 0 ) , 0 ) )
79 ifan ⊢ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) = if ( ran 𝑓 ⊆ { 0 , 1 } , if ( ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 , 1 , 0 ) , 0 )
80 78 79 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑓 ) = if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) )
81 80 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( 𝑓 ∈ 𝐷 ↦ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑓 ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) )
82 33 81 eqtrd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) )
83 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
84 1 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
85 eqid ⊢ ( 0g ‘ ( 𝐼 mPoly 𝑅 ) ) = ( 0g ‘ ( 𝐼 mPoly 𝑅 ) )
86 3 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
87 83 84 5 85 2 86 mpl0 ⊢ ( 𝜑 → ( 0g ‘ ( 𝐼 mPoly 𝑅 ) ) = ( 𝐷 × { 0 } ) )
88 87 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( 0g ‘ ( 𝐼 mPoly 𝑅 ) ) = ( 𝐷 × { 0 } ) )
89 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐼 ∈ Fin )
90 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝑅 ∈ Ring )
91 4 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐾 ∈ ℕ0 )
92 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) )
93 91 92 eldifd ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐾 ∈ ( ℕ0 ∖ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) )
94 1 89 90 93 85 esplyfval2 ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 0g ‘ ( 𝐼 mPoly 𝑅 ) ) )
95 breq1 ⊢ ( ℎ = 𝑓 → ( ℎ finSupp 0 ↔ 𝑓 finSupp 0 ) )
96 1 eleq2i ⊢ ( 𝑓 ∈ 𝐷 ↔ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
97 96 biimpi ⊢ ( 𝑓 ∈ 𝐷 → 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
98 97 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
99 95 98 elrabrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 finSupp 0 )
100 99 fsuppimpd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 supp 0 ) ∈ Fin )
101 hashcl ⊢ ( ( 𝑓 supp 0 ) ∈ Fin → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℕ0 )
102 100 101 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℕ0 )
103 102 nn0red ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℝ )
104 103 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℝ )
105 hashcl ⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
106 2 105 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
107 106 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℝ )
108 107 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ 𝐼 ) ∈ ℝ )
109 4 nn0red ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
110 109 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → 𝐾 ∈ ℝ )
111 suppssdm ⊢ ( 𝑓 supp 0 ) ⊆ dom 𝑓
112 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝐼 ∈ Fin )
113 nn0ex ⊢ ℕ0 ∈ V
114 113 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ℕ0 ∈ V )
115 1 ssrab3 ⊢ 𝐷 ⊆ ( ℕ0 ↑m 𝐼 )
116 115 a1i ⊢ ( 𝜑 → 𝐷 ⊆ ( ℕ0 ↑m 𝐼 ) )
117 116 sselda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) )
118 112 114 117 elmaprd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 : 𝐼 ⟶ ℕ0 )
119 111 118 fssdm ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 supp 0 ) ⊆ 𝐼 )
120 hashss ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑓 supp 0 ) ⊆ 𝐼 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ≤ ( ♯ ‘ 𝐼 ) )
121 2 119 120 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ≤ ( ♯ ‘ 𝐼 ) )
122 121 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ≤ ( ♯ ‘ 𝐼 ) )
123 106 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℤ )
124 123 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ 𝐼 ) ∈ ℤ )
125 nn0diffz0 ⊢ ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 → ( ℕ0 ∖ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) = ( ℤ≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
126 89 105 125 3syl ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ℕ0 ∖ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) = ( ℤ≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
127 93 126 eleqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐾 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
128 127 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → 𝐾 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
129 eluzp1l ⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℤ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) ) → ( ♯ ‘ 𝐼 ) < 𝐾 )
130 124 128 129 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ 𝐼 ) < 𝐾 )
131 104 108 110 122 130 lelttrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) < 𝐾 )
132 104 131 ltned ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ≠ 𝐾 )
133 132 neneqd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 )
134 133 intnand ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ¬ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) )
135 134 iffalsed ⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) = 0 )
136 135 mpteq2dva ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) = ( 𝑓 ∈ 𝐷 ↦ 0 ) )
137 fconstmpt ⊢ ( 𝐷 × { 0 } ) = ( 𝑓 ∈ 𝐷 ↦ 0 )
138 136 137 eqtr4di ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) = ( 𝐷 × { 0 } ) )
139 88 94 138 3eqtr4d ⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) )
140 82 139 pm2.61dan ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) )