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	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
	esplyfv.i	$⊢ φ \to I \in Fin$
	esplyfv.r	$⊢ φ \to R \in Ring$
	esplyfv.k	$⊢ φ \to K \in (0 \dots \|I\|)$
	esplyfv.f	$⊢ φ \to F \in D$
	esplyfv.0	$⊢ \underset{˙}{0} = 0_{R}$
	esplyfv.1	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	esplyfv	Could not format assertion : No typesetting found for \|- ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( ran F C_ { 0 , 1 } /\ ( # ` ( F supp 0 ) ) = K ) , .1. , .0. ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		esplyfv.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
2		esplyfv.i	$⊢ φ \to I \in Fin$
3		esplyfv.r	$⊢ φ \to R \in Ring$
4		esplyfv.k	$⊢ φ \to K \in (0 \dots \|I\|)$
5		esplyfv.f	$⊢ φ \to F \in D$
6		esplyfv.0	$⊢ \underset{˙}{0} = 0_{R}$
7		esplyfv.1	$⊢ \underset{˙}{1} = 1_{R}$
8		eqeq2	Could not format ( if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) -> ( ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) <-> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) ) ) : No typesetting found for \|- ( if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) -> ( ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) <-> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) ) ) with typecode \|-
9		eqeq2	Could not format ( .0. = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) -> ( ( ( ( I eSymPoly R ) ` K ) ` F ) = .0. <-> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) ) ) : No typesetting found for \|- ( .0. = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) -> ( ( ( ( I eSymPoly R ) ` K ) ` F ) = .0. <-> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) ) ) with typecode \|-
10	2	adantr	$⊢ (φ \land ran F \subseteq \{0, 1\}) \to I \in Fin$
11	3	adantr	$⊢ (φ \land ran F \subseteq \{0, 1\}) \to R \in Ring$
12	4	adantr	$⊢ (φ \land ran F \subseteq \{0, 1\}) \to K \in (0 \dots \|I\|)$
13	5	adantr	$⊢ (φ \land ran F \subseteq \{0, 1\}) \to F \in D$
14		simpr	$⊢ (φ \land ran F \subseteq \{0, 1\}) \to ran F \subseteq \{0, 1\}$
15	1 10 11 12 13 6 7 14	esplyfv1	Could not format ( ( ph /\ ran F C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) ) : No typesetting found for \|- ( ( ph /\ ran F C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) ) with typecode \|-
16	2	adantr	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to I \in Fin$
17	3	adantr	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to R \in Ring$
18		elfznn0	$⊢ K \in (0 \dots \|I\|) \to K \in ℕ_{0}$
19	4 18	syl	$⊢ φ \to K \in ℕ_{0}$
20	19	adantr	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to K \in ℕ_{0}$
21	1 16 17 20	esplyfval	Could not format ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) ) : No typesetting found for \|- ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) ) with typecode \|-
22	21	fveq1d	Could not format ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` F ) = ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) ` F ) ) : No typesetting found for \|- ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` F ) = ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) ` F ) ) with typecode \|-
23		ovex	$⊢ {ℕ_{0}}^{I} \in V$
24	1 23	rabex2	$⊢ D \in V$
25	24	a1i	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to D \in V$
26	1 16 17 20	esplylem	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D$
27		indf	$⊢ (D \in V \land 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ \{0, 1\}$
28	25 26 27	syl2anc	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ \{0, 1\}$
29	5	adantr	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to F \in D$
30	28 29	fvco3d	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to (ℤRHom (R) \circ 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}])) (F) = ℤRHom (R) (𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (F))$
31		simpr	$⊢ ((((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \land d \in \{c \in 𝒫 I \| \|c\| = K\}) \land 𝟙_{I} (d) = F) \to 𝟙_{I} (d) = F$
32	2	ad4antr	$⊢ ((((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \land d \in \{c \in 𝒫 I \| \|c\| = K\}) \land 𝟙_{I} (d) = F) \to I \in Fin$
33		ssrab2	$⊢ \{c \in 𝒫 I \| \|c\| = K\} \subseteq 𝒫 I$
34	33	a1i	$⊢ ((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \to \{c \in 𝒫 I \| \|c\| = K\} \subseteq 𝒫 I$
35	34	sselda	$⊢ (((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \land d \in \{c \in 𝒫 I \| \|c\| = K\}) \to d \in 𝒫 I$
36	35	adantr	$⊢ ((((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \land d \in \{c \in 𝒫 I \| \|c\| = K\}) \land 𝟙_{I} (d) = F) \to d \in 𝒫 I$
37	36	elpwid	$⊢ ((((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \land d \in \{c \in 𝒫 I \| \|c\| = K\}) \land 𝟙_{I} (d) = F) \to d \subseteq I$
38		indf	$⊢ (I \in Fin \land d \subseteq I) \to 𝟙_{I} (d) : I ⟶ \{0, 1\}$
39	32 37 38	syl2anc	$⊢ ((((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \land d \in \{c \in 𝒫 I \| \|c\| = K\}) \land 𝟙_{I} (d) = F) \to 𝟙_{I} (d) : I ⟶ \{0, 1\}$
40	31 39	feq1dd	$⊢ ((((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \land d \in \{c \in 𝒫 I \| \|c\| = K\}) \land 𝟙_{I} (d) = F) \to F : I ⟶ \{0, 1\}$
41	40	frnd	$⊢ ((((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \land d \in \{c \in 𝒫 I \| \|c\| = K\}) \land 𝟙_{I} (d) = F) \to ran F \subseteq \{0, 1\}$
42		indf1o	$⊢ I \in Fin \to 𝟙_{I} : 𝒫 I \underset{1-1 onto}{⟶} {\{0, 1\}}^{I}$
43		f1of	$⊢ 𝟙_{I} : 𝒫 I \underset{1-1 onto}{⟶} {\{0, 1\}}^{I} \to 𝟙_{I} : 𝒫 I ⟶ {\{0, 1\}}^{I}$
44	16 42 43	3syl	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to 𝟙_{I} : 𝒫 I ⟶ {\{0, 1\}}^{I}$
45	44	ffnd	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to 𝟙_{I} Fn 𝒫 I$
46	33	a1i	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to \{c \in 𝒫 I \| \|c\| = K\} \subseteq 𝒫 I$
47	45 46	fvelimabd	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to (F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \leftrightarrow \exists d \in \{c \in 𝒫 I \| \|c\| = K\} 𝟙_{I} (d) = F)$
48	47	biimpa	$⊢ ((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \to \exists d \in \{c \in 𝒫 I \| \|c\| = K\} 𝟙_{I} (d) = F$
49	41 48	r19.29a	$⊢ ((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \to ran F \subseteq \{0, 1\}$
50		simplr	$⊢ ((φ \land \neg ran F \subseteq \{0, 1\}) \land F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \to \neg ran F \subseteq \{0, 1\}$
51	49 50	pm2.65da	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to \neg F \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]$
52	29 51	eldifd	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to F \in (D ∖ 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}])$
53		ind0	$⊢ (D \in V \land 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D \land F \in (D ∖ 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}])) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (F) = 0$
54	24 26 52 53	mp3an2i	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (F) = 0$
55	54	fveq2d	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to ℤRHom (R) (𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (F)) = ℤRHom (R) (0)$
56		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
57	56 6	zrh0	$⊢ R \in Ring \to ℤRHom (R) (0) = \underset{˙}{0}$
58	3 57	syl	$⊢ φ \to ℤRHom (R) (0) = \underset{˙}{0}$
59	58	adantr	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to ℤRHom (R) (0) = \underset{˙}{0}$
60	55 59	eqtrd	$⊢ (φ \land \neg ran F \subseteq \{0, 1\}) \to ℤRHom (R) (𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (F)) = \underset{˙}{0}$
61	22 30 60	3eqtrd	Could not format ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` F ) = .0. ) : No typesetting found for \|- ( ( ph /\ -. ran F C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` F ) = .0. ) with typecode \|-
62	8 9 15 61	ifbothda	Could not format ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) ) : No typesetting found for \|- ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ran F C_ { 0 , 1 } , if ( ( # ` ( F supp 0 ) ) = K , .1. , .0. ) , .0. ) ) with typecode \|-
63		ifan	$⊢ if ((ran F \subseteq \{0, 1\} \land \|F supp 0\| = K), \underset{˙}{1}, \underset{˙}{0}) = if (ran F \subseteq \{0, 1\}, if (\|F supp 0\| = K, \underset{˙}{1}, \underset{˙}{0}), \underset{˙}{0})$
64	62 63	eqtr4di	Could not format ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( ran F C_ { 0 , 1 } /\ ( # ` ( F supp 0 ) ) = K ) , .1. , .0. ) ) : No typesetting found for \|- ( ph -> ( ( ( I eSymPoly R ) ` K ) ` F ) = if ( ( ran F C_ { 0 , 1 } /\ ( # ` ( F supp 0 ) ) = K ) , .1. , .0. ) ) with typecode \|-

Metamath Proof Explorer

Theorem esplyfv

Proof