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

Metamath Proof Explorer

Theorem esplyfval0

Description: The 0 -th elementary symmetric polynomial is the constant 1 . (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses esplyfval0.i 
|- ( ph -> I e. V )
esplyfval0.r 
|- ( ph -> R e. Ring )
esplyfval0.0 
|- U = ( 1r ` ( I mPoly R ) )
Assertion esplyfval0 
|- ( ph -> ( ( I eSymPoly R ) ` 0 ) = U )

Proof

Step Hyp Ref Expression
1 esplyfval0.i 
 |-  ( ph -> I e. V )
2 esplyfval0.r 
 |-  ( ph -> R e. Ring )
3 esplyfval0.0 
 |-  U = ( 1r ` ( I mPoly R ) )
4 eqid 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 }
5 4 1 2 esplyval 
 |-  ( ph -> ( I eSymPoly R ) = ( k e. NN0 |-> ( ( ZRHom ` R ) o. ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = k } ) ) ) ) )
6 eqeq2 
 |-  ( k = 0 -> ( ( # ` c ) = k <-> ( # ` c ) = 0 ) )
7 6 rabbidv 
 |-  ( k = 0 -> { c e. ~P I | ( # ` c ) = k } = { c e. ~P I | ( # ` c ) = 0 } )
8 7 imaeq2d 
 |-  ( k = 0 -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = k } ) = ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = 0 } ) )
9 8 fveq2d 
 |-  ( k = 0 -> ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = k } ) ) = ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = 0 } ) ) )
10 9 coeq2d 
 |-  ( k = 0 -> ( ( ZRHom ` R ) o. ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = k } ) ) ) = ( ( ZRHom ` R ) o. ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = 0 } ) ) ) )
11 fvif 
 |-  ( ( ZRHom ` R ) ` if ( f = ( I X. { 0 } ) , 1 , 0 ) ) = if ( f = ( I X. { 0 } ) , ( ( ZRHom ` R ) ` 1 ) , ( ( ZRHom ` R ) ` 0 ) )
12 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
13 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
14 12 13 zrh1 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 1 ) = ( 1r ` R ) )
15 2 14 syl 
 |-  ( ph -> ( ( ZRHom ` R ) ` 1 ) = ( 1r ` R ) )
16 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
17 12 16 zrh0 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
18 2 17 syl 
 |-  ( ph -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
19 15 18 ifeq12d 
 |-  ( ph -> if ( f = ( I X. { 0 } ) , ( ( ZRHom ` R ) ` 1 ) , ( ( ZRHom ` R ) ` 0 ) ) = if ( f = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) )
20 19 adantr 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> if ( f = ( I X. { 0 } ) , ( ( ZRHom ` R ) ` 1 ) , ( ( ZRHom ` R ) ` 0 ) ) = if ( f = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) )
21 11 20 eqtrid 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( ZRHom ` R ) ` if ( f = ( I X. { 0 } ) , 1 , 0 ) ) = if ( f = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) )
22 21 mpteq2dva 
 |-  ( ph -> ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( ZRHom ` R ) ` if ( f = ( I X. { 0 } ) , 1 , 0 ) ) ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( f = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
23 1zzd 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> 1 e. ZZ )
24 0zd 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> 0 e. ZZ )
25 23 24 ifcld 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> if ( f = ( I X. { 0 } ) , 1 , 0 ) e. ZZ )
26 fveqeq2 
 |-  ( c = (/) -> ( ( # ` c ) = 0 <-> ( # ` (/) ) = 0 ) )
27 0elpw 
 |-  (/) e. ~P I
28 27 a1i 
 |-  ( ph -> (/) e. ~P I )
29 hash0 
 |-  ( # ` (/) ) = 0
30 29 a1i 
 |-  ( ph -> ( # ` (/) ) = 0 )
31 hasheq0 
 |-  ( c e. ~P I -> ( ( # ` c ) = 0 <-> c = (/) ) )
32 31 biimpa 
 |-  ( ( c e. ~P I /\ ( # ` c ) = 0 ) -> c = (/) )
33 32 adantll 
 |-  ( ( ( ph /\ c e. ~P I ) /\ ( # ` c ) = 0 ) -> c = (/) )
34 26 28 30 33 rabeqsnd 
 |-  ( ph -> { c e. ~P I | ( # ` c ) = 0 } = { (/) } )
35 34 imaeq2d 
 |-  ( ph -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = 0 } ) = ( ( _Ind ` I ) " { (/) } ) )
36 indf1o 
 |-  ( I e. V -> ( _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 1 36 37 3syl 
 |-  ( ph -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
39 38 ffnd 
 |-  ( ph -> ( _Ind ` I ) Fn ~P I )
40 39 28 fnimasnd 
 |-  ( ph -> ( ( _Ind ` I ) " { (/) } ) = { ( ( _Ind ` I ) ` (/) ) } )
41 indconst0 
 |-  ( I e. V -> ( ( _Ind ` I ) ` (/) ) = ( I X. { 0 } ) )
42 1 41 syl 
 |-  ( ph -> ( ( _Ind ` I ) ` (/) ) = ( I X. { 0 } ) )
43 42 sneqd 
 |-  ( ph -> { ( ( _Ind ` I ) ` (/) ) } = { ( I X. { 0 } ) } )
44 35 40 43 3eqtrd 
 |-  ( ph -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = 0 } ) = { ( I X. { 0 } ) } )
45 44 fveq2d 
 |-  ( ph -> ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = 0 } ) ) = ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` { ( I X. { 0 } ) } ) )
46 ovex 
 |-  ( NN0 ^m I ) e. _V
47 46 rabex 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V
48 breq1 
 |-  ( h = ( I X. { 0 } ) -> ( h finSupp 0 <-> ( I X. { 0 } ) finSupp 0 ) )
49 nn0ex 
 |-  NN0 e. _V
50 49 a1i 
 |-  ( ph -> NN0 e. _V )
51 c0ex 
 |-  0 e. _V
52 51 fconst 
 |-  ( I X. { 0 } ) : I --> { 0 }
53 52 a1i 
 |-  ( ph -> ( I X. { 0 } ) : I --> { 0 } )
54 0nn0 
 |-  0 e. NN0
55 54 a1i 
 |-  ( ph -> 0 e. NN0 )
56 55 snssd 
 |-  ( ph -> { 0 } C_ NN0 )
57 53 56 fssd 
 |-  ( ph -> ( I X. { 0 } ) : I --> NN0 )
58 50 1 57 elmapdd 
 |-  ( ph -> ( I X. { 0 } ) e. ( NN0 ^m I ) )
59 0zd 
 |-  ( ph -> 0 e. ZZ )
60 1 59 fczfsuppd 
 |-  ( ph -> ( I X. { 0 } ) finSupp 0 )
61 48 58 60 elrabd 
 |-  ( ph -> ( I X. { 0 } ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
62 indsn 
 |-  ( ( { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V /\ ( I X. { 0 } ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` { ( I X. { 0 } ) } ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( f = ( I X. { 0 } ) , 1 , 0 ) ) )
63 47 61 62 sylancr 
 |-  ( ph -> ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` { ( I X. { 0 } ) } ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( f = ( I X. { 0 } ) , 1 , 0 ) ) )
64 45 63 eqtrd 
 |-  ( ph -> ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = 0 } ) ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( f = ( I X. { 0 } ) , 1 , 0 ) ) )
65 12 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
66 zringbas 
 |-  ZZ = ( Base ` ZZring )
67 eqid 
 |-  ( Base ` R ) = ( Base ` R )
68 66 67 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
69 2 65 68 3syl 
 |-  ( ph -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
70 69 feqmptd 
 |-  ( ph -> ( ZRHom ` R ) = ( z e. ZZ |-> ( ( ZRHom ` R ) ` z ) ) )
71 fveq2 
 |-  ( z = if ( f = ( I X. { 0 } ) , 1 , 0 ) -> ( ( ZRHom ` R ) ` z ) = ( ( ZRHom ` R ) ` if ( f = ( I X. { 0 } ) , 1 , 0 ) ) )
72 25 64 70 71 fmptco 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = 0 } ) ) ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( ZRHom ` R ) ` if ( f = ( I X. { 0 } ) , 1 , 0 ) ) ) )
73 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
74 4 psrbasfsupp 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
75 73 74 16 13 3 1 2 mpl1 
 |-  ( ph -> U = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( f = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
76 22 72 75 3eqtr4d 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = 0 } ) ) ) = U )
77 10 76 sylan9eqr 
 |-  ( ( ph /\ k = 0 ) -> ( ( ZRHom ` R ) o. ( ( _Ind ` { h e. ( NN0 ^m I ) | h finSupp 0 } ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = k } ) ) ) = U )
78 3 fvexi 
 |-  U e. _V
79 78 a1i 
 |-  ( ph -> U e. _V )
80 5 77 55 79 fvmptd 
 |-  ( ph -> ( ( I eSymPoly R ) ` 0 ) = U )