Theorem 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 } ) ) ) )

Proof

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 } ) ) ) )