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	23	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
73	14 5	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) )
74	2 72 73	elmaprd	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ℕ0 )
75	71 74	fssdm	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐼 )
76	75	adantr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ( 𝐹 supp 0 ) ⊆ 𝐼 )
77	70 76	sselpwd	⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ( 𝐹 supp 0 ) ∈ 𝒫 𝐼 )
78		simpr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 )
79	69 77 78	elrabd	⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ( 𝐹 supp 0 ) ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } )
80	74	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐼 )
81		df-f	⊢ ( 𝐹 : 𝐼 ⟶ { 0 , 1 } ↔ ( 𝐹 Fn 𝐼 ∧ ran 𝐹 ⊆ { 0 , 1 } ) )
82	80 8 81	sylanbrc	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ { 0 , 1 } )
83	2 82	indfsid	⊢ ( 𝜑 → 𝐹 = ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐹 supp 0 ) ) )
84	83	adantr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → 𝐹 = ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐹 supp 0 ) ) )
85	84	eqcomd	⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ ( 𝐹 supp 0 ) ) = 𝐹 )
86	68 79 85	rspcedvdw	⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → ∃ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 )
87	65	biimpar	⊢ ( ( 𝜑 ∧ ∃ 𝑑 ∈ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ( ( 𝟭 ‘ 𝐼 ) ‘ 𝑑 ) = 𝐹 ) → 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
88	86 87	syldan	⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) → 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
89	67 88	impbida	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ↔ ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 ) )
90		eqid	⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
91	90 7	zrh1	⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = 1 )
92	3 91	syl	⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = 1 )
93	90 6	zrh0	⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = 0 )
94	3 93	syl	⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = 0 )
95	89 92 94	ifbieq12d	⊢ ( 𝜑 → if ( 𝐹 ∈ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) , ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) ) = if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) )
96	48 50 95	3eqtrd	⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ‘ 𝐹 ) ) = if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) )
97	12 45 96	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝐹 ) = if ( ( ♯ ‘ ( 𝐹 supp 0 ) ) = 𝐾 , 1 , 0 ) )