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