Theorem splyval

Description: The symmetric polynomials for a given index I of variables and base ring R . These are the fixed points of the action A which permutes variables. (Contributed by Thierry Arnoux, 11-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$$
	splyval.r	$$⊢\phi \to R\in W$$
Assertion	splyval	Could not format assertion : No typesetting found for |- ( ph -> ( I SymPoly R ) = ( M FixPts A ) ) 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		splyval.r	$$⊢\phi \to R\in W$$
7		df-sply	Could not format SymPoly = ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) : No typesetting found for |- SymPoly = ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) with typecode |-
8	7	a1i	Could not format ( ph -> SymPoly = ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) ) : No typesetting found for |- ( ph -> SymPoly = ( i e. _V , r e. _V |-> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) ) ) with typecode |-
9		oveq12	$$⊢\left(i=I\wedge r=R\right)\to i\mathrm{mPoly}r=I\mathrm{mPoly}R$$
10	9	fveq2d	$$⊢\left(i=I\wedge r=R\right)\to {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
11	10 3	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}=M$$
12		fveq2	$$⊢i=I\to \mathrm{SymGrp}\left(i\right)=\mathrm{SymGrp}\left(I\right)$$
13	12	adantr	$$⊢\left(i=I\wedge r=R\right)\to \mathrm{SymGrp}\left(i\right)=\mathrm{SymGrp}\left(I\right)$$
14	13 1	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to \mathrm{SymGrp}\left(i\right)=S$$
15	14	fveq2d	$$⊢\left(i=I\wedge r=R\right)\to {\mathrm{Base}}_{\mathrm{SymGrp}\left(i\right)}={\mathrm{Base}}_S$$
16	15 2	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to {\mathrm{Base}}_{\mathrm{SymGrp}\left(i\right)}=P$$
17		oveq2	$$⊢i=I\to {{\mathbb{N}}_0}^i={{\mathbb{N}}_0}^I$$
18	17	adantr	$$⊢\left(i=I\wedge r=R\right)\to {{\mathbb{N}}_0}^i={{\mathbb{N}}_0}^I$$
19	18	rabeqdv	$$⊢\left(i=I\wedge r=R\right)\to \left\{h\in \left({{\mathbb{N}}_0}^i\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
20	19	mpteq1d	$$⊢\left(i=I\wedge r=R\right)\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 d\right)\right)$$
21	16 11 20	mpoeq123dv	$$⊢\left(i=I\wedge r=R\right)\to \left(d\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(i\right)},f\in {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}⟼\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(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)$$
22	21 4	eqtr4di	$$⊢\left(i=I\wedge r=R\right)\to \left(d\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(i\right)},f\in {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}⟼\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)=A$$
23	11 22	oveq12d	Could not format ( ( i = I /\ r = R ) -> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) = ( M FixPts A ) ) : No typesetting found for |- ( ( i = I /\ r = R ) -> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) = ( M FixPts A ) ) with typecode |-
24	23	adantl	Could not format ( ( ph /\ ( i = I /\ r = R ) ) -> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) = ( M FixPts A ) ) : No typesetting found for |- ( ( ph /\ ( i = I /\ r = R ) ) -> ( ( Base ` ( i mPoly r ) ) FixPts ( d e. ( Base ` ( SymGrp ` i ) ) , f e. ( Base ` ( i mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) ) = ( M FixPts A ) ) with typecode |-
25	5	elexd	$$⊢\phi \to I\in \mathrm{V}$$
26	6	elexd	$$⊢\phi \to R\in \mathrm{V}$$
27		ovexd	Could not format ( ph -> ( M FixPts A ) e. _V ) : No typesetting found for |- ( ph -> ( M FixPts A ) e. _V ) with typecode |-
28	8 24 25 26 27	ovmpod	Could not format ( ph -> ( I SymPoly R ) = ( M FixPts A ) ) : No typesetting found for |- ( ph -> ( I SymPoly R ) = ( M FixPts A ) ) with typecode |-