This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem esplympl

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

Ref Expression
Hypotheses esplympl.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
esplympl.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplympl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
esplympl.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
esplympl.1 ⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
Assertion esplympl ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ 𝑀 )

Proof

Step Hyp Ref Expression
1 esplympl.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 esplympl.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
3 esplympl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 esplympl.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
5 esplympl.1 ⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
6 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
7 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
8 1 7 rabex2 ⊢ 𝐷 ∈ V
9 8 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
10 1 2 3 4 esplyfval ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) = ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) )
11 10 eqcomd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) = ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) )
12 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
13 12 zrhrhm ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
14 zringbas ⊢ ℤ = ( Base ‘ ℤring )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 14 15 rhmf ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
17 3 13 16 3syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
18 1 2 3 4 esplylem ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 )
19 indf ⊢ ( ( 𝐷 ∈ V ∧ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ⊆ 𝐷 ) → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
20 9 18 19 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ { 0 , 1 } )
21 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
22 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
23 21 22 prssd ⊢ ( 𝜑 → { 0 , 1 } ⊆ ℤ )
24 20 23 fssd ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) : 𝐷 ⟶ ℤ )
25 17 24 fcod ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
26 11 25 feq1dd ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
27 6 9 26 elmapdd ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
28 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
29 1 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
30 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
31 28 15 29 30 2 psrbas ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
32 27 31 eleqtrrd ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
33 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
34 zex ⊢ ℤ ∈ V
35 34 a1i ⊢ ( 𝜑 → ℤ ∈ V )
36 indf1o ⊢ ( 𝐼 ∈ Fin → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) )
37 f1of ⊢ ( ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 –1-1-onto→ ( { 0 , 1 } ↑m 𝐼 ) → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
38 2 36 37 3syl ⊢ ( 𝜑 → ( 𝟭 ‘ 𝐼 ) : 𝒫 𝐼 ⟶ ( { 0 , 1 } ↑m 𝐼 ) )
39 38 ffund ⊢ ( 𝜑 → Fun ( 𝟭 ‘ 𝐼 ) )
40 2 pwexd ⊢ ( 𝜑 → 𝒫 𝐼 ∈ V )
41 ssrab2 ⊢ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼
42 41 a1i ⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ⊆ 𝒫 𝐼 )
43 40 42 ssexd ⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ V )
44 hashcl ⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
45 2 44 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
46 4 nn0zd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
47 bccl ⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( ♯ ‘ 𝐼 ) C 𝐾 ) ∈ ℕ0 )
48 45 46 47 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) C 𝐾 ) ∈ ℕ0 )
49 hashbc ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐾 ∈ ℤ ) → ( ( ♯ ‘ 𝐼 ) C 𝐾 ) = ( ♯ ‘ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
50 2 46 49 syl2anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) C 𝐾 ) = ( ♯ ‘ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) )
51 50 eqcomd ⊢ ( 𝜑 → ( ♯ ‘ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) = ( ( ♯ ‘ 𝐼 ) C 𝐾 ) )
52 hashvnfin ⊢ ( ( { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ V ∧ ( ( ♯ ‘ 𝐼 ) C 𝐾 ) ∈ ℕ0 ) → ( ( ♯ ‘ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) = ( ( ♯ ‘ 𝐼 ) C 𝐾 ) → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ Fin ) )
53 52 imp ⊢ ( ( ( { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ V ∧ ( ( ♯ ‘ 𝐼 ) C 𝐾 ) ∈ ℕ0 ) ∧ ( ♯ ‘ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) = ( ( ♯ ‘ 𝐼 ) C 𝐾 ) ) → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ Fin )
54 43 48 51 53 syl21anc ⊢ ( 𝜑 → { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ Fin )
55 imafi ⊢ ( ( Fun ( 𝟭 ‘ 𝐼 ) ∧ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ∈ Fin ) → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∈ Fin )
56 39 54 55 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ∈ Fin )
57 9 18 56 indfsd ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) finSupp 0 )
58 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
59 12 58 zrh0 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
60 3 59 syl ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
61 33 21 20 17 23 9 35 57 60 fsuppcor ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝑅 ) ∘ ( ( 𝟭 ‘ 𝐷 ) ‘ ( ( 𝟭 ‘ 𝐼 ) “ { 𝑐 ∈ 𝒫 𝐼 ∣ ( ♯ ‘ 𝑐 ) = 𝐾 } ) ) ) finSupp ( 0g ‘ 𝑅 ) )
62 10 61 eqbrtrd ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) finSupp ( 0g ‘ 𝑅 ) )
63 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
64 63 28 30 58 5 mplelbas ⊢ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ 𝑀 ↔ ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) finSupp ( 0g ‘ 𝑅 ) ) )
65 32 62 64 sylanbrc ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ 𝑀 )