Metamath Proof Explorer

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 = ( SymGrp ` I )
splyval.p 
|- P = ( Base ` S )
splyval.m 
|- M = ( Base ` ( I mPoly R ) )
splyval.a 
|- A = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) )
splyval.i 
|- ( ph -> I e. V )
splyval.r 
|- ( ph -> R e. W )
Assertion splyval 
|- ( ph -> ( I SymPoly R ) = ( M FixPts A ) )

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 e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) )
5 splyval.i 
 |-  ( ph -> I e. V )
6 splyval.r 
 |-  ( ph -> R e. W )
7 df-sply 
 |-  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 ) ) ) ) ) )
8 7 a1i 
 |-  ( 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 ) ) ) ) ) ) )
9 oveq12 
 |-  ( ( i = I /\ r = R ) -> ( i mPoly r ) = ( I mPoly R ) )
10 9 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( i mPoly r ) ) = ( Base ` ( I mPoly R ) ) )
11 10 3 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( i mPoly r ) ) = M )
12 fveq2 
 |-  ( i = I -> ( SymGrp ` i ) = ( SymGrp ` I ) )
13 12 adantr 
 |-  ( ( i = I /\ r = R ) -> ( SymGrp ` i ) = ( SymGrp ` I ) )
14 13 1 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( SymGrp ` i ) = S )
15 14 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( SymGrp ` i ) ) = ( Base ` S ) )
16 15 2 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( SymGrp ` i ) ) = P )
17 oveq2 
 |-  ( i = I -> ( NN0 ^m i ) = ( NN0 ^m I ) )
18 17 adantr 
 |-  ( ( i = I /\ r = R ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
19 18 rabeqdv 
 |-  ( ( i = I /\ r = R ) -> { h e. ( NN0 ^m i ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 } )
20 19 mpteq1d 
 |-  ( ( i = I /\ r = R ) -> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) )
21 16 11 20 mpoeq123dv 
 |-  ( ( i = I /\ r = R ) -> ( 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 ) ) ) ) = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) )
22 21 4 eqtr4di 
 |-  ( ( i = I /\ r = R ) -> ( 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 ) ) ) ) = A )
23 11 22 oveq12d 
 |-  ( ( 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 ) )
24 23 adantl 
 |-  ( ( 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 ) )
25 5 elexd 
 |-  ( ph -> I e. _V )
26 6 elexd 
 |-  ( ph -> R e. _V )
27 ovexd 
 |-  ( ph -> ( M FixPts A ) e. _V )
28 8 24 25 26 27 ovmpod 
 |-  ( ph -> ( I SymPoly R ) = ( M FixPts A ) )