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=\mathrm{SymGrp}\left(I\right)$$
	splyval.p	$$⊢P={\mathrm{Base}}_S$$
	splyval.m	$$⊢M={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
	splyval.a	$$⊢A=\left(d\in P,f\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)\right)$$
	splyval.i	$$⊢\phi \to I\in V$$
	splysubrg.r	$$⊢\phi \to R\in \mathrm{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=\mathrm{SymGrp}\left(I\right)$$
2		splyval.p	$$⊢P={\mathrm{Base}}_S$$
3		splyval.m	$$⊢M={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
4		splyval.a	$$⊢A=\left(d\in P,f\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)\right)$$
5		splyval.i	$$⊢\phi \to I\in V$$
6		splysubrg.r	$$⊢\phi \to R\in \mathrm{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	$$⊢\left(f\in M⟼dAf\right)=\left(f\in M⟼dAf\right)$$
9	1 2 3 4 5	mplvrpmga	$$⊢\phi \to A\in \left(S\mathrm{GrpAct}M\right)$$
10		coeq2	$$⊢d=e\to x\circ d=x\circ e$$
11	10	fveq2d	$$⊢d=e\to f\left(x\circ d\right)=f\left(x\circ e\right)$$
12	11	mpteq2dv	$$⊢d=e\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ e\right)\right)$$
13		fveq1	$$⊢f=g\to f\left(x\circ e\right)=g\left(x\circ e\right)$$
14	13	mpteq2dv	$$⊢f=g\to \left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ e\right)\right)=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ e\right)\right)$$
15	12 14	cbvmpov	$$⊢\left(d\in P,f\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼f\left(x\circ d\right)\right)\right)=\left(e\in P,g\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ e\right)\right)\right)$$
16	4 15	eqtri	$$⊢A=\left(e\in P,g\in M⟼\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}⟼g\left(x\circ e\right)\right)\right)$$
17	5	adantr	$$⊢\left(\phi \wedge d\in P\right)\to I\in V$$
18		oveq2	$$⊢f=g\to dAf=dAg$$
19	18	cbvmptv	$$⊢\left(f\in M⟼dAf\right)=\left(g\in M⟼dAg\right)$$
20		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
21	6	adantr	$$⊢\left(\phi \wedge d\in P\right)\to R\in \mathrm{Ring}$$
22		simpr	$$⊢\left(\phi \wedge d\in P\right)\to d\in P$$
23	1 2 3 16 17 19 20 21 22	mplvrpmrhm	$$⊢\left(\phi \wedge d\in P\right)\to \left(f\in M⟼dAf\right)\in \left(\left(I\mathrm{mPoly}R\right)\mathrm{RingHom}\left(I\mathrm{mPoly}R\right)\right)$$
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 |-