Metamath Proof Explorer

Theorem esplyfval3

Description: Alternate expression for the value of the K -th elementary symmetric polynomial. (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses esplyfval3.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
esplyfval3.i 
|- ( ph -> I e. Fin )
esplyfval3.r 
|- ( ph -> R e. Ring )
esplyfval3.k 
|- ( ph -> K e. NN0 )
esplyfval3.1 
|- .0. = ( 0g ` R )
esplyfval3.2 
|- .1. = ( 1r ` R )
Assertion esplyfval3 
|- ( ph -> ( ( I eSymPoly R ) ` K ) = ( f e. D |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) )

Proof

Step Hyp Ref Expression
1 esplyfval3.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2 esplyfval3.i 
 |-  ( ph -> I e. Fin )
3 esplyfval3.r 
 |-  ( ph -> R e. Ring )
4 esplyfval3.k 
 |-  ( ph -> K e. NN0 )
5 esplyfval3.1 
 |-  .0. = ( 0g ` R )
6 esplyfval3.2 
 |-  .1. = ( 1r ` R )
7 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
8 7 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
9 zringbas 
 |-  ZZ = ( Base ` ZZring )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 9 10 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
12 3 8 11 3syl 
 |-  ( ph -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
13 12 ffnd 
 |-  ( ph -> ( ZRHom ` R ) Fn ZZ )
14 ovex 
 |-  ( NN0 ^m I ) e. _V
15 1 14 rabex2 
 |-  D e. _V
16 15 a1i 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> D e. _V )
17 2 adantr 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> I e. Fin )
18 3 adantr 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> R e. Ring )
19 4 adantr 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> K e. NN0 )
20 1 17 18 19 esplylem 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D )
21 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 } )
22 16 20 21 syl2anc 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } )
23 0zd 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> 0 e. ZZ )
24 1zzd 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> 1 e. ZZ )
25 23 24 prssd 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> { 0 , 1 } C_ ZZ )
26 22 25 fssd 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> ZZ )
27 fnfco 
 |-  ( ( ( ZRHom ` R ) Fn ZZ /\ ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> ZZ ) -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) Fn D )
28 13 26 27 syl2an2r 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) Fn D )
29 1 17 18 19 esplyfval 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) )
30 29 fneq1d 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( ( I eSymPoly R ) ` K ) Fn D <-> ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) Fn D ) )
31 28 30 mpbird 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) Fn D )
32 dffn5 
 |-  ( ( ( I eSymPoly R ) ` K ) Fn D <-> ( ( I eSymPoly R ) ` K ) = ( f e. D |-> ( ( ( I eSymPoly R ) ` K ) ` f ) ) )
33 31 32 sylib 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( f e. D |-> ( ( ( I eSymPoly R ) ` K ) ` f ) ) )
34 eqeq2 
 |-  ( if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) = if ( ran f C_ { 0 , 1 } , if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) , .0. ) -> ( ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) <-> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ran f C_ { 0 , 1 } , if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) , .0. ) ) )
35 eqeq2 
 |-  ( .0. = if ( ran f C_ { 0 , 1 } , if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) , .0. ) -> ( ( ( ( I eSymPoly R ) ` K ) ` f ) = .0. <-> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ran f C_ { 0 , 1 } , if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) , .0. ) ) )
36 17 adantr 
 |-  ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> I e. Fin )
37 36 adantr 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ ran f C_ { 0 , 1 } ) -> I e. Fin )
38 18 ad2antrr 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ ran f C_ { 0 , 1 } ) -> R e. Ring )
39 simpllr 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ ran f C_ { 0 , 1 } ) -> K e. ( 0 ... ( # ` I ) ) )
40 simplr 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ ran f C_ { 0 , 1 } ) -> f e. D )
41 simpr 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ ran f C_ { 0 , 1 } ) -> ran f C_ { 0 , 1 } )
42 1 37 38 39 40 5 6 41 esplyfv1 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ ran f C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) )
43 29 ad2antrr 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) )
44 43 fveq1d 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` f ) )
45 26 ad2antrr 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> ZZ )
46 simplr 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> f e. D )
47 45 46 fvco3d 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` f ) = ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` f ) ) )
48 20 ad2antrr 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D )
49 simpr 
 |-  ( ( ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = f ) -> ( ( _Ind ` I ) ` d ) = f )
50 36 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = f ) -> I e. Fin )
51 ssrab2 
 |-  { c e. ~P I | ( # ` c ) = K } C_ ~P I
52 51 a1i 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> { c e. ~P I | ( # ` c ) = K } C_ ~P I )
53 52 sselda 
 |-  ( ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) -> d e. ~P I )
54 53 adantr 
 |-  ( ( ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = f ) -> d e. ~P I )
55 54 elpwid 
 |-  ( ( ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = f ) -> d C_ I )
56 indf 
 |-  ( ( I e. Fin /\ d C_ I ) -> ( ( _Ind ` I ) ` d ) : I --> { 0 , 1 } )
57 50 55 56 syl2anc 
 |-  ( ( ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = f ) -> ( ( _Ind ` I ) ` d ) : I --> { 0 , 1 } )
58 49 57 feq1dd 
 |-  ( ( ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) /\ d e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` d ) = f ) -> f : I --> { 0 , 1 } )
59 indf1o 
 |-  ( I e. Fin -> ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) )
60 f1of 
 |-  ( ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
61 36 59 60 3syl 
 |-  ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
62 61 ffnd 
 |-  ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( _Ind ` I ) Fn ~P I )
63 51 a1i 
 |-  ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> { c e. ~P I | ( # ` c ) = K } C_ ~P I )
64 62 63 fvelimabd 
 |-  ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) <-> E. d e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` d ) = f ) )
65 64 biimpa 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> E. d e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` d ) = f )
66 58 65 r19.29a 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> f : I --> { 0 , 1 } )
67 66 frnd 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> ran f C_ { 0 , 1 } )
68 67 stoic1a 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> -. f e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) )
69 46 68 eldifd 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> f e. ( D \ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) )
70 ind0 
 |-  ( ( D e. _V /\ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D /\ f e. ( D \ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` f ) = 0 )
71 15 48 69 70 mp3an2i 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` f ) = 0 )
72 71 fveq2d 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` f ) ) = ( ( ZRHom ` R ) ` 0 ) )
73 7 5 zrh0 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 0 ) = .0. )
74 3 73 syl 
 |-  ( ph -> ( ( ZRHom ` R ) ` 0 ) = .0. )
75 74 ad3antrrr 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( ZRHom ` R ) ` 0 ) = .0. )
76 72 75 eqtrd 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` f ) ) = .0. )
77 44 47 76 3eqtrd 
 |-  ( ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) /\ -. ran f C_ { 0 , 1 } ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = .0. )
78 34 35 42 77 ifbothda 
 |-  ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ran f C_ { 0 , 1 } , if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) , .0. ) )
79 ifan 
 |-  if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) = if ( ran f C_ { 0 , 1 } , if ( ( # ` ( f supp 0 ) ) = K , .1. , .0. ) , .0. )
80 78 79 eqtr4di 
 |-  ( ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( ( ( I eSymPoly R ) ` K ) ` f ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) )
81 80 mpteq2dva 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( f e. D |-> ( ( ( I eSymPoly R ) ` K ) ` f ) ) = ( f e. D |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) )
82 33 81 eqtrd 
 |-  ( ( ph /\ K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( f e. D |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) )
83 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
84 1 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
85 eqid 
 |-  ( 0g ` ( I mPoly R ) ) = ( 0g ` ( I mPoly R ) )
86 3 ringgrpd 
 |-  ( ph -> R e. Grp )
87 83 84 5 85 2 86 mpl0 
 |-  ( ph -> ( 0g ` ( I mPoly R ) ) = ( D X. { .0. } ) )
88 87 adantr 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> ( 0g ` ( I mPoly R ) ) = ( D X. { .0. } ) )
89 2 adantr 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> I e. Fin )
90 3 adantr 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> R e. Ring )
91 4 adantr 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> K e. NN0 )
92 simpr 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> -. K e. ( 0 ... ( # ` I ) ) )
93 91 92 eldifd 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> K e. ( NN0 \ ( 0 ... ( # ` I ) ) ) )
94 1 89 90 93 85 esplyfval2 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( 0g ` ( I mPoly R ) ) )
95 breq1 
 |-  ( h = f -> ( h finSupp 0 <-> f finSupp 0 ) )
96 1 eleq2i 
 |-  ( f e. D <-> f e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
97 96 biimpi 
 |-  ( f e. D -> f e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
98 97 adantl 
 |-  ( ( ph /\ f e. D ) -> f e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
99 95 98 elrabrd 
 |-  ( ( ph /\ f e. D ) -> f finSupp 0 )
100 99 fsuppimpd 
 |-  ( ( ph /\ f e. D ) -> ( f supp 0 ) e. Fin )
101 hashcl 
 |-  ( ( f supp 0 ) e. Fin -> ( # ` ( f supp 0 ) ) e. NN0 )
102 100 101 syl 
 |-  ( ( ph /\ f e. D ) -> ( # ` ( f supp 0 ) ) e. NN0 )
103 102 nn0red 
 |-  ( ( ph /\ f e. D ) -> ( # ` ( f supp 0 ) ) e. RR )
104 103 adantlr 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( # ` ( f supp 0 ) ) e. RR )
105 hashcl 
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
106 2 105 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
107 106 nn0red 
 |-  ( ph -> ( # ` I ) e. RR )
108 107 ad2antrr 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( # ` I ) e. RR )
109 4 nn0red 
 |-  ( ph -> K e. RR )
110 109 ad2antrr 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> K e. RR )
111 suppssdm 
 |-  ( f supp 0 ) C_ dom f
112 2 adantr 
 |-  ( ( ph /\ f e. D ) -> I e. Fin )
113 nn0ex 
 |-  NN0 e. _V
114 113 a1i 
 |-  ( ( ph /\ f e. D ) -> NN0 e. _V )
115 1 ssrab3 
 |-  D C_ ( NN0 ^m I )
116 115 a1i 
 |-  ( ph -> D C_ ( NN0 ^m I ) )
117 116 sselda 
 |-  ( ( ph /\ f e. D ) -> f e. ( NN0 ^m I ) )
118 112 114 117 elmaprd 
 |-  ( ( ph /\ f e. D ) -> f : I --> NN0 )
119 111 118 fssdm 
 |-  ( ( ph /\ f e. D ) -> ( f supp 0 ) C_ I )
120 hashss 
 |-  ( ( I e. Fin /\ ( f supp 0 ) C_ I ) -> ( # ` ( f supp 0 ) ) <_ ( # ` I ) )
121 2 119 120 syl2an2r 
 |-  ( ( ph /\ f e. D ) -> ( # ` ( f supp 0 ) ) <_ ( # ` I ) )
122 121 adantlr 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( # ` ( f supp 0 ) ) <_ ( # ` I ) )
123 106 nn0zd 
 |-  ( ph -> ( # ` I ) e. ZZ )
124 123 ad2antrr 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( # ` I ) e. ZZ )
125 nn0diffz0 
 |-  ( ( # ` I ) e. NN0 -> ( NN0 \ ( 0 ... ( # ` I ) ) ) = ( ZZ>= ` ( ( # ` I ) + 1 ) ) )
126 89 105 125 3syl 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> ( NN0 \ ( 0 ... ( # ` I ) ) ) = ( ZZ>= ` ( ( # ` I ) + 1 ) ) )
127 93 126 eleqtrd 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> K e. ( ZZ>= ` ( ( # ` I ) + 1 ) ) )
128 127 adantr 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> K e. ( ZZ>= ` ( ( # ` I ) + 1 ) ) )
129 eluzp1l 
 |-  ( ( ( # ` I ) e. ZZ /\ K e. ( ZZ>= ` ( ( # ` I ) + 1 ) ) ) -> ( # ` I ) < K )
130 124 128 129 syl2anc 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( # ` I ) < K )
131 104 108 110 122 130 lelttrd 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( # ` ( f supp 0 ) ) < K )
132 104 131 ltned 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> ( # ` ( f supp 0 ) ) =/= K )
133 132 neneqd 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> -. ( # ` ( f supp 0 ) ) = K )
134 133 intnand 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> -. ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) )
135 134 iffalsed 
 |-  ( ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) /\ f e. D ) -> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) = .0. )
136 135 mpteq2dva 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> ( f e. D |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) = ( f e. D |-> .0. ) )
137 fconstmpt 
 |-  ( D X. { .0. } ) = ( f e. D |-> .0. )
138 136 137 eqtr4di 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> ( f e. D |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) = ( D X. { .0. } ) )
139 88 94 138 3eqtr4d 
 |-  ( ( ph /\ -. K e. ( 0 ... ( # ` I ) ) ) -> ( ( I eSymPoly R ) ` K ) = ( f e. D |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) )
140 82 139 pm2.61dan 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) = ( f e. D |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , .1. , .0. ) ) )