Metamath Proof Explorer

Theorem esplysply

Description: The K -th elementary symmetric polynomial is symmetric. (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses esplyfv.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
esplyfv.i 
|- ( ph -> I e. Fin )
esplyfv.r 
|- ( ph -> R e. Ring )
esplyfv.k 
|- ( ph -> K e. ( 0 ... ( # ` I ) ) )
Assertion esplysply 
|- ( ph -> ( ( I eSymPoly R ) ` K ) e. ( I SymPoly R ) )

Proof

Step Hyp Ref Expression
1 esplyfv.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2 esplyfv.i 
 |-  ( ph -> I e. Fin )
3 esplyfv.r 
 |-  ( ph -> R e. Ring )
4 esplyfv.k 
 |-  ( ph -> K e. ( 0 ... ( # ` I ) ) )
5 eqid 
 |-  ( SymGrp ` I ) = ( SymGrp ` I )
6 eqid 
 |-  ( Base ` ( SymGrp ` I ) ) = ( Base ` ( SymGrp ` I ) )
7 eqid 
 |-  ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
8 elfznn0 
 |-  ( K e. ( 0 ... ( # ` I ) ) -> K e. NN0 )
9 4 8 syl 
 |-  ( ph -> K e. NN0 )
10 1 2 3 9 7 esplympl 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPoly R ) ) )
11 1 ssrab3 
 |-  D C_ ( NN0 ^m I )
12 11 a1i 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) -> D C_ ( NN0 ^m I ) )
13 12 sselda 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> x e. ( NN0 ^m I ) )
14 13 elmaprd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> x : I --> NN0 )
15 14 fdmd 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> dom x = I )
16 simplr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> p e. ( Base ` ( SymGrp ` I ) ) )
17 5 6 symgbasf1o 
 |-  ( p e. ( Base ` ( SymGrp ` I ) ) -> p : I -1-1-onto-> I )
18 16 17 syl 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> p : I -1-1-onto-> I )
19 f1ofo 
 |-  ( p : I -1-1-onto-> I -> p : I -onto-> I )
20 forn 
 |-  ( p : I -onto-> I -> ran p = I )
21 18 19 20 3syl 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ran p = I )
22 15 21 eqtr4d 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> dom x = ran p )
23 rncoeq 
 |-  ( dom x = ran p -> ran ( x o. p ) = ran x )
24 22 23 syl 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ran ( x o. p ) = ran x )
25 24 sseq1d 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ran ( x o. p ) C_ { 0 , 1 } <-> ran x C_ { 0 , 1 } ) )
26 f1ocnv 
 |-  ( p : I -1-1-onto-> I -> `' p : I -1-1-onto-> I )
27 f1of1 
 |-  ( `' p : I -1-1-onto-> I -> `' p : I -1-1-> I )
28 18 26 27 3syl 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> `' p : I -1-1-> I )
29 cnvimass 
 |-  ( `' x " ( NN0 \ { 0 } ) ) C_ dom x
30 29 14 fssdm 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( `' x " ( NN0 \ { 0 } ) ) C_ I )
31 2 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> I e. Fin )
32 28 30 31 hashimaf1 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( # ` ( `' p " ( `' x " ( NN0 \ { 0 } ) ) ) ) = ( # ` ( `' x " ( NN0 \ { 0 } ) ) ) )
33 c0ex 
 |-  0 e. _V
34 33 a1i 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> 0 e. _V )
35 simpr 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) -> p e. ( Base ` ( SymGrp ` I ) ) )
36 f1of 
 |-  ( p : I -1-1-onto-> I -> p : I --> I )
37 35 17 36 3syl 
 |-  ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) -> p : I --> I )
38 37 adantr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> p : I --> I )
39 14 38 fcod 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( x o. p ) : I --> NN0 )
40 fsuppeq 
 |-  ( ( I e. Fin /\ 0 e. _V ) -> ( ( x o. p ) : I --> NN0 -> ( ( x o. p ) supp 0 ) = ( `' ( x o. p ) " ( NN0 \ { 0 } ) ) ) )
41 40 imp 
 |-  ( ( ( I e. Fin /\ 0 e. _V ) /\ ( x o. p ) : I --> NN0 ) -> ( ( x o. p ) supp 0 ) = ( `' ( x o. p ) " ( NN0 \ { 0 } ) ) )
42 31 34 39 41 syl21anc 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( x o. p ) supp 0 ) = ( `' ( x o. p ) " ( NN0 \ { 0 } ) ) )
43 cnvco 
 |-  `' ( x o. p ) = ( `' p o. `' x )
44 43 imaeq1i 
 |-  ( `' ( x o. p ) " ( NN0 \ { 0 } ) ) = ( ( `' p o. `' x ) " ( NN0 \ { 0 } ) )
45 imaco 
 |-  ( ( `' p o. `' x ) " ( NN0 \ { 0 } ) ) = ( `' p " ( `' x " ( NN0 \ { 0 } ) ) )
46 44 45 eqtri 
 |-  ( `' ( x o. p ) " ( NN0 \ { 0 } ) ) = ( `' p " ( `' x " ( NN0 \ { 0 } ) ) )
47 42 46 eqtrdi 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( x o. p ) supp 0 ) = ( `' p " ( `' x " ( NN0 \ { 0 } ) ) ) )
48 47 fveq2d 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( # ` ( ( x o. p ) supp 0 ) ) = ( # ` ( `' p " ( `' x " ( NN0 \ { 0 } ) ) ) ) )
49 fsuppeq 
 |-  ( ( I e. Fin /\ 0 e. _V ) -> ( x : I --> NN0 -> ( x supp 0 ) = ( `' x " ( NN0 \ { 0 } ) ) ) )
50 49 imp 
 |-  ( ( ( I e. Fin /\ 0 e. _V ) /\ x : I --> NN0 ) -> ( x supp 0 ) = ( `' x " ( NN0 \ { 0 } ) ) )
51 31 34 14 50 syl21anc 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( x supp 0 ) = ( `' x " ( NN0 \ { 0 } ) ) )
52 51 fveq2d 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( # ` ( x supp 0 ) ) = ( # ` ( `' x " ( NN0 \ { 0 } ) ) ) )
53 32 48 52 3eqtr4d 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( # ` ( ( x o. p ) supp 0 ) ) = ( # ` ( x supp 0 ) ) )
54 53 eqeq1d 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( # ` ( ( x o. p ) supp 0 ) ) = K <-> ( # ` ( x supp 0 ) ) = K ) )
55 25 54 anbi12d 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( ran ( x o. p ) C_ { 0 , 1 } /\ ( # ` ( ( x o. p ) supp 0 ) ) = K ) <-> ( ran x C_ { 0 , 1 } /\ ( # ` ( x supp 0 ) ) = K ) ) )
56 55 ifbid 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> if ( ( ran ( x o. p ) C_ { 0 , 1 } /\ ( # ` ( ( x o. p ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( ran x C_ { 0 , 1 } /\ ( # ` ( x supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
57 3 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> R e. Ring )
58 4 ad2antrr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> K e. ( 0 ... ( # ` I ) ) )
59 simpr 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> x e. D )
60 59 1 eleqtrdi 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> x e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
61 5 6 31 16 60 mplvrpmlem 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( x o. p ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
62 61 1 eleqtrrdi 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( x o. p ) e. D )
63 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
64 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
65 1 31 57 58 62 63 64 esplyfv 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` ( x o. p ) ) = if ( ( ran ( x o. p ) C_ { 0 , 1 } /\ ( # ` ( ( x o. p ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
66 1 31 57 58 59 63 64 esplyfv 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` x ) = if ( ( ran x C_ { 0 , 1 } /\ ( # ` ( x supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
67 56 65 66 3eqtr4d 
 |-  ( ( ( ph /\ p e. ( Base ` ( SymGrp ` I ) ) ) /\ x e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` ( x o. p ) ) = ( ( ( I eSymPoly R ) ` K ) ` x ) )
68 5 6 7 1 2 3 10 67 issply 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) e. ( I SymPoly R ) )