esplyfval2

Description: When K is out-of-bounds, the K -th elementary symmetric polynomial is zero. (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Hypotheses	esplyfval2.d	\|- D = { h e. ( NN0 ^m I ) \| h finSupp 0 }
	esplyfval2.i	\|- ( ph -> I e. Fin )
	esplyfval2.r	\|- ( ph -> R e. Ring )
	esplyfval2.k	\|- ( ph -> K e. ( NN0 \ ( 0 ... ( # ` I ) ) ) )
	esplyfval2.z	\|- Z = ( 0g ` ( I mPoly R ) )
Assertion	esplyfval2	\|- ( ph -> ( ( I eSymPoly R ) ` K ) = Z )

Proof

Step	Hyp	Ref	Expression
1		esplyfval2.d	\|- D = { h e. ( NN0 ^m I ) \| h finSupp 0 }
2		esplyfval2.i	\|- ( ph -> I e. Fin )
3		esplyfval2.r	\|- ( ph -> R e. Ring )
4		esplyfval2.k	\|- ( ph -> K e. ( NN0 \ ( 0 ... ( # ` I ) ) ) )
5		esplyfval2.z	\|- Z = ( 0g ` ( I mPoly R ) )
6	2	adantr	\|- ( ( ph /\ c e. ~P I ) -> I e. Fin )
7		elpwi	\|- ( c e. ~P I -> c C_ I )
8	7	adantl	\|- ( ( ph /\ c e. ~P I ) -> c C_ I )
9	6 8	ssfid	\|- ( ( ph /\ c e. ~P I ) -> c e. Fin )
10		hashcl	\|- ( c e. Fin -> ( # ` c ) e. NN0 )
11	9 10	syl	\|- ( ( ph /\ c e. ~P I ) -> ( # ` c ) e. NN0 )
12	11	nn0red	\|- ( ( ph /\ c e. ~P I ) -> ( # ` c ) e. RR )
13		hashcl	\|- ( I e. Fin -> ( # ` I ) e. NN0 )
14	2 13	syl	\|- ( ph -> ( # ` I ) e. NN0 )
15	14	nn0red	\|- ( ph -> ( # ` I ) e. RR )
16	15	adantr	\|- ( ( ph /\ c e. ~P I ) -> ( # ` I ) e. RR )
17	4	eldifad	\|- ( ph -> K e. NN0 )
18	17	nn0red	\|- ( ph -> K e. RR )
19	18	adantr	\|- ( ( ph /\ c e. ~P I ) -> K e. RR )
20		hashss	\|- ( ( I e. Fin /\ c C_ I ) -> ( # ` c ) <_ ( # ` I ) )
21	6 8 20	syl2anc	\|- ( ( ph /\ c e. ~P I ) -> ( # ` c ) <_ ( # ` I ) )
22	14	nn0zd	\|- ( ph -> ( # ` I ) e. ZZ )
23		nn0diffz0	\|- ( ( # ` I ) e. NN0 -> ( NN0 \ ( 0 ... ( # ` I ) ) ) = ( ZZ>= ` ( ( # ` I ) + 1 ) ) )
24	14 23	syl	\|- ( ph -> ( NN0 \ ( 0 ... ( # ` I ) ) ) = ( ZZ>= ` ( ( # ` I ) + 1 ) ) )
25	4 24	eleqtrd	\|- ( ph -> K e. ( ZZ>= ` ( ( # ` I ) + 1 ) ) )
26		eluzp1l	\|- ( ( ( # ` I ) e. ZZ /\ K e. ( ZZ>= ` ( ( # ` I ) + 1 ) ) ) -> ( # ` I ) < K )
27	22 25 26	syl2anc	\|- ( ph -> ( # ` I ) < K )
28	27	adantr	\|- ( ( ph /\ c e. ~P I ) -> ( # ` I ) < K )
29	12 16 19 21 28	lelttrd	\|- ( ( ph /\ c e. ~P I ) -> ( # ` c ) < K )
30	12 29	ltned	\|- ( ( ph /\ c e. ~P I ) -> ( # ` c ) =/= K )
31	30	neneqd	\|- ( ( ph /\ c e. ~P I ) -> -. ( # ` c ) = K )
32	31	ralrimiva	\|- ( ph -> A. c e. ~P I -. ( # ` c ) = K )
33		rabeq0	\|- ( { c e. ~P I \| ( # ` c ) = K } = (/) <-> A. c e. ~P I -. ( # ` c ) = K )
34	32 33	sylibr	\|- ( ph -> { c e. ~P I \| ( # ` c ) = K } = (/) )
35	34	imaeq2d	\|- ( ph -> ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) = ( ( _Ind ` I ) " (/) ) )
36		ima0	\|- ( ( _Ind ` I ) " (/) ) = (/)
37	35 36	eqtrdi	\|- ( ph -> ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) = (/) )
38	37	fveq2d	\|- ( ph -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) = ( ( _Ind ` D ) ` (/) ) )
39		ovex	\|- ( NN0 ^m I ) e. _V
40	1 39	rabex2	\|- D e. _V
41		indconst0	\|- ( D e. _V -> ( ( _Ind ` D ) ` (/) ) = ( D X. { 0 } ) )
42	40 41	mp1i	\|- ( ph -> ( ( _Ind ` D ) ` (/) ) = ( D X. { 0 } ) )
43	38 42	eqtrd	\|- ( ph -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) = ( D X. { 0 } ) )
44	43	coeq2d	\|- ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) = ( ( ZRHom ` R ) o. ( D X. { 0 } ) ) )
45		eqid	\|- ( ZRHom ` R ) = ( ZRHom ` R )
46	45	zrhrhm	\|- ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
47		zringbas	\|- ZZ = ( Base ` ZZring )
48		eqid	\|- ( Base ` R ) = ( Base ` R )
49	47 48	rhmf	\|- ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
50	3 46 49	3syl	\|- ( ph -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
51	50	ffnd	\|- ( ph -> ( ZRHom ` R ) Fn ZZ )
52		0zd	\|- ( ph -> 0 e. ZZ )
53		fcoconst	\|- ( ( ( ZRHom ` R ) Fn ZZ /\ 0 e. ZZ ) -> ( ( ZRHom ` R ) o. ( D X. { 0 } ) ) = ( D X. { ( ( ZRHom ` R ) ` 0 ) } ) )
54	51 52 53	syl2anc	\|- ( ph -> ( ( ZRHom ` R ) o. ( D X. { 0 } ) ) = ( D X. { ( ( ZRHom ` R ) ` 0 ) } ) )
55		eqid	\|- ( 0g ` R ) = ( 0g ` R )
56	45 55	zrh0	\|- ( R e. Ring -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
57	3 56	syl	\|- ( ph -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
58	57	sneqd	\|- ( ph -> { ( ( ZRHom ` R ) ` 0 ) } = { ( 0g ` R ) } )
59	58	xpeq2d	\|- ( ph -> ( D X. { ( ( ZRHom ` R ) ` 0 ) } ) = ( D X. { ( 0g ` R ) } ) )
60	44 54 59	3eqtrd	\|- ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) = ( D X. { ( 0g ` R ) } ) )
61	1 2 3 17	esplyfval	\|- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) )
62		eqid	\|- ( I mPoly R ) = ( I mPoly R )
63	1	psrbasfsupp	\|- D = { h e. ( NN0 ^m I ) \| ( `' h " NN ) e. Fin }
64	3	ringgrpd	\|- ( ph -> R e. Grp )
65	62 63 55 5 2 64	mpl0	\|- ( ph -> Z = ( D X. { ( 0g ` R ) } ) )
66	60 61 65	3eqtr4d	\|- ( ph -> ( ( I eSymPoly R ) ` K ) = Z )

Metamath Proof Explorer

Theorem esplyfval2

Proof