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

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