esplympl

Description: Elementary symmetric polynomials are polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	esplympl.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
	esplympl.i	$⊢ φ \to I \in Fin$
	esplympl.r	$⊢ φ \to R \in Ring$
	esplympl.k	$⊢ φ \to K \in ℕ_{0}$
	esplympl.1	$⊢ M = {Base}_{(I mPoly R)}$
Assertion	esplympl	Could not format assertion : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` K ) e. M ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		esplympl.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
2		esplympl.i	$⊢ φ \to I \in Fin$
3		esplympl.r	$⊢ φ \to R \in Ring$
4		esplympl.k	$⊢ φ \to K \in ℕ_{0}$
5		esplympl.1	$⊢ M = {Base}_{(I mPoly R)}$
6		fvexd	$⊢ φ \to {Base}_{R} \in V$
7		ovex	$⊢ {ℕ_{0}}^{I} \in V$
8	1 7	rabex2	$⊢ D \in V$
9	8	a1i	$⊢ φ \to D \in V$
10	1 2 3 4	esplyfval	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 \|-
11	10	eqcomd	Could not format ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) = ( ( I eSymPoly R ) ` K ) ) : No typesetting found for \|- ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I \| ( # ` c ) = K } ) ) ) = ( ( I eSymPoly R ) ` K ) ) with typecode \|-
12		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
13	12	zrhrhm	$⊢ R \in Ring \to ℤRHom (R) \in (ℤ_{ring} RingHom R)$
14		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16	14 15	rhmf	$⊢ ℤRHom (R) \in (ℤ_{ring} RingHom R) \to ℤRHom (R) : ℤ ⟶ {Base}_{R}$
17	3 13 16	3syl	$⊢ φ \to ℤRHom (R) : ℤ ⟶ {Base}_{R}$
18	1 2 3 4	esplylem	$⊢ φ \to 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D$
19		indf	$⊢ (D \in V \land 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \subseteq D) \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ \{0, 1\}$
20	9 18 19	syl2anc	$⊢ φ \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ \{0, 1\}$
21		0zd	$⊢ φ \to 0 \in ℤ$
22		1zzd	$⊢ φ \to 1 \in ℤ$
23	21 22	prssd	$⊢ φ \to \{0, 1\} \subseteq ℤ$
24	20 23	fssd	$⊢ φ \to 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]) : D ⟶ ℤ$
25	17 24	fcod	$⊢ φ \to (ℤRHom (R) \circ 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}])) : D ⟶ {Base}_{R}$
26	11 25	feq1dd	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) : D --> ( Base ` R ) ) : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` K ) : D --> ( Base ` R ) ) with typecode \|-
27	6 9 26	elmapdd	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) e. ( ( Base ` R ) ^m D ) ) : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` K ) e. ( ( Base ` R ) ^m D ) ) with typecode \|-
28		eqid	$⊢ I mPwSer R = I mPwSer R$
29	1	psrbasfsupp	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
30		eqid	$⊢ {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer R)}$
31	28 15 29 30 2	psrbas	$⊢ φ \to {Base}_{(I mPwSer R)} = {Base}_{R}^{D}$
32	27 31	eleqtrrd	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPwSer R ) ) ) : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPwSer R ) ) ) with typecode \|-
33		fvexd	$⊢ φ \to 0_{R} \in V$
34		zex	$⊢ ℤ \in V$
35	34	a1i	$⊢ φ \to ℤ \in V$
36		indf1o	$⊢ I \in Fin \to 𝟙_{I} : 𝒫 I \underset{1-1 onto}{⟶} {\{0, 1\}}^{I}$
37		f1of	$⊢ 𝟙_{I} : 𝒫 I \underset{1-1 onto}{⟶} {\{0, 1\}}^{I} \to 𝟙_{I} : 𝒫 I ⟶ {\{0, 1\}}^{I}$
38	2 36 37	3syl	$⊢ φ \to 𝟙_{I} : 𝒫 I ⟶ {\{0, 1\}}^{I}$
39	38	ffund	$⊢ φ \to Fun 𝟙_{I}$
40	2	pwexd	$⊢ φ \to 𝒫 I \in V$
41		ssrab2	$⊢ \{c \in 𝒫 I \| \|c\| = K\} \subseteq 𝒫 I$
42	41	a1i	$⊢ φ \to \{c \in 𝒫 I \| \|c\| = K\} \subseteq 𝒫 I$
43	40 42	ssexd	$⊢ φ \to \{c \in 𝒫 I \| \|c\| = K\} \in V$
44		hashcl	$⊢ I \in Fin \to \|I\| \in ℕ_{0}$
45	2 44	syl	$⊢ φ \to \|I\| \in ℕ_{0}$
46	4	nn0zd	$⊢ φ \to K \in ℤ$
47		bccl	$⊢ (\|I\| \in ℕ_{0} \land K \in ℤ) \to (\binom{\|I\|}{K}) \in ℕ_{0}$
48	45 46 47	syl2anc	$⊢ φ \to (\binom{\|I\|}{K}) \in ℕ_{0}$
49		hashbc	$⊢ (I \in Fin \land K \in ℤ) \to (\binom{\|I\|}{K}) = \|\{c \in 𝒫 I \| \|c\| = K\}\|$
50	2 46 49	syl2anc	$⊢ φ \to (\binom{\|I\|}{K}) = \|\{c \in 𝒫 I \| \|c\| = K\}\|$
51	50	eqcomd	$⊢ φ \to \|\{c \in 𝒫 I \| \|c\| = K\}\| = (\binom{\|I\|}{K})$
52		hashvnfin	$⊢ (\{c \in 𝒫 I \| \|c\| = K\} \in V \land (\binom{\|I\|}{K}) \in ℕ_{0}) \to (\|\{c \in 𝒫 I \| \|c\| = K\}\| = (\binom{\|I\|}{K}) \to \{c \in 𝒫 I \| \|c\| = K\} \in Fin)$
53	52	imp	$⊢ ((\{c \in 𝒫 I \| \|c\| = K\} \in V \land (\binom{\|I\|}{K}) \in ℕ_{0}) \land \|\{c \in 𝒫 I \| \|c\| = K\}\| = (\binom{\|I\|}{K})) \to \{c \in 𝒫 I \| \|c\| = K\} \in Fin$
54	43 48 51 53	syl21anc	$⊢ φ \to \{c \in 𝒫 I \| \|c\| = K\} \in Fin$
55		imafi	$⊢ (Fun 𝟙_{I} \land \{c \in 𝒫 I \| \|c\| = K\} \in Fin) \to 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \in Fin$
56	39 54 55	syl2anc	$⊢ φ \to 𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}] \in Fin$
57	9 18 56	indfsd	$⊢ φ \to {finSupp}_{0} (𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}]))$
58		eqid	$⊢ 0_{R} = 0_{R}$
59	12 58	zrh0	$⊢ R \in Ring \to ℤRHom (R) (0) = 0_{R}$
60	3 59	syl	$⊢ φ \to ℤRHom (R) (0) = 0_{R}$
61	33 21 20 17 23 9 35 57 60	fsuppcor	$⊢ φ \to {finSupp}_{0_{R}} ((ℤRHom (R) \circ 𝟙_{D} (𝟙_{I} [\{c \in 𝒫 I \| \|c\| = K\}])))$
62	10 61	eqbrtrd	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) finSupp ( 0g ` R ) ) : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` K ) finSupp ( 0g ` R ) ) with typecode \|-
63		eqid	$⊢ I mPoly R = I mPoly R$
64	63 28 30 58 5	mplelbas	Could not format ( ( ( I eSymPoly R ) ` K ) e. M <-> ( ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPwSer R ) ) /\ ( ( I eSymPoly R ) ` K ) finSupp ( 0g ` R ) ) ) : No typesetting found for \|- ( ( ( I eSymPoly R ) ` K ) e. M <-> ( ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPwSer R ) ) /\ ( ( I eSymPoly R ) ` K ) finSupp ( 0g ` R ) ) ) with typecode \|-
65	32 62 64	sylanbrc	Could not format ( ph -> ( ( I eSymPoly R ) ` K ) e. M ) : No typesetting found for \|- ( ph -> ( ( I eSymPoly R ) ` K ) e. M ) with typecode \|-

Metamath Proof Explorer

Theorem esplympl

Proof