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

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 ⊢ S = SymGrp ⁡ I
splyval.p ⊢ P = Base S
splyval.m ⊢ M = Base I mPoly R
splyval.a ⊢ A = d ∈ P , f ∈ M ⟼ x ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h ⟼ f ⁡ x ∘ d
splyval.i ⊢ φ → I ∈ V
splysubrg.r ⊢ φ → R ∈ Ring
Assertion splysubrg Could not format assertion : No typesetting found for |- ( ph -> ( I SymPoly R ) e. ( SubRing ` ( I mPoly R ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 splyval.s ⊢ S = SymGrp ⁡ I
2 splyval.p ⊢ P = Base S
3 splyval.m ⊢ M = Base I mPoly R
4 splyval.a ⊢ A = d ∈ P , f ∈ M ⟼ x ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h ⟼ f ⁡ x ∘ d
5 splyval.i ⊢ φ → I ∈ V
6 splysubrg.r ⊢ φ → R ∈ Ring
7 1 2 3 4 5 6 splyval Could not format ( ph -> ( I SymPoly R ) = ( M FixPts A ) ) : No typesetting found for |- ( ph -> ( I SymPoly R ) = ( M FixPts A ) ) with typecode |-
8 eqid ⊢ f ∈ M ⟼ d A f = f ∈ M ⟼ d A f
9 1 2 3 4 5 mplvrpmga ⊢ φ → A ∈ S GrpAct M
10 coeq2 ⊢ d = e → x ∘ d = x ∘ e
11 10 fveq2d ⊢ d = e → f ⁡ x ∘ d = f ⁡ x ∘ e
12 11 mpteq2dv ⊢ d = e → x ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h ⟼ f ⁡ x ∘ d = x ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h ⟼ f ⁡ x ∘ e
13 fveq1 ⊢ f = g → f ⁡ x ∘ e = g ⁡ x ∘ e
14 13 mpteq2dv ⊢ f = g → x ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h ⟼ f ⁡ x ∘ e = x ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h ⟼ g ⁡ x ∘ e
15 12 14 cbvmpov ⊢ d ∈ P , f ∈ M ⟼ x ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h ⟼ f ⁡ x ∘ d = e ∈ P , g ∈ M ⟼ x ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h ⟼ g ⁡ x ∘ e
16 4 15 eqtri ⊢ A = e ∈ P , g ∈ M ⟼ x ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h ⟼ g ⁡ x ∘ e
17 5 adantr ⊢ φ ∧ d ∈ P → I ∈ V
18 oveq2 ⊢ f = g → d A f = d A g
19 18 cbvmptv ⊢ f ∈ M ⟼ d A f = g ∈ M ⟼ d A g
20 eqid ⊢ I mPoly R = I mPoly R
21 6 adantr ⊢ φ ∧ d ∈ P → R ∈ Ring
22 simpr ⊢ φ ∧ d ∈ P → d ∈ P
23 1 2 3 16 17 19 20 21 22 mplvrpmrhm ⊢ φ ∧ d ∈ P → f ∈ M ⟼ d A f ∈ I mPoly R RingHom I mPoly R
24 2 3 8 9 23 fxpsubrg Could not format ( ph -> ( M FixPts A ) e. ( SubRing ` ( I mPoly R ) ) ) : No typesetting found for |- ( ph -> ( M FixPts A ) e. ( SubRing ` ( I mPoly R ) ) ) with typecode |-
25 7 24 eqeltrd Could not format ( ph -> ( I SymPoly R ) e. ( SubRing ` ( I mPoly R ) ) ) : No typesetting found for |- ( ph -> ( I SymPoly R ) e. ( SubRing ` ( I mPoly R ) ) ) with typecode |-