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=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	esplyval.i	$$⊢\phi \to I\in V$$
	esplyval.r	$$⊢\phi \to R\in W$$
	esplyfval.k	$$⊢\phi \to K\in {\mathbb{N}}_0$$
Assertion	esplyfval	Could not format assertion : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		esplyval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
2		esplyval.i	$$⊢\phi \to I\in V$$
3		esplyval.r	$$⊢\phi \to R\in W$$
4		esplyfval.k	$$⊢\phi \to K\in {\mathbb{N}}_0$$
5		eqeq2	$$⊢k=K\to \left(\left|c\right|=k\leftrightarrow \left|c\right|=K\right)$$
6	5	rabbidv	$$⊢k=K\to \left\{c\in 𝒫I|\left|c\right|=k\right\}=\left\{c\in 𝒫I|\left|c\right|=K\right\}$$
7	6	imaeq2d	$$⊢k=K\to {𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=k\right\}\right]={𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]$$
8	7	fveq2d	$$⊢k=K\to {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=k\right\}\right]\right)={𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)$$
9	8	coeq2d	$$⊢k=K\to \mathrm{\mathbb{Z}RHom}\left(R\right)\circ {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=k\right\}\right]\right)=\mathrm{\mathbb{Z}RHom}\left(R\right)\circ {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)$$
10	1 2 3	esplyval	Could not format ( ph -> ( I eSymPoly R ) = ( k e. NN0 |-> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = k } ) ) ) ) ) : No typesetting found for |- ( ph -> ( I eSymPoly R ) = ( k e. NN0 |-> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = k } ) ) ) ) ) with typecode |-
11		fvexd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(R\right)\in \mathrm{V}$$
12		fvexd	$$⊢\phi \to {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)\in \mathrm{V}$$
13	11 12	coexd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(R\right)\circ {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=K\right\}\right]\right)\in \mathrm{V}$$
14	9 10 4 13	fvmptd4	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ) with typecode |-