Metamath Proof Explorer

Theorem esplymhp

Description: The K -th elementary symmetric polynomial is homogeneous of degree K . (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 )
esplymhp.1 
|- H = ( I mHomP R )
Assertion esplymhp 
|- ( ph -> ( ( I eSymPoly R ) ` K ) e. ( H ` K ) )

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 esplymhp.1 
 |-  H = ( I mHomP R )
6 2 ad2antrr 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> I e. Fin )
7 simpr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( _Ind ` I ) ` b ) = d )
8 6 ad2antrr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> I e. Fin )
9 ssrab2 
 |-  { c e. ~P I | ( # ` c ) = K } C_ ~P I
10 9 a1i 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> { c e. ~P I | ( # ` c ) = K } C_ ~P I )
11 10 sselda 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) -> b e. ~P I )
12 11 elpwid 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) -> b C_ I )
13 12 adantr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> b C_ I )
14 indf 
 |-  ( ( I e. Fin /\ b C_ I ) -> ( ( _Ind ` I ) ` b ) : I --> { 0 , 1 } )
15 8 13 14 syl2anc 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( _Ind ` I ) ` b ) : I --> { 0 , 1 } )
16 7 15 feq1dd 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> d : I --> { 0 , 1 } )
17 indf1o 
 |-  ( I e. Fin -> ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) )
18 f1of 
 |-  ( ( _Ind ` I ) : ~P I -1-1-onto-> ( { 0 , 1 } ^m I ) -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
19 2 17 18 3syl 
 |-  ( ph -> ( _Ind ` I ) : ~P I --> ( { 0 , 1 } ^m I ) )
20 19 ffund 
 |-  ( ph -> Fun ( _Ind ` I ) )
21 20 ad2antrr 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> Fun ( _Ind ` I ) )
22 ovex 
 |-  ( NN0 ^m I ) e. _V
23 1 ssrab3 
 |-  D C_ ( NN0 ^m I )
24 22 23 ssexi 
 |-  D e. _V
25 24 a1i 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> D e. _V )
26 3 ad2antrr 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> R e. Ring )
27 4 ad2antrr 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> K e. NN0 )
28 1 6 26 27 esplylem 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D )
29 simplr 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d e. D )
30 simpr 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) )
31 30 neneqd 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> -. ( ( ( I eSymPoly R ) ` K ) ` d ) = ( 0g ` R ) )
32 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 } )
33 25 28 32 syl2anc 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } )
34 33 adantr 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) : D --> { 0 , 1 } )
35 29 adantr 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> d e. D )
36 34 35 ffvelcdmd 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) e. { 0 , 1 } )
37 simpr 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 )
38 elprn2 
 |-  ( ( ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) e. { 0 , 1 } /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) = 0 )
39 36 37 38 syl2anc 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) = 0 )
40 39 fveq2d 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) = ( ( ZRHom ` R ) ` 0 ) )
41 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
42 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
43 41 42 zrh0 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
44 3 43 syl 
 |-  ( ph -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
45 44 ad3antrrr 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` 0 ) = ( 0g ` R ) )
46 40 45 eqtrd 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) = ( 0g ` R ) )
47 1 2 3 4 esplyfval 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) )
48 47 ad2antrr 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( I eSymPoly R ) ` K ) = ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) )
49 48 fveq1d 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) = ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` d ) )
50 33 29 fvco3d 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( ZRHom ` R ) o. ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ) ` d ) = ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) )
51 49 50 eqtrd 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) = ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) )
52 51 30 eqnetrrd 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) =/= ( 0g ` R ) )
53 52 adantr 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ZRHom ` R ) ` ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) ) =/= ( 0g ` R ) )
54 46 53 pm2.21ddne 
 |-  ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 ) -> ( ( ( I eSymPoly R ) ` K ) ` d ) = ( 0g ` R ) )
55 31 54 mtand 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> -. ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 )
56 nne 
 |-  ( -. ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) =/= 1 <-> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) = 1 )
57 55 56 sylib 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) = 1 )
58 ind1a 
 |-  ( ( D e. _V /\ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D /\ d e. D ) -> ( ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) = 1 <-> d e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) )
59 58 biimpa 
 |-  ( ( ( D e. _V /\ ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) C_ D /\ d e. D ) /\ ( ( ( _Ind ` D ) ` ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) ` d ) = 1 ) -> d e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) )
60 25 28 29 57 59 syl31anc 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) )
61 fvelima 
 |-  ( ( Fun ( _Ind ` I ) /\ d e. ( ( _Ind ` I ) " { c e. ~P I | ( # ` c ) = K } ) ) -> E. b e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` b ) = d )
62 21 60 61 syl2anc 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> E. b e. { c e. ~P I | ( # ` c ) = K } ( ( _Ind ` I ) ` b ) = d )
63 16 62 r19.29a 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d : I --> { 0 , 1 } )
64 6 63 indfsid 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d = ( ( _Ind ` I ) ` ( d supp 0 ) ) )
65 64 oveq2d 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum d ) = ( CCfld gsum ( ( _Ind ` I ) ` ( d supp 0 ) ) ) )
66 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
67 66 a1i 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> NN0 e. ( SubMnd ` CCfld ) )
68 23 a1i 
 |-  ( ph -> D C_ ( NN0 ^m I ) )
69 68 sselda 
 |-  ( ( ph /\ d e. D ) -> d e. ( NN0 ^m I ) )
70 69 adantr 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d e. ( NN0 ^m I ) )
71 6 67 70 elmaprd 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> d : I --> NN0 )
72 eqid 
 |-  ( CCfld |`s NN0 ) = ( CCfld |`s NN0 )
73 6 67 71 72 gsumsubm 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum d ) = ( ( CCfld |`s NN0 ) gsum d ) )
74 suppssdm 
 |-  ( d supp 0 ) C_ dom d
75 2 adantr 
 |-  ( ( ph /\ d e. D ) -> I e. Fin )
76 nn0ex 
 |-  NN0 e. _V
77 76 a1i 
 |-  ( ( ph /\ d e. D ) -> NN0 e. _V )
78 75 77 69 elmaprd 
 |-  ( ( ph /\ d e. D ) -> d : I --> NN0 )
79 78 fdmd 
 |-  ( ( ph /\ d e. D ) -> dom d = I )
80 79 adantr 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> dom d = I )
81 74 80 sseqtrid 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( d supp 0 ) C_ I )
82 6 81 ssfid 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( d supp 0 ) e. Fin )
83 6 81 82 gsumind 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum ( ( _Ind ` I ) ` ( d supp 0 ) ) ) = ( # ` ( d supp 0 ) ) )
84 7 oveq1d 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( ( _Ind ` I ) ` b ) supp 0 ) = ( d supp 0 ) )
85 indsupp 
 |-  ( ( I e. Fin /\ b C_ I ) -> ( ( ( _Ind ` I ) ` b ) supp 0 ) = b )
86 8 13 85 syl2anc 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( ( ( _Ind ` I ) ` b ) supp 0 ) = b )
87 84 86 eqtr3d 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( d supp 0 ) = b )
88 87 fveq2d 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( # ` ( d supp 0 ) ) = ( # ` b ) )
89 fveqeq2 
 |-  ( c = b -> ( ( # ` c ) = K <-> ( # ` b ) = K ) )
90 simplr 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> b e. { c e. ~P I | ( # ` c ) = K } )
91 89 90 elrabrd 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( # ` b ) = K )
92 88 91 eqtrd 
 |-  ( ( ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) /\ b e. { c e. ~P I | ( # ` c ) = K } ) /\ ( ( _Ind ` I ) ` b ) = d ) -> ( # ` ( d supp 0 ) ) = K )
93 92 62 r19.29a 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( # ` ( d supp 0 ) ) = K )
94 83 93 eqtrd 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( CCfld gsum ( ( _Ind ` I ) ` ( d supp 0 ) ) ) = K )
95 65 73 94 3eqtr3d 
 |-  ( ( ( ph /\ d e. D ) /\ ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) ) -> ( ( CCfld |`s NN0 ) gsum d ) = K )
96 95 ex 
 |-  ( ( ph /\ d e. D ) -> ( ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) )
97 96 ralrimiva 
 |-  ( ph -> A. d e. D ( ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) )
98 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
99 eqid 
 |-  ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
100 1 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
101 1 2 3 4 99 esplympl 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) e. ( Base ` ( I mPoly R ) ) )
102 5 98 99 42 100 4 101 ismhp3 
 |-  ( ph -> ( ( ( I eSymPoly R ) ` K ) e. ( H ` K ) <-> A. d e. D ( ( ( ( I eSymPoly R ) ` K ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = K ) ) )
103 97 102 mpbird 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) e. ( H ` K ) )