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 = SymGrp (I)$
	splyval.p	$⊢ P = {Base}_{S}$
	splyval.m	$⊢ M = {Base}_{(I mPoly R)}$
	splyval.a	$⊢ A = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
	splyval.i	$⊢ φ \to I \in V$
	splyval.r	$⊢ φ \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 = SymGrp (I)$
2		splyval.p	$⊢ P = {Base}_{S}$
3		splyval.m	$⊢ M = {Base}_{(I mPoly R)}$
4		splyval.a	$⊢ A = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
5		splyval.i	$⊢ φ \to I \in V$
6		splyval.r	$⊢ φ \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	$⊢ (i = I \land r = R) \to i mPoly r = I mPoly R$
10	9	fveq2d	$⊢ (i = I \land r = R) \to {Base}_{(i mPoly r)} = {Base}_{(I mPoly R)}$
11	10 3	eqtr4di	$⊢ (i = I \land r = R) \to {Base}_{(i mPoly r)} = M$
12		fveq2	$⊢ i = I \to SymGrp (i) = SymGrp (I)$
13	12	adantr	$⊢ (i = I \land r = R) \to SymGrp (i) = SymGrp (I)$
14	13 1	eqtr4di	$⊢ (i = I \land r = R) \to SymGrp (i) = S$
15	14	fveq2d	$⊢ (i = I \land r = R) \to {Base}_{SymGrp (i)} = {Base}_{S}$
16	15 2	eqtr4di	$⊢ (i = I \land r = R) \to {Base}_{SymGrp (i)} = P$
17		oveq2	$⊢ i = I \to {ℕ_{0}}^{i} = {ℕ_{0}}^{I}$
18	17	adantr	$⊢ (i = I \land r = R) \to {ℕ_{0}}^{i} = {ℕ_{0}}^{I}$
19	18	rabeqdv	$⊢ (i = I \land r = R) \to \{h \in ({ℕ_{0}}^{i}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
20	19	mpteq1d	$⊢ (i = I \land r = R) \to (x \in \{h \in ({ℕ_{0}}^{i}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d))$
21	16 11 20	mpoeq123dv	$⊢ (i = I \land r = R) \to (d \in {Base}_{SymGrp (i)}, f \in {Base}_{(i mPoly r)} ⟼ (x \in \{h \in ({ℕ_{0}}^{i}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d))) = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
22	21 4	eqtr4di	$⊢ (i = I \land r = R) \to (d \in {Base}_{SymGrp (i)}, f \in {Base}_{(i mPoly r)} ⟼ (x \in \{h \in ({ℕ_{0}}^{i}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d))) = 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	$⊢ φ \to I \in V$
26	6	elexd	$⊢ φ \to R \in 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 \|-

Metamath Proof Explorer

Theorem splyval

Proof