esplyfval

Description: The K -th elementary polynomial for a given index I of variables and base ring R . (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	esplyval.d	\|- D = { h e. ( NN0 ^m I ) \| h finSupp 0 }
	esplyval.i	\|- ( ph -> I e. V )
	esplyval.r	\|- ( ph -> R e. W )
	esplyfval.k	\|- ( ph -> K e. NN0 )
Assertion	esplyfval	\|- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) )

Step	Hyp	Ref	Expression
1		esplyval.d	\|- D = { h e. ( NN0 ^m I ) \| h finSupp 0 }
2		esplyval.i	\|- ( ph -> I e. V )
3		esplyval.r	\|- ( ph -> R e. W )
4		esplyfval.k	\|- ( ph -> K e. NN0 )
5		eqeq2	\|- ( k = K -> ( ( # ` c ) = k <-> ( # ` c ) = K ) )
6	5	rabbidv	\|- ( k = K -> { c e. ~P I \| ( # ` c ) = k } = { c e. ~P I \| ( # ` c ) = K } )
7	6	imaeq2d	\|- ( k = K -> ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = k } ) = ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) )
8	7	fveq2d	\|- ( k = K -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = k } ) ) = ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) )
9	8	coeq2d	\|- ( k = K -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = k } ) ) ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) )
10	1 2 3	esplyval	\|- ( ph -> ( I eSymPoly R ) = ( k e. NN0 \|-> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = k } ) ) ) ) )
11		fvexd	\|- ( ph -> ( ZRHom ` R ) e. _V )
12		fvexd	\|- ( ph -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) e. _V )
13	11 12	coexd	\|- ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) e. _V )
14	9 10 4 13	fvmptd4	\|- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) )

Metamath Proof Explorer