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

Proof

Step	Hyp	Ref	Expression
1		esplyfval3.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
2		esplyfval3.i	$⊢ φ \to I \in Fin$
3		esplyfval3.r	$⊢ φ \to R \in Ring$
4		esplyfval3.k	$⊢ φ \to K \in ℕ_{0}$
5		esplyfval3.1	$⊢ \underset{˙}{0} = 0_{R}$
6		esplyfval3.2	$⊢ \underset{˙}{1} = 1_{R}$
7		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
8	7	zrhrhm	$⊢ R \in Ring \to ℤRHom (R) \in (ℤ_{ring} RingHom R)$
9		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11	9 10	rhmf	$⊢ ℤRHom (R) \in (ℤ_{ring} RingHom R) \to ℤRHom (R) : ℤ ⟶ {Base}_{R}$
12	3 8 11	3syl	$⊢ φ \to ℤRHom (R) : ℤ ⟶ {Base}_{R}$
13	12	ffnd	$⊢ φ \to ℤRHom (R) Fn ℤ$
14		ovex	$⊢ {ℕ_{0}}^{I} \in V$
15	1 14	rabex2	$⊢ D \in V$
16	15	a1i	$⊢ (φ \land K \in (0 \dots \|I\|)) \to D \in V$
17	2	adantr	$⊢ (φ \land K \in (0 \dots \|I\|)) \to I \in Fin$
18	3	adantr	$⊢ (φ \land K \in (0 \dots \|I\|)) \to R \in Ring$
19	4	adantr	$⊢ (φ \land K \in (0 \dots \|I\|)) \to K \in ℕ_{0}$
20	1 17 18 19	esplylem	$⊢ (φ \land K \in (0 \dots \|I\|)) \to 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D$
21		indf	$⊢ (D \in V \land 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ \{0, 1\}$
22	16 20 21	syl2anc	$⊢ (φ \land K \in (0 \dots \|I\|)) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ \{0, 1\}$
23		0zd	$⊢ (φ \land K \in (0 \dots \|I\|)) \to 0 \in ℤ$
24		1zzd	$⊢ (φ \land K \in (0 \dots \|I\|)) \to 1 \in ℤ$
25	23 24	prssd	$⊢ (φ \land K \in (0 \dots \|I\|)) \to \{0, 1\} \subseteq ℤ$
26	22 25	fssd	$⊢ (φ \land K \in (0 \dots \|I\|)) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ ℤ$
27		fnfco	$⊢ (ℤRHom (R) Fn ℤ \land 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ ℤ) \to (ℤRHom (R) \circ 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}])) Fn D$
28	13 26 27	syl2an2r	$⊢ (φ \land K \in (0 \dots \|I\|)) \to (ℤRHom (R) \circ 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}])) Fn D$
29	1 17 18 19	esplyfval	Could not format ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) ) : No typesetting found for \|- ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) ) with typecode \|-
30	29	fneq1d	Could not format ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( ( I eSymPoly R ) ` K ) Fn D <-> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) Fn D ) ) : No typesetting found for \|- ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( ( I eSymPoly R ) ` K ) Fn D <-> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) Fn D ) ) with typecode \|-
31	28 30	mpbird	Could not format ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) Fn D ) : No typesetting found for \|- ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) Fn D ) with typecode \|-
32		dffn5	Could not format ( ( ( I eSymPoly R ) ` K ) Fn D <-> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> ( ( ( I eSymPoly R ) ` K ) ` f ) ) ) : No typesetting found for \|- ( ( ( I eSymPoly R ) ` K ) Fn D <-> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> ( ( ( I eSymPoly R ) ` K ) ` f ) ) ) with typecode \|-
33	31 32	sylib	Could not format ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> ( ( ( I eSymPoly R ) ` K ) ` f ) ) ) : No typesetting found for \|- ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> ( ( ( I eSymPoly R ) ` K ) ` f ) ) ) with typecode \|-
34		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 \|-
35		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 \|-
36	17	adantr	$⊢ ((φ \land K \in (0 \dots \|I\|)) \land f \in D) \to I \in Fin$
37	36	adantr	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land ran f \subseteq \{0, 1\}) \to I \in Fin$
38	18	ad2antrr	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land ran f \subseteq \{0, 1\}) \to R \in Ring$
39		simpllr	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land ran f \subseteq \{0, 1\}) \to K \in (0 \dots \|I\|)$
40		simplr	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land ran f \subseteq \{0, 1\}) \to f \in D$
41		simpr	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land ran f \subseteq \{0, 1\}) \to ran f \subseteq \{0, 1\}$
42	1 37 38 39 40 5 6 41	esplyfv1	Could not format ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ ran f C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) ) : No typesetting found for \|- ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ ran f C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) ) with typecode \|-
43	29	ad2antrr	Could not format ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. 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 /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) ) with typecode \|-
44	43	fveq1d	Could not format ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. 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 /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. 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 \|-
45	26	ad2antrr	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land \neg ran f \subseteq \{0, 1\}) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ ℤ$
46		simplr	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land \neg ran f \subseteq \{0, 1\}) \to f \in D$
47	45 46	fvco3d	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \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))$
48	20	ad2antrr	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land \neg ran f \subseteq \{0, 1\}) \to 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D$
49		simpr	$⊢ (((((φ \land K \in (0 \dots \|I\|)) \land f \in D) \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$
50	36	ad3antrrr	$⊢ (((((φ \land K \in (0 \dots \|I\|)) \land f \in D) \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$
51		ssrab2	$⊢ \{c \in 𝒫 I \| \|c\| = K\} \subseteq 𝒫 I$
52	51	a1i	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land f \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \to \{c \in 𝒫 I \| \|c\| = K\} \subseteq 𝒫 I$
53	52	sselda	$⊢ ((((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land f \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \land d \in \{c \in 𝒫 I \| \|c\| = K\}) \to d \in 𝒫 I$
54	53	adantr	$⊢ (((((φ \land K \in (0 \dots \|I\|)) \land f \in D) \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$
55	54	elpwid	$⊢ (((((φ \land K \in (0 \dots \|I\|)) \land f \in D) \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$
56		indf	$⊢ (I \in Fin \land d \subseteq I) \to 𝟙_{I} (d) : I ⟶ \{0, 1\}$
57	50 55 56	syl2anc	$⊢ (((((φ \land K \in (0 \dots \|I\|)) \land f \in D) \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\}$
58	49 57	feq1dd	$⊢ (((((φ \land K \in (0 \dots \|I\|)) \land f \in D) \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\}$
59		indf1o	$⊢ I \in Fin \to 𝟙_{I} : 𝒫 I \underset{1-1 onto}{⟶} {\{0, 1\}}^{I}$
60		f1of	$⊢ 𝟙_{I} : 𝒫 I \underset{1-1 onto}{⟶} {\{0, 1\}}^{I} \to 𝟙_{I} : 𝒫 I ⟶ {\{0, 1\}}^{I}$
61	36 59 60	3syl	$⊢ ((φ \land K \in (0 \dots \|I\|)) \land f \in D) \to 𝟙_{I} : 𝒫 I ⟶ {\{0, 1\}}^{I}$
62	61	ffnd	$⊢ ((φ \land K \in (0 \dots \|I\|)) \land f \in D) \to 𝟙_{I} Fn 𝒫 I$
63	51	a1i	$⊢ ((φ \land K \in (0 \dots \|I\|)) \land f \in D) \to \{c \in 𝒫 I \| \|c\| = K\} \subseteq 𝒫 I$
64	62 63	fvelimabd	$⊢ ((φ \land K \in (0 \dots \|I\|)) \land f \in D) \to (f \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \leftrightarrow \exists d \in \{c \in 𝒫 I \| \|c\| = K\} 𝟙_{I} (d) = f)$
65	64	biimpa	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land f \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \to \exists d \in \{c \in 𝒫 I \| \|c\| = K\} 𝟙_{I} (d) = f$
66	58 65	r19.29a	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land f \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \to f : I ⟶ \{0, 1\}$
67	66	frnd	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land f \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) \to ran f \subseteq \{0, 1\}$
68	67	stoic1a	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land \neg ran f \subseteq \{0, 1\}) \to \neg f \in 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]$
69	46 68	eldifd	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land \neg ran f \subseteq \{0, 1\}) \to f \in (D ∖ 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}])$
70		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$
71	15 48 69 70	mp3an2i	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land \neg ran f \subseteq \{0, 1\}) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (f) = 0$
72	71	fveq2d	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land \neg ran f \subseteq \{0, 1\}) \to ℤRHom (R) (𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (f)) = ℤRHom (R) (0)$
73	7 5	zrh0	$⊢ R \in Ring \to ℤRHom (R) (0) = \underset{˙}{0}$
74	3 73	syl	$⊢ φ \to ℤRHom (R) (0) = \underset{˙}{0}$
75	74	ad3antrrr	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land \neg ran f \subseteq \{0, 1\}) \to ℤRHom (R) (0) = \underset{˙}{0}$
76	72 75	eqtrd	$⊢ (((φ \land K \in (0 \dots \|I\|)) \land f \in D) \land \neg ran f \subseteq \{0, 1\}) \to ℤRHom (R) (𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) (f)) = \underset{˙}{0}$
77	44 47 76	3eqtrd	Could not format ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = .0. ) : No typesetting found for \|- ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = .0. ) with typecode \|-
78	34 35 42 77	ifbothda	Could not format ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ran f C_ { 0 , 1 } , if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) , .0. ) ) : No typesetting found for \|- ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ran f C_ { 0 , 1 } , if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) , .0. ) ) with typecode \|-
79		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})$
80	78 79	eqtr4di	Could not format ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) : No typesetting found for \|- ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) with typecode \|-
81	80	mpteq2dva	Could not format ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( f e. D \|-> ( ( ( I eSymPoly R ) ` K ) ` f ) ) = ( f e. D \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) ) : No typesetting found for \|- ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( f e. D \|-> ( ( ( I eSymPoly R ) ` K ) ` f ) ) = ( f e. D \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) ) with typecode \|-
82	33 81	eqtrd	Could not format ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) ) : No typesetting found for \|- ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) ) with typecode \|-
83		eqid	$⊢ I mPoly R = I mPoly R$
84	1	psrbasfsupp	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
85		eqid	$⊢ 0_{(I mPoly R)} = 0_{(I mPoly R)}$
86	3	ringgrpd	$⊢ φ \to R \in Grp$
87	83 84 5 85 2 86	mpl0	$⊢ φ \to 0_{(I mPoly R)} = D \times \{\underset{˙}{0}\}$
88	87	adantr	$⊢ (φ \land \neg K \in (0 \dots \|I\|)) \to 0_{(I mPoly R)} = D \times \{\underset{˙}{0}\}$
89	2	adantr	$⊢ (φ \land \neg K \in (0 \dots \|I\|)) \to I \in Fin$
90	3	adantr	$⊢ (φ \land \neg K \in (0 \dots \|I\|)) \to R \in Ring$
91	4	adantr	$⊢ (φ \land \neg K \in (0 \dots \|I\|)) \to K \in ℕ_{0}$
92		simpr	$⊢ (φ \land \neg K \in (0 \dots \|I\|)) \to \neg K \in (0 \dots \|I\|)$
93	91 92	eldifd	$⊢ (φ \land \neg K \in (0 \dots \|I\|)) \to K \in (ℕ_{0} ∖ (0 \dots \|I\|))$
94	1 89 90 93 85	esplyfval2	Could not format ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( 0g ` ( I mPoly R ) ) ) : No typesetting found for \|- ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( 0g ` ( I mPoly R ) ) ) with typecode \|-
95		breq1	$⊢ h = f \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (f))$
96	1	eleq2i	$⊢ f \in D \leftrightarrow f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
97	96	bilani	$⊢ (φ \land f \in D) \to f \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
98	95 97	elrabrd	$⊢ (φ \land f \in D) \to {finSupp}_{0} (f)$
99	98	fsuppimpd	$⊢ (φ \land f \in D) \to f supp 0 \in Fin$
100		hashcl	$⊢ f supp 0 \in Fin \to \|f supp 0\| \in ℕ_{0}$
101	99 100	syl	$⊢ (φ \land f \in D) \to \|f supp 0\| \in ℕ_{0}$
102	101	nn0red	$⊢ (φ \land f \in D) \to \|f supp 0\| \in ℝ$
103	102	adantlr	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to \|f supp 0\| \in ℝ$
104		hashcl	$⊢ I \in Fin \to \|I\| \in ℕ_{0}$
105	2 104	syl	$⊢ φ \to \|I\| \in ℕ_{0}$
106	105	nn0red	$⊢ φ \to \|I\| \in ℝ$
107	106	ad2antrr	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to \|I\| \in ℝ$
108	4	nn0red	$⊢ φ \to K \in ℝ$
109	108	ad2antrr	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to K \in ℝ$
110		suppssdm	$⊢ f supp 0 \subseteq dom f$
111	1	ssrab3	$⊢ D \subseteq {ℕ_{0}}^{I}$
112	111	a1i	$⊢ φ \to D \subseteq {ℕ_{0}}^{I}$
113	112	sselda	$⊢ (φ \land f \in D) \to f \in ({ℕ_{0}}^{I})$
114	113	elmaprd	$⊢ (φ \land f \in D) \to f : I ⟶ ℕ_{0}$
115	110 114	fssdm	$⊢ (φ \land f \in D) \to f supp 0 \subseteq I$
116		hashss	$⊢ (I \in Fin \land f supp 0 \subseteq I) \to \|f supp 0\| \leq \|I\|$
117	2 115 116	syl2an2r	$⊢ (φ \land f \in D) \to \|f supp 0\| \leq \|I\|$
118	117	adantlr	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to \|f supp 0\| \leq \|I\|$
119	105	nn0zd	$⊢ φ \to \|I\| \in ℤ$
120	119	ad2antrr	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to \|I\| \in ℤ$
121		nn0diffz0	$⊢ \|I\| \in ℕ_{0} \to ℕ_{0} ∖ (0 \dots \|I\|) = ℤ_{\geq (\|I\| + 1)}$
122	89 104 121	3syl	$⊢ (φ \land \neg K \in (0 \dots \|I\|)) \to ℕ_{0} ∖ (0 \dots \|I\|) = ℤ_{\geq (\|I\| + 1)}$
123	93 122	eleqtrd	$⊢ (φ \land \neg K \in (0 \dots \|I\|)) \to K \in ℤ_{\geq (\|I\| + 1)}$
124	123	adantr	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to K \in ℤ_{\geq (\|I\| + 1)}$
125		eluzp1l	$⊢ (\|I\| \in ℤ \land K \in ℤ_{\geq (\|I\| + 1)}) \to \|I\| < K$
126	120 124 125	syl2anc	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to \|I\| < K$
127	103 107 109 118 126	lelttrd	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to \|f supp 0\| < K$
128	103 127	ltned	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to \|f supp 0\| \neq K$
129	128	neneqd	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to \neg \|f supp 0\| = K$
130	129	intnand	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to \neg (ran f \subseteq \{0, 1\} \land \|f supp 0\| = K)$
131	130	iffalsed	$⊢ ((φ \land \neg K \in (0 \dots \|I\|)) \land f \in D) \to if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
132	131	mpteq2dva	$⊢ (φ \land \neg K \in (0 \dots \|I\|)) \to (f \in D ⟼ if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), \underset{˙}{1}, \underset{˙}{0})) = (f \in D ⟼ \underset{˙}{0})$
133		fconstmpt	$⊢ D \times \{\underset{˙}{0}\} = (f \in D ⟼ \underset{˙}{0})$
134	132 133	eqtr4di	$⊢ (φ \land \neg K \in (0 \dots \|I\|)) \to (f \in D ⟼ if ((ran f \subseteq \{0, 1\} \land \|f supp 0\| = K), \underset{˙}{1}, \underset{˙}{0})) = D \times \{\underset{˙}{0}\}$
135	88 94 134	3eqtr4d	Could not format ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) ) : No typesetting found for \|- ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) ) with typecode \|-
136	82 135	pm2.61dan	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) ) : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` K ) = ( f e. D \|-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem esplyfval3

Proof