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	bilani	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
98	95 97	elrabrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 finSupp 0 )
99	98	fsuppimpd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 supp 0 ) ∈ Fin )
100		hashcl	⊢ ( ( 𝑓 supp 0 ) ∈ Fin → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℕ₀ )
101	99 100	syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℕ₀ )
102	101	nn0red	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℝ )
103	102	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ∈ ℝ )
104		hashcl	⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ₀ )
105	2 104	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ₀ )
106	105	nn0red	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℝ )
107	106	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ 𝐼 ) ∈ ℝ )
108	4	nn0red	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
109	108	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → 𝐾 ∈ ℝ )
110		suppssdm	⊢ ( 𝑓 supp 0 ) ⊆ dom 𝑓
111	1	ssrab3	⊢ 𝐷 ⊆ ( ℕ₀ ↑_m 𝐼 )
112	111	a1i	⊢ ( 𝜑 → 𝐷 ⊆ ( ℕ₀ ↑_m 𝐼 ) )
113	112	sselda	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) )
114	113	elmaprd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → 𝑓 : 𝐼 ⟶ ℕ₀ )
115	110 114	fssdm	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( 𝑓 supp 0 ) ⊆ 𝐼 )
116		hashss	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑓 supp 0 ) ⊆ 𝐼 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ≤ ( ♯ ‘ 𝐼 ) )
117	2 115 116	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ≤ ( ♯ ‘ 𝐼 ) )
118	117	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ≤ ( ♯ ‘ 𝐼 ) )
119	105	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℤ )
120	119	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ 𝐼 ) ∈ ℤ )
121		nn0diffz0	⊢ ( ( ♯ ‘ 𝐼 ) ∈ ℕ₀ → ( ℕ₀ ∖ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) = ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
122	89 104 121	3syl	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ℕ₀ ∖ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) = ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
123	93 122	eleqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → 𝐾 ∈ ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
124	123	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → 𝐾 ∈ ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) )
125		eluzp1l	⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℤ ∧ 𝐾 ∈ ( ℤ_≥ ‘ ( ( ♯ ‘ 𝐼 ) + 1 ) ) ) → ( ♯ ‘ 𝐼 ) < 𝐾 )
126	120 124 125	syl2anc	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ 𝐼 ) < 𝐾 )
127	103 107 109 118 126	lelttrd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) < 𝐾 )
128	103 127	ltned	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑓 supp 0 ) ) ≠ 𝐾 )
129	128	neneqd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ¬ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 )
130	129	intnand	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → ¬ ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) )
131	130	iffalsed	⊢ ( ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝐷 ) → if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) = 0 )
132	131	mpteq2dva	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) = ( 𝑓 ∈ 𝐷 ↦ 0 ) )
133		fconstmpt	⊢ ( 𝐷 × { 0 } ) = ( 𝑓 ∈ 𝐷 ↦ 0 )
134	132 133	eqtr4di	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) = ( 𝐷 × { 0 } ) )
135	88 94 134	3eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) ) → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) )
136	82 135	pm2.61dan	⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( 𝑓 ∈ 𝐷 ↦ if ( ( ran 𝑓 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑓 supp 0 ) ) = 𝐾 ) , 1 , 0 ) ) )

Metamath Proof Explorer

Theorem esplyfval3

Proof