This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issply

Description: Conditions for being a symmetric polynomial. (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses issply.s 
|- S = ( SymGrp ` I )
issply.p 
|- P = ( Base ` S )
issply.m 
|- M = ( Base ` ( I mPoly R ) )
issply.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
issply.i 
|- ( ph -> I e. V )
issply.r 
|- ( ph -> R e. W )
issply.f 
|- ( ph -> F e. M )
issply.1 
|- ( ( ( ph /\ p e. P ) /\ x e. D ) -> ( F ` ( x o. p ) ) = ( F ` x ) )
Assertion issply 
|- ( ph -> F e. ( I SymPoly R ) )

Proof

Step Hyp Ref Expression
1 issply.s 
 |-  S = ( SymGrp ` I )
2 issply.p 
 |-  P = ( Base ` S )
3 issply.m 
 |-  M = ( Base ` ( I mPoly R ) )
4 issply.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
5 issply.i 
 |-  ( ph -> I e. V )
6 issply.r 
 |-  ( ph -> R e. W )
7 issply.f 
 |-  ( ph -> F e. M )
8 issply.1 
 |-  ( ( ( ph /\ p e. P ) /\ x e. D ) -> ( F ` ( x o. p ) ) = ( F ` x ) )
9 8 mpteq2dva 
 |-  ( ( ph /\ p e. P ) -> ( x e. D |-> ( F ` ( x o. p ) ) ) = ( x e. D |-> ( F ` x ) ) )
10 coeq2 
 |-  ( c = d -> ( y o. c ) = ( y o. d ) )
11 10 fveq2d 
 |-  ( c = d -> ( e ` ( y o. c ) ) = ( e ` ( y o. d ) ) )
12 11 mpteq2dv 
 |-  ( c = d -> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) = ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. d ) ) ) )
13 fveq1 
 |-  ( e = f -> ( e ` ( y o. d ) ) = ( f ` ( y o. d ) ) )
14 13 mpteq2dv 
 |-  ( e = f -> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. d ) ) ) = ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( y o. d ) ) ) )
15 12 14 cbvmpov 
 |-  ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) = ( d e. P , f e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( y o. d ) ) ) )
16 coeq1 
 |-  ( y = x -> ( y o. d ) = ( x o. d ) )
17 16 fveq2d 
 |-  ( y = x -> ( f ` ( y o. d ) ) = ( f ` ( x o. d ) ) )
18 17 cbvmptv 
 |-  ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( y o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) )
19 18 a1i 
 |-  ( ( d e. P /\ f e. M ) -> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( y o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) )
20 19 mpoeq3ia 
 |-  ( d e. P , f e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( y o. d ) ) ) ) = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) )
21 15 20 eqtri 
 |-  ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) )
22 21 a1i 
 |-  ( ( ph /\ p e. P ) -> ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) )
23 4 eqcomi 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = D
24 23 a1i 
 |-  ( ( d = p /\ f = F ) -> { h e. ( NN0 ^m I ) | h finSupp 0 } = D )
25 simpr 
 |-  ( ( d = p /\ f = F ) -> f = F )
26 coeq2 
 |-  ( d = p -> ( x o. d ) = ( x o. p ) )
27 26 adantr 
 |-  ( ( d = p /\ f = F ) -> ( x o. d ) = ( x o. p ) )
28 25 27 fveq12d 
 |-  ( ( d = p /\ f = F ) -> ( f ` ( x o. d ) ) = ( F ` ( x o. p ) ) )
29 24 28 mpteq12dv 
 |-  ( ( d = p /\ f = F ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. D |-> ( F ` ( x o. p ) ) ) )
30 29 adantl 
 |-  ( ( ( ph /\ p e. P ) /\ ( d = p /\ f = F ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. D |-> ( F ` ( x o. p ) ) ) )
31 simpr 
 |-  ( ( ph /\ p e. P ) -> p e. P )
32 7 adantr 
 |-  ( ( ph /\ p e. P ) -> F e. M )
33 ovex 
 |-  ( NN0 ^m I ) e. _V
34 4 33 rabex2 
 |-  D e. _V
35 34 a1i 
 |-  ( ( ph /\ p e. P ) -> D e. _V )
36 35 mptexd 
 |-  ( ( ph /\ p e. P ) -> ( x e. D |-> ( F ` ( x o. p ) ) ) e. _V )
37 22 30 31 32 36 ovmpod 
 |-  ( ( ph /\ p e. P ) -> ( p ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) F ) = ( x e. D |-> ( F ` ( x o. p ) ) ) )
38 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
39 eqid 
 |-  ( Base ` R ) = ( Base ` R )
40 4 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
41 38 39 3 40 32 mplelf 
 |-  ( ( ph /\ p e. P ) -> F : D --> ( Base ` R ) )
42 41 feqmptd 
 |-  ( ( ph /\ p e. P ) -> F = ( x e. D |-> ( F ` x ) ) )
43 9 37 42 3eqtr4d 
 |-  ( ( ph /\ p e. P ) -> ( p ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) F ) = F )
44 43 ralrimiva 
 |-  ( ph -> A. p e. P ( p ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) F ) = F )
45 1 2 3 21 5 mplvrpmga 
 |-  ( ph -> ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) e. ( S GrpAct M ) )
46 2 45 7 isfxp 
 |-  ( ph -> ( F e. ( M FixPts ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) ) <-> A. p e. P ( p ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) F ) = F ) )
47 44 46 mpbird 
 |-  ( ph -> F e. ( M FixPts ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) ) )
48 1 2 3 21 5 6 splyval 
 |-  ( ph -> ( I SymPoly R ) = ( M FixPts ( c e. P , e e. M |-> ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( e ` ( y o. c ) ) ) ) ) )
49 47 48 eleqtrrd 
 |-  ( ph -> F e. ( I SymPoly R ) )