Theorem esplyfval0

Description: The 0 -th elementary symmetric polynomial is the constant 1 . (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	esplyfval0.i	$$⊢\phi \to I\in V$$
	esplyfval0.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	esplyfval0.0	$$⊢U=1_{\left(I\mathrm{mPoly}R\right)}$$
Assertion	esplyfval0	Could not format assertion : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` 0 ) = U ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		esplyfval0.i	$$⊢\phi \to I\in V$$
2		esplyfval0.r	$$⊢\phi \to R\in \mathrm{Ring}$$
3		esplyfval0.0	$$⊢U=1_{\left(I\mathrm{mPoly}R\right)}$$
4		eqid	$$⊢\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\}$$
5	4 1 2	esplyval	Could not format ( ph -> ( I eSymPoly R ) = ( 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 -> ( I eSymPoly R ) = ( 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		eqeq2	$$⊢k=0\to \left(\left|c\right|=k\leftrightarrow \left|c\right|=0\right)$$
7	6	rabbidv	$$⊢k=0\to \left\{c\in 𝒫I|\left|c\right|=k\right\}=\left\{c\in 𝒫I|\left|c\right|=0\right\}$$
8	7	imaeq2d	$$⊢k=0\to {𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=k\right\}\right]={𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=0\right\}\right]$$
9	8	fveq2d	$$⊢k=0\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)={𝟙}_{\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|=0\right\}\right]\right)$$
10	9	coeq2d	$$⊢k=0\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 {𝟙}_{\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|=0\right\}\right]\right)$$
11		fvif	$$⊢\mathrm{\mathbb{Z}RHom}\left(R\right)\left(if\left(f=I\times \left\{0\right\},1,0\right)\right)=if\left(f=I\times \left\{0\right\},\mathrm{\mathbb{Z}RHom}\left(R\right)\left(1\right),\mathrm{\mathbb{Z}RHom}\left(R\right)\left(0\right)\right)$$
12		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(R\right)=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
13		eqid	$$⊢1_R=1_R$$
14	12 13	zrh1	$$⊢R\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(R\right)\left(1\right)=1_R$$
15	2 14	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(R\right)\left(1\right)=1_R$$
16		eqid	$$⊢0_R=0_R$$
17	12 16	zrh0	$$⊢R\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(R\right)\left(0\right)=0_R$$
18	2 17	syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(R\right)\left(0\right)=0_R$$
19	15 18	ifeq12d	$$⊢\phi \to if\left(f=I\times \left\{0\right\},\mathrm{\mathbb{Z}RHom}\left(R\right)\left(1\right),\mathrm{\mathbb{Z}RHom}\left(R\right)\left(0\right)\right)=if\left(f=I\times \left\{0\right\},1_R,0_R\right)$$
20	19	adantr	$$⊢\left(\phi \wedge f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to if\left(f=I\times \left\{0\right\},\mathrm{\mathbb{Z}RHom}\left(R\right)\left(1\right),\mathrm{\mathbb{Z}RHom}\left(R\right)\left(0\right)\right)=if\left(f=I\times \left\{0\right\},1_R,0_R\right)$$
21	11 20	eqtrid	$$⊢\left(\phi \wedge f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to \mathrm{\mathbb{Z}RHom}\left(R\right)\left(if\left(f=I\times \left\{0\right\},1,0\right)\right)=if\left(f=I\times \left\{0\right\},1_R,0_R\right)$$
22	21	mpteq2dva	$$⊢\phi \to \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\mathrm{\mathbb{Z}RHom}\left(R\right)\left(if\left(f=I\times \left\{0\right\},1,0\right)\right)\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(f=I\times \left\{0\right\},1_R,0_R\right)\right)$$
23		1zzd	$$⊢\left(\phi \wedge f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 1\in \mathbb{Z}$$
24		0zd	$$⊢\left(\phi \wedge f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to 0\in \mathbb{Z}$$
25	23 24	ifcld	$$⊢\left(\phi \wedge f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to if\left(f=I\times \left\{0\right\},1,0\right)\in \mathbb{Z}$$
26		fveqeq2	$$⊢c=\varnothing \to \left(\left|c\right|=0\leftrightarrow \left|\varnothing \right|=0\right)$$
27		0elpw	$$⊢\varnothing \in 𝒫I$$
28	27	a1i	$$⊢\phi \to \varnothing \in 𝒫I$$
29		hash0	$$⊢\left|\varnothing \right|=0$$
30	29	a1i	$$⊢\phi \to \left|\varnothing \right|=0$$
31		hasheq0	$$⊢c\in 𝒫I\to \left(\left|c\right|=0\leftrightarrow c=\varnothing \right)$$
32	31	biimpa	$$⊢\left(c\in 𝒫I\wedge \left|c\right|=0\right)\to c=\varnothing$$
33	32	adantll	$$⊢\left(\left(\phi \wedge c\in 𝒫I\right)\wedge \left|c\right|=0\right)\to c=\varnothing$$
34	26 28 30 33	rabeqsnd	$$⊢\phi \to \left\{c\in 𝒫I|\left|c\right|=0\right\}=\left\{\varnothing \right\}$$
35	34	imaeq2d	$$⊢\phi \to {𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=0\right\}\right]={𝟙}_I\left[\left\{\varnothing \right\}\right]$$
36		indf1o	$$⊢I\in V\to {𝟙}_I:𝒫I\underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^I$$
37		f1of	$$⊢{𝟙}_I:𝒫I\underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^I\to {𝟙}_I:𝒫I⟶{\left\{0,1\right\}}^I$$
38	1 36 37	3syl	$$⊢\phi \to {𝟙}_I:𝒫I⟶{\left\{0,1\right\}}^I$$
39	38	ffnd	$$⊢\phi \to {𝟙}_{I}Fn𝒫I$$
40	39 28	fnimasnd	$$⊢\phi \to {𝟙}_I\left[\left\{\varnothing \right\}\right]=\left\{{𝟙}_I\left(\varnothing \right)\right\}$$
41		indconst0	$$⊢I\in V\to {𝟙}_I\left(\varnothing \right)=I\times \left\{0\right\}$$
42	1 41	syl	$$⊢\phi \to {𝟙}_I\left(\varnothing \right)=I\times \left\{0\right\}$$
43	42	sneqd	$$⊢\phi \to \left\{{𝟙}_I\left(\varnothing \right)\right\}=\left\{I\times \left\{0\right\}\right\}$$
44	35 40 43	3eqtrd	$$⊢\phi \to {𝟙}_I\left[\left\{c\in 𝒫I|\left|c\right|=0\right\}\right]=\left\{I\times \left\{0\right\}\right\}$$
45	44	fveq2d	$$⊢\phi \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|=0\right\}\right]\right)={𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}}\left(\left\{I\times \left\{0\right\}\right\}\right)$$
46		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
47	46	rabex	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}$$
48		breq1	$$⊢h=I\times \left\{0\right\}\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(\left(I\times \left\{0\right\}\right)\right)\right)$$
49		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
50	49	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
51		c0ex	$$⊢0\in \mathrm{V}$$
52	51	fconst	$$⊢\left(I\times \left\{0\right\}\right):I⟶\left\{0\right\}$$
53	52	a1i	$$⊢\phi \to \left(I\times \left\{0\right\}\right):I⟶\left\{0\right\}$$
54		0nn0	$$⊢0\in {\mathbb{N}}_0$$
55	54	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
56	55	snssd	$$⊢\phi \to \left\{0\right\}\subseteq {\mathbb{N}}_0$$
57	53 56	fssd	$$⊢\phi \to \left(I\times \left\{0\right\}\right):I⟶{\mathbb{N}}_0$$
58	50 1 57	elmapdd	$$⊢\phi \to I\times \left\{0\right\}\in \left({{\mathbb{N}}_0}^I\right)$$
59		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
60	1 59	fczfsuppd	$$⊢\phi \to {finSupp}_0\left(\left(I\times \left\{0\right\}\right)\right)$$
61	48 58 60	elrabd	$$⊢\phi \to I\times \left\{0\right\}\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
62		indsn	$$⊢\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\in \mathrm{V}\wedge I\times \left\{0\right\}\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}\right)\to {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}}\left(\left\{I\times \left\{0\right\}\right\}\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(f=I\times \left\{0\right\},1,0\right)\right)$$
63	47 61 62	sylancr	$$⊢\phi \to {𝟙}_{\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}}\left(\left\{I\times \left\{0\right\}\right\}\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(f=I\times \left\{0\right\},1,0\right)\right)$$
64	45 63	eqtrd	$$⊢\phi \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|=0\right\}\right]\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(f=I\times \left\{0\right\},1,0\right)\right)$$
65	12	zrhrhm	$$⊢R\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(R\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
66		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
67		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
68	66 67	rhmf	$$⊢\mathrm{\mathbb{Z}RHom}\left(R\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)\to \mathrm{\mathbb{Z}RHom}\left(R\right):\mathbb{Z}⟶{\mathrm{Base}}_R$$
69	2 65 68	3syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(R\right):\mathbb{Z}⟶{\mathrm{Base}}_R$$
70	69	feqmptd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(R\right)=\left(z\in \mathbb{Z}⟼\mathrm{\mathbb{Z}RHom}\left(R\right)\left(z\right)\right)$$
71		fveq2	$$⊢z=if\left(f=I\times \left\{0\right\},1,0\right)\to \mathrm{\mathbb{Z}RHom}\left(R\right)\left(z\right)=\mathrm{\mathbb{Z}RHom}\left(R\right)\left(if\left(f=I\times \left\{0\right\},1,0\right)\right)$$
72	25 64 70 71	fmptco	$$⊢\phi \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|=0\right\}\right]\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼\mathrm{\mathbb{Z}RHom}\left(R\right)\left(if\left(f=I\times \left\{0\right\},1,0\right)\right)\right)$$
73		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
74	4	psrbasfsupp	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
75	73 74 16 13 3 1 2	mpl1	$$⊢\phi \to U=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼if\left(f=I\times \left\{0\right\},1_R,0_R\right)\right)$$
76	22 72 75	3eqtr4d	$$⊢\phi \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|=0\right\}\right]\right)=U$$
77	10 76	sylan9eqr	$$⊢\left(\phi \wedge k=0\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)=U$$
78	3	fvexi	$$⊢U\in \mathrm{V}$$
79	78	a1i	$$⊢\phi \to U\in \mathrm{V}$$
80	5 77 55 79	fvmptd	Could not format ( ph -> ( ( I eSymPoly R ) ` 0 ) = U ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` 0 ) = U ) with typecode |-