Theorem esplyval

Description: The elementary polynomials 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$$
Assertion	esplyval	Could not format assertion : 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 |-

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		df-esply	Could not format eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) ) : No typesetting found for |- eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) ) with typecode |-
5	4	a1i	Could not format ( ph -> eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) ) ) : No typesetting found for |- ( ph -> eSymPoly = ( i e. _V , r e. _V |-> ( k e. NN0 |-> ( ( ZRHom ` r ) o. ( ( _Ind ` { h e. ( NN0 ^m i ) | h finSupp 0 } ) ` ( ( _Ind ` i ) " { c e. ~P i | ( # ` c ) = k } ) ) ) ) ) ) with typecode |-
6		fveq2	$$⊢r=R\to \mathrm{\mathbb{Z}RHom}\left(r\right)=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
7	6	adantl	$$⊢\left(i=I\wedge r=R\right)\to \mathrm{\mathbb{Z}RHom}\left(r\right)=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
8		oveq2	$$⊢i=I\to {{\mathbb{N}}_0}^i={{\mathbb{N}}_0}^I$$
9	8	rabeqdv	$$⊢i=I\to \left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
10	9 1	eqtr4di	$$⊢i=I\to \left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}=D$$
11	10	fveq2d	$$⊢i=I\to {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}={𝟙}_D$$
12	11	adantr	$$⊢\left(i=I\wedge r=R\right)\to {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}={𝟙}_D$$
13		fveq2	$$⊢i=I\to {𝟙}_i={𝟙}_I$$
14	13	adantr	$$⊢\left(i=I\wedge r=R\right)\to {𝟙}_i={𝟙}_I$$
15		pweq	$$⊢i=I\to 𝒫i=𝒫I$$
16	15	rabeqdv	$$⊢i=I\to \left\{c\in 𝒫i|\left|c\right|=k\right\}=\left\{c\in 𝒫I|\left|c\right|=k\right\}$$
17	16	adantr	$$⊢\left(i=I\wedge r=R\right)\to \left\{c\in 𝒫i|\left|c\right|=k\right\}=\left\{c\in 𝒫I|\left|c\right|=k\right\}$$
18	14 17	imaeq12d	$$⊢\left(i=I\wedge r=R\right)\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]$$
19	12 18	fveq12d	$$⊢\left(i=I\wedge r=R\right)\to {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}\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)$$
20	7 19	coeq12d	$$⊢\left(i=I\wedge r=R\right)\to \mathrm{\mathbb{Z}RHom}\left(r\right)\circ {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}\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)$$
21	20	mpteq2dv	$$⊢\left(i=I\wedge r=R\right)\to \left(k\in {\mathbb{N}}_0⟼\mathrm{\mathbb{Z}RHom}\left(r\right)\circ {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}\left({𝟙}_i\left[\left\{c\in 𝒫i|\left|c\right|=k\right\}\right]\right)\right)=\left(k\in {\mathbb{N}}_0⟼\mathrm{\mathbb{Z}RHom}\left(R\right)\circ {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=k\right\}\right]\right)\right)$$
22	21	adantl	$$⊢\left(\phi \wedge \left(i=I\wedge r=R\right)\right)\to \left(k\in {\mathbb{N}}_0⟼\mathrm{\mathbb{Z}RHom}\left(r\right)\circ {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}}\left({𝟙}_i\left[\left\{c\in 𝒫i|\left|c\right|=k\right\}\right]\right)\right)=\left(k\in {\mathbb{N}}_0⟼\mathrm{\mathbb{Z}RHom}\left(R\right)\circ {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=k\right\}\right]\right)\right)$$
23	2	elexd	$$⊢\phi \to I\in \mathrm{V}$$
24	3	elexd	$$⊢\phi \to R\in \mathrm{V}$$
25		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
26	25	mptex	$$⊢\left(k\in {\mathbb{N}}_0⟼\mathrm{\mathbb{Z}RHom}\left(R\right)\circ {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=k\right\}\right]\right)\right)\in \mathrm{V}$$
27	26	a1i	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\mathrm{\mathbb{Z}RHom}\left(R\right)\circ {𝟙}_D\left({𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=k\right\}\right]\right)\right)\in \mathrm{V}$$
28	5 22 23 24 27	ovmpod	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 |-