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	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 }
	esplyfval3.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	esplyfval3.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	esplyfval3.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ₀ )
	esplyfval3.1	⊢ 0 = ( 0_g ‘ 𝑅 )
	esplyfval3.2	⊢ 1 = ( 1_r ‘ 𝑅 )
Assertion	esplyfval3	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		esplyfval3.d	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 }
2		esplyfval3.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
3		esplyfval3.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		esplyfval3.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ₀ )
5		esplyfval3.1	⊢ 0 = ( 0_g ‘ 𝑅 )
6		esplyfval3.2	⊢ 1 = ( 1_r ‘ 𝑅 )
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	⊢ ( ℕ₀ ↑_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 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐾 ∈ ℕ₀ )
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	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
85		eqid	⊢ ( 0_g ‘ ( 𝐼 mPoly 𝑅 ) ) = ( 0_g ‘ ( 𝐼 mPoly 𝑅 ) )
86	3	ringgrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
87	83 84 5 85 2 86	mpl0	⊢ ( 𝜑 → ( 0_g ‘ ( 𝐼 mPoly 𝑅 ) ) = ( 𝐷 × { 0 } ) )
88	87	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( 0_g ‘ ( 𝐼 mPoly 𝑅 ) ) = ( 𝐷 × { 0 } ) )
89	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐼 ∈ Fin )
90	3	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝑅 ∈ Ring )
91	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐾 ∈ ℕ₀ )
92		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) )
93	91 92	eldifd	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐾 ∈ ( ℕ₀ ∖ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) )
94	1 89 90 93 85	esplyfval2	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 0_g ‘ ( 𝐼 mPoly 𝑅 ) ) )
95		breq1	⊢ ( ℎ = 𝑓 → ( ℎ finSupp 0 ↔ 𝑓 finSupp 0 ) )
96	1	eleq2i	⊢ ( 𝑓 ∈ 𝐷 ↔ 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
97	96	biimpi	⊢ ( 𝑓 ∈ 𝐷 → 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
98	97	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
99	95 98	elrabrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 finSupp 0 )
100	99	fsuppimpd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 supp 0 ) ∈ Fin )
101		hashcl	⊢ ( ( 𝑓 supp 0 ) ∈ Fin → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℕ₀ )
102	100 101	syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℕ₀ )
103	102	nn0red	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℝ )
104	103	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℝ )
105		hashcl	⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ₀ )
106	2 105	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ₀ )
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	⊢ ℕ₀ ∈ V
114	113	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ℕ₀ ∈ V )
115	1	ssrab3	⊢ 𝐷 ⊆ ( ℕ₀ ↑_m 𝐼 )
116	115	a1i	⊢ ( 𝜑 → 𝐷 ⊆ ( ℕ₀ ↑_m 𝐼 ) )
117	116	sselda	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) )
118	112 114 117	elmaprd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 : 𝐼 ⟶ ℕ₀ )
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 ... ( ♯ ‘ 𝐼 ) ) ) = ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
126	89 105 125	3syl	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 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 ) ) )

Metamath Proof Explorer

Theorem esplyfval3

Proof