Metamath Proof Explorer

Theorem splysubrg

Description: The symmetric polynomials form a subring of the ring of polynomials. (Contributed by Thierry Arnoux, 15-Jan-2026)

Ref Expression
Hypotheses splyval.s ⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
splyval.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
splyval.m ⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
splyval.a ⊢ 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
splyval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
splysubrg.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion splysubrg ( 𝜑 → ( 𝐼 SymPoly 𝑅 ) ∈ ( SubRing ‘ ( 𝐼 mPoly 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 splyval.s ⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
2 splyval.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
3 splyval.m ⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
4 splyval.a ⊢ 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
5 splyval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 splysubrg.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 1 2 3 4 5 6 splyval ⊢ ( 𝜑 → ( 𝐼 SymPoly 𝑅 ) = ( 𝑀 FixPts 𝐴 ) )
8 eqid ⊢ ( 𝑓 ∈ 𝑀 ↦ ( 𝑑 𝐴 𝑓 ) ) = ( 𝑓 ∈ 𝑀 ↦ ( 𝑑 𝐴 𝑓 ) )
9 1 2 3 4 5 mplvrpmga ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 GrpAct 𝑀 ) )
10 coeq2 ⊢ ( 𝑑 = 𝑒 → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝑒 ) )
11 10 fveq2d ⊢ ( 𝑑 = 𝑒 → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( 𝑓 ‘ ( 𝑥 ∘ 𝑒 ) ) )
12 11 mpteq2dv ⊢ ( 𝑑 = 𝑒 → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑒 ) ) ) )
13 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ ( 𝑥 ∘ 𝑒 ) ) = ( 𝑔 ‘ ( 𝑥 ∘ 𝑒 ) ) )
14 13 mpteq2dv ⊢ ( 𝑓 = 𝑔 → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑒 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ 𝑒 ) ) ) )
15 12 14 cbvmpov ⊢ ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) = ( 𝑒 ∈ 𝑃 , 𝑔 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ 𝑒 ) ) ) )
16 4 15 eqtri ⊢ 𝐴 = ( 𝑒 ∈ 𝑃 , 𝑔 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ 𝑒 ) ) ) )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) → 𝐼 ∈ 𝑉 )
18 oveq2 ⊢ ( 𝑓 = 𝑔 → ( 𝑑 𝐴 𝑓 ) = ( 𝑑 𝐴 𝑔 ) )
19 18 cbvmptv ⊢ ( 𝑓 ∈ 𝑀 ↦ ( 𝑑 𝐴 𝑓 ) ) = ( 𝑔 ∈ 𝑀 ↦ ( 𝑑 𝐴 𝑔 ) )
20 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
21 6 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) → 𝑅 ∈ Ring )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) → 𝑑 ∈ 𝑃 )
23 1 2 3 16 17 19 20 21 22 mplvrpmrhm ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) → ( 𝑓 ∈ 𝑀 ↦ ( 𝑑 𝐴 𝑓 ) ) ∈ ( ( 𝐼 mPoly 𝑅 ) RingHom ( 𝐼 mPoly 𝑅 ) ) )
24 2 3 8 9 23 fxpsubrg ⊢ ( 𝜑 → ( 𝑀 FixPts 𝐴 ) ∈ ( SubRing ‘ ( 𝐼 mPoly 𝑅 ) ) )
25 7 24 eqeltrd ⊢ ( 𝜑 → ( 𝐼 SymPoly 𝑅 ) ∈ ( SubRing ‘ ( 𝐼 mPoly 𝑅 ) ) )