Metamath Proof Explorer

Theorem esplysply

Description: The K -th elementary symmetric polynomial is symmetric. (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses esplyfv.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
esplyfv.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplyfv.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
esplyfv.k ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) )
Assertion esplysply ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( 𝐼 SymPoly 𝑅 ) )

Proof

Step Hyp Ref Expression
1 esplyfv.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 esplyfv.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
3 esplyfv.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 esplyfv.k ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) )
5 eqid ⊢ ( SymGrp ‘ 𝐼 ) = ( SymGrp ‘ 𝐼 )
6 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) = ( Base ‘ ( SymGrp ‘ 𝐼 ) )
7 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
8 elfznn0 ⊢ ( 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) → 𝐾 ∈ ℕ0 )
9 4 8 syl ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
10 1 2 3 9 7 esplympl ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
11 1 ssrab3 ⊢ 𝐷 ⊆ ( ℕ0 ↑m 𝐼 )
12 11 a1i ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) → 𝐷 ⊆ ( ℕ0 ↑m 𝐼 ) )
13 12 sselda ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) )
14 13 elmaprd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 : 𝐼 ⟶ ℕ0 )
15 14 fdmd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → dom 𝑥 = 𝐼 )
16 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) )
17 5 6 symgbasf1o ⊢ ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) → 𝑝 : 𝐼 –1-1-onto→ 𝐼 )
18 16 17 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑝 : 𝐼 –1-1-onto→ 𝐼 )
19 f1ofo ⊢ ( 𝑝 : 𝐼 –1-1-onto→ 𝐼 → 𝑝 : 𝐼 –onto→ 𝐼 )
20 forn ⊢ ( 𝑝 : 𝐼 –onto→ 𝐼 → ran 𝑝 = 𝐼 )
21 18 19 20 3syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ran 𝑝 = 𝐼 )
22 15 21 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → dom 𝑥 = ran 𝑝 )
23 rncoeq ⊢ ( dom 𝑥 = ran 𝑝 → ran ( 𝑥 ∘ 𝑝 ) = ran 𝑥 )
24 22 23 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ran ( 𝑥 ∘ 𝑝 ) = ran 𝑥 )
25 24 sseq1d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ran ( 𝑥 ∘ 𝑝 ) ⊆ { 0 , 1 } ↔ ran 𝑥 ⊆ { 0 , 1 } ) )
26 f1ocnv ⊢ ( 𝑝 : 𝐼 –1-1-onto→ 𝐼 → ◡ 𝑝 : 𝐼 –1-1-onto→ 𝐼 )
27 f1of1 ⊢ ( ◡ 𝑝 : 𝐼 –1-1-onto→ 𝐼 → ◡ 𝑝 : 𝐼 –1-1→ 𝐼 )
28 18 26 27 3syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ◡ 𝑝 : 𝐼 –1-1→ 𝐼 )
29 cnvimass ⊢ ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) ⊆ dom 𝑥
30 29 14 fssdm ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) ⊆ 𝐼 )
31 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝐼 ∈ Fin )
32 28 30 31 hashimaf1 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ♯ ‘ ( ◡ 𝑝 “ ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) ) ) = ( ♯ ‘ ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) ) )
33 c0ex ⊢ 0 ∈ V
34 33 a1i ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 0 ∈ V )
35 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) → 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) )
36 f1of ⊢ ( 𝑝 : 𝐼 –1-1-onto→ 𝐼 → 𝑝 : 𝐼 ⟶ 𝐼 )
37 35 17 36 3syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) → 𝑝 : 𝐼 ⟶ 𝐼 )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑝 : 𝐼 ⟶ 𝐼 )
39 14 38 fcod ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ∘ 𝑝 ) : 𝐼 ⟶ ℕ0 )
40 fsuppeq ⊢ ( ( 𝐼 ∈ Fin ∧ 0 ∈ V ) → ( ( 𝑥 ∘ 𝑝 ) : 𝐼 ⟶ ℕ0 → ( ( 𝑥 ∘ 𝑝 ) supp 0 ) = ( ◡ ( 𝑥 ∘ 𝑝 ) “ ( ℕ0 ∖ { 0 } ) ) ) )
41 40 imp ⊢ ( ( ( 𝐼 ∈ Fin ∧ 0 ∈ V ) ∧ ( 𝑥 ∘ 𝑝 ) : 𝐼 ⟶ ℕ0 ) → ( ( 𝑥 ∘ 𝑝 ) supp 0 ) = ( ◡ ( 𝑥 ∘ 𝑝 ) “ ( ℕ0 ∖ { 0 } ) ) )
42 31 34 39 41 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ∘ 𝑝 ) supp 0 ) = ( ◡ ( 𝑥 ∘ 𝑝 ) “ ( ℕ0 ∖ { 0 } ) ) )
43 cnvco ⊢ ◡ ( 𝑥 ∘ 𝑝 ) = ( ◡ 𝑝 ∘ ◡ 𝑥 )
44 43 imaeq1i ⊢ ( ◡ ( 𝑥 ∘ 𝑝 ) “ ( ℕ0 ∖ { 0 } ) ) = ( ( ◡ 𝑝 ∘ ◡ 𝑥 ) “ ( ℕ0 ∖ { 0 } ) )
45 imaco ⊢ ( ( ◡ 𝑝 ∘ ◡ 𝑥 ) “ ( ℕ0 ∖ { 0 } ) ) = ( ◡ 𝑝 “ ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) )
46 44 45 eqtri ⊢ ( ◡ ( 𝑥 ∘ 𝑝 ) “ ( ℕ0 ∖ { 0 } ) ) = ( ◡ 𝑝 “ ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) )
47 42 46 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ∘ 𝑝 ) supp 0 ) = ( ◡ 𝑝 “ ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) ) )
48 47 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ♯ ‘ ( ( 𝑥 ∘ 𝑝 ) supp 0 ) ) = ( ♯ ‘ ( ◡ 𝑝 “ ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) ) ) )
49 fsuppeq ⊢ ( ( 𝐼 ∈ Fin ∧ 0 ∈ V ) → ( 𝑥 : 𝐼 ⟶ ℕ0 → ( 𝑥 supp 0 ) = ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) ) )
50 49 imp ⊢ ( ( ( 𝐼 ∈ Fin ∧ 0 ∈ V ) ∧ 𝑥 : 𝐼 ⟶ ℕ0 ) → ( 𝑥 supp 0 ) = ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) )
51 31 34 14 50 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 supp 0 ) = ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) )
52 51 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑥 supp 0 ) ) = ( ♯ ‘ ( ◡ 𝑥 “ ( ℕ0 ∖ { 0 } ) ) ) )
53 32 48 52 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ♯ ‘ ( ( 𝑥 ∘ 𝑝 ) supp 0 ) ) = ( ♯ ‘ ( 𝑥 supp 0 ) ) )
54 53 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ♯ ‘ ( ( 𝑥 ∘ 𝑝 ) supp 0 ) ) = 𝐾 ↔ ( ♯ ‘ ( 𝑥 supp 0 ) ) = 𝐾 ) )
55 25 54 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ran ( 𝑥 ∘ 𝑝 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑥 ∘ 𝑝 ) supp 0 ) ) = 𝐾 ) ↔ ( ran 𝑥 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑥 supp 0 ) ) = 𝐾 ) ) )
56 55 ifbid ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → if ( ( ran ( 𝑥 ∘ 𝑝 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑥 ∘ 𝑝 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( ( ran 𝑥 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑥 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
57 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑅 ∈ Ring )
58 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐼 ) ) )
59 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
60 59 1 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
61 5 6 31 16 60 mplvrpmlem ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ∘ 𝑝 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
62 61 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ∘ 𝑝 ) ∈ 𝐷 )
63 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
64 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
65 1 31 57 58 62 63 64 esplyfv ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ ( 𝑥 ∘ 𝑝 ) ) = if ( ( ran ( 𝑥 ∘ 𝑝 ) ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( ( 𝑥 ∘ 𝑝 ) supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
66 1 31 57 58 59 63 64 esplyfv ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑥 ) = if ( ( ran 𝑥 ⊆ { 0 , 1 } ∧ ( ♯ ‘ ( 𝑥 supp 0 ) ) = 𝐾 ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
67 56 65 66 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝐼 ) ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ ( 𝑥 ∘ 𝑝 ) ) = ( ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ‘ 𝑥 ) )
68 5 6 7 1 2 3 10 67 issply ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( 𝐼 SymPoly 𝑅 ) )