Metamath Proof Explorer

Theorem esplympl

Description: Elementary symmetric polynomials are polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses esplympl.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
esplympl.i 
|- ( ph -> I e. Fin )
esplympl.r 
|- ( ph -> R e. Ring )
esplympl.k 
|- ( ph -> K e. NN0 )
esplympl.1 
|- M = ( Base ` ( I mPoly R ) )
Assertion esplympl 
|- ( ph -> ( ( I eSymPoly R ) ` K ) e. M )

Proof

Step Hyp Ref Expression
1 esplympl.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2 esplympl.i 
 |-  ( ph -> I e. Fin )
3 esplympl.r 
 |-  ( ph -> R e. Ring )
4 esplympl.k 
 |-  ( ph -> K e. NN0 )
5 esplympl.1 
 |-  M = ( Base ` ( I mPoly R ) )
6 fvexd 
 |-  ( ph -> ( Base ` R ) e. _V )
7 ovex 
 |-  ( NN0 ^m I ) e. _V
8 1 7 rabex2 
 |-  D e. _V
9 8 a1i 
 |-  ( ph -> D e. _V )
10 1 2 3 4 esplyfval 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) )
11 10 eqcomd 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) = ( ( I eSymPoly R ) ` K ) )
12 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
13 12 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
14 zringbas 
 |-  ZZ = ( Base ` ZZring )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 14 15 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
17 3 13 16 3syl 
 |-  ( ph -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
18 1 2 3 4 esplylem 
 |-  ( ph -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D )
19 indf 
 |-  ( ( D e. _V /\ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } )
20 9 18 19 syl2anc 
 |-  ( ph -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } )
21 0zd 
 |-  ( ph -> 0 e. ZZ )
22 1zzd 
 |-  ( ph -> 1 e. ZZ )
23 21 22 prssd 
 |-  ( ph -> { 0 , 1 } C_ ZZ )
24 20 23 fssd 
 |-  ( ph -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> ZZ )
25 17 24 fcod 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) : D --> ( Base ` R ) )
26 11 25 feq1dd 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) : D --> ( Base ` R ) )
27 6 9 26 elmapdd 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) e. ( ( Base ` R ) ^m D ) )
28 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
29 1 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
30 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
31 28 15 29 30 2 psrbas 
 |-  ( ph -> ( Base ` ( I mPwSer R ) ) = ( ( Base ` R ) ^m D ) )
32 27 31 eleqtrrd 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPwSer R ) ) )
33 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
34 zex 
 |-  ZZ e. _V
35 34 a1i 
 |-  ( ph -> ZZ e. _V )
36 indf1o 
 |-  ( I e. Fin -> ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) )
37 f1of 
 |-  ( ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
38 2 36 37 3syl 
 |-  ( ph -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
39 38 ffund 
 |-  ( ph -> Fun ( _Ind ` I ) )
40 2 pwexd 
 |-  ( ph -> ~P I e. _V )
41 ssrab2 
 |-  { c e. ~P I | ( # ` c ) = K } C_ ~P I
42 41 a1i 
 |-  ( ph -> { c e. ~P I | ( # ` c ) = K } C_ ~P I )
43 40 42 ssexd 
 |-  ( ph -> { c e. ~P I | ( # ` c ) = K } e. _V )
44 hashcl 
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
45 2 44 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
46 4 nn0zd 
 |-  ( ph -> K e. ZZ )
47 bccl 
 |-  ( ( ( # ` I ) e. NN0 /\ K e. ZZ ) -> ( ( # ` I ) _C K ) e. NN0 )
48 45 46 47 syl2anc 
 |-  ( ph -> ( ( # ` I ) _C K ) e. NN0 )
49 hashbc 
 |-  ( ( I e. Fin /\ K e. ZZ ) -> ( ( # ` I ) _C K ) = ( # ` { c e. ~P I | ( # ` c ) = K } ) )
50 2 46 49 syl2anc 
 |-  ( ph -> ( ( # ` I ) _C K ) = ( # ` { c e. ~P I | ( # ` c ) = K } ) )
51 50 eqcomd 
 |-  ( ph -> ( # ` { c e. ~P I | ( # ` c ) = K } ) = ( ( # ` I ) _C K ) )
52 hashvnfin 
 |-  ( ( { c e. ~P I | ( # ` c ) = K } e. _V /\ ( ( # ` I ) _C K ) e. NN0 ) -> ( ( # ` { c e. ~P I | ( # ` c ) = K } ) = ( ( # ` I ) _C K ) -> { c e. ~P I | ( # ` c ) = K } e. Fin ) )
53 52 imp 
 |-  ( ( ( { c e. ~P I | ( # ` c ) = K } e. _V /\ ( ( # ` I ) _C K ) e. NN0 ) /\ ( # ` { c e. ~P I | ( # ` c ) = K } ) = ( ( # ` I ) _C K ) ) -> { c e. ~P I | ( # ` c ) = K } e. Fin )
54 43 48 51 53 syl21anc 
 |-  ( ph -> { c e. ~P I | ( # ` c ) = K } e. Fin )
55 imafi 
 |-  ( ( Fun ( _Ind ` I ) /\ { c e. ~P I | ( # ` c ) = K } e. Fin ) -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) e. Fin )
56 39 54 55 syl2anc 
 |-  ( ph -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) e. Fin )
57 9 18 56 indfsd 
 |-  ( ph -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) finSupp 0 )
58 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
59 12 58 zrh0 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
60 3 59 syl 
 |-  ( ph -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
61 33 21 20 17 23 9 35 57 60 fsuppcor 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) finSupp ( 0g ` R ) )
62 10 61 eqbrtrd 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) finSupp ( 0g ` R ) )
63 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
64 63 28 30 58 5 mplelbas 
 |-  ( ( ( I eSymPoly R ) ` K ) e. M <-> ( ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPwSer R ) ) /\ ( ( I eSymPoly R ) ` K ) finSupp ( 0g ` R ) ) )
65 32 62 64 sylanbrc 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) e. M )