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 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 )
splysubrg.r 
|- ( ph -> R e. Ring )
Assertion splysubrg 
|- ( ph -> ( I SymPoly R ) e. ( SubRing ` ( I mPoly R ) ) )

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 splysubrg.r 
 |-  ( ph -> R e. Ring )
7 1 2 3 4 5 6 splyval 
 |-  ( ph -> ( I SymPoly R ) = ( M FixPts A ) )
8 eqid 
 |-  ( f e. M |-> ( d A f ) ) = ( f e. M |-> ( d A f ) )
9 1 2 3 4 5 mplvrpmga 
 |-  ( ph -> A e. ( S GrpAct M ) )
10 coeq2 
 |-  ( d = e -> ( x o. d ) = ( x o. e ) )
11 10 fveq2d 
 |-  ( d = e -> ( f ` ( x o. d ) ) = ( f ` ( x o. e ) ) )
12 11 mpteq2dv 
 |-  ( d = e -> ( 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. e ) ) ) )
13 fveq1 
 |-  ( f = g -> ( f ` ( x o. e ) ) = ( g ` ( x o. e ) ) )
14 13 mpteq2dv 
 |-  ( f = g -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. e ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( g ` ( x o. e ) ) ) )
15 12 14 cbvmpov 
 |-  ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) = ( e e. P , g e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( g ` ( x o. e ) ) ) )
16 4 15 eqtri 
 |-  A = ( e e. P , g e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( g ` ( x o. e ) ) ) )
17 5 adantr 
 |-  ( ( ph /\ d e. P ) -> I e. V )
18 oveq2 
 |-  ( f = g -> ( d A f ) = ( d A g ) )
19 18 cbvmptv 
 |-  ( f e. M |-> ( d A f ) ) = ( g e. M |-> ( d A g ) )
20 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
21 6 adantr 
 |-  ( ( ph /\ d e. P ) -> R e. Ring )
22 simpr 
 |-  ( ( ph /\ d e. P ) -> d e. P )
23 1 2 3 16 17 19 20 21 22 mplvrpmrhm 
 |-  ( ( ph /\ d e. P ) -> ( f e. M |-> ( d A f ) ) e. ( ( I mPoly R ) RingHom ( I mPoly R ) ) )
24 2 3 8 9 23 fxpsubrg 
 |-  ( ph -> ( M FixPts A ) e. ( SubRing ` ( I mPoly R ) ) )
25 7 24 eqeltrd 
 |-  ( ph -> ( I SymPoly R ) e. ( SubRing ` ( I mPoly R ) ) )