Metamath Proof Explorer

Theorem esplyfval1

Description: The first elementary symmetric polynomial is the sum of all variables. (Contributed by Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses esplyfval1.w 
|- W = ( I mPoly R )
esplyfval1.v 
|- V = ( I mVar R )
esplyfval1.e 
|- E = ( I eSymPoly R )
esplyfval1.i 
|- ( ph -> I e. Fin )
esplyfval1.r 
|- ( ph -> R e. Ring )
Assertion esplyfval1 
|- ( ph -> ( E ` 1 ) = ( W gsum V ) )

Proof

Step Hyp Ref Expression
1 esplyfval1.w 
 |-  W = ( I mPoly R )
2 esplyfval1.v 
 |-  V = ( I mVar R )
3 esplyfval1.e 
 |-  E = ( I eSymPoly R )
4 esplyfval1.i 
 |-  ( ph -> I e. Fin )
5 esplyfval1.r 
 |-  ( ph -> R e. Ring )
6 eqid 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 }
7 6 psrbasfsupp 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
10 4 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> I e. Fin )
11 5 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> R e. Ring )
12 simplr 
 |-  ( ( ( ph /\ i e. I ) /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> i e. I )
13 simpr 
 |-  ( ( ( ph /\ i e. I ) /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> f e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
14 2 7 8 9 10 11 12 13 mvrval2 
 |-  ( ( ( ph /\ i e. I ) /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( V ` i ) ` f ) = if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
15 14 ad4ant14 
 |-  ( ( ( ( ( ph /\ i e. I ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( V ` i ) ` f ) = if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
16 15 an52ds 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> ( ( V ` i ) ` f ) = if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
17 16 mpteq2dva 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( i e. I |-> ( ( V ` i ) ` f ) ) = ( i e. I |-> if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
18 17 oveq2d 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) = ( R gsum ( i e. I |-> if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
19 nfv 
 |-  F/ j ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I )
20 nfmpt1 
 |-  F/_ j ( j e. I |-> if ( j = i , 1 , 0 ) )
21 20 nfeq2 
 |-  F/ j f = ( j e. I |-> if ( j = i , 1 , 0 ) )
22 nfv 
 |-  F/ j i = U. ( f supp 0 )
23 21 22 nfbi 
 |-  F/ j ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) <-> i = U. ( f supp 0 ) )
24 unisnv 
 |-  U. { j } = j
25 24 eqeq2i 
 |-  ( i = U. { j } <-> i = j )
26 25 a1i 
 |-  ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> ( i = U. { j } <-> i = j ) )
27 simpr 
 |-  ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> ( f supp 0 ) = { j } )
28 27 unieqd 
 |-  ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> U. ( f supp 0 ) = U. { j } )
29 28 adantllr 
 |-  ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> U. ( f supp 0 ) = U. { j } )
30 29 eqeq2d 
 |-  ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> ( i = U. ( f supp 0 ) <-> i = U. { j } ) )
31 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ i = j ) -> ( f supp 0 ) = { j } )
32 31 fveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ i = j ) -> ( ( _Ind ` I ) ` ( f supp 0 ) ) = ( ( _Ind ` I ) ` { j } ) )
33 4 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> I e. Fin )
34 ssrab2 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I )
35 34 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I ) )
36 35 sselda 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> f e. ( NN0 ^m I ) )
37 36 elmaprd 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> f : I --> NN0 )
38 37 adantr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> f : I --> NN0 )
39 ffrn 
 |-  ( f : I --> NN0 -> f : I --> ran f )
40 38 39 syl 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> f : I --> ran f )
41 simpr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> ran f C_ { 0 , 1 } )
42 40 41 fssd 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> f : I --> { 0 , 1 } )
43 33 42 indfsid 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> f = ( ( _Ind ` I ) ` ( f supp 0 ) ) )
44 43 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ i = j ) -> f = ( ( _Ind ` I ) ` ( f supp 0 ) ) )
45 sneq 
 |-  ( i = j -> { i } = { j } )
46 45 adantl 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ i = j ) -> { i } = { j } )
47 46 fveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ i = j ) -> ( ( _Ind ` I ) ` { i } ) = ( ( _Ind ` I ) ` { j } ) )
48 32 44 47 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ i = j ) -> f = ( ( _Ind ` I ) ` { i } ) )
49 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ f = ( ( _Ind ` I ) ` { i } ) ) -> f = ( ( _Ind ` I ) ` { i } ) )
50 49 oveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ f = ( ( _Ind ` I ) ` { i } ) ) -> ( f supp 0 ) = ( ( ( _Ind ` I ) ` { i } ) supp 0 ) )
51 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ f = ( ( _Ind ` I ) ` { i } ) ) -> ( f supp 0 ) = { j } )
52 4 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> I e. Fin )
53 52 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ f = ( ( _Ind ` I ) ` { i } ) ) -> I e. Fin )
54 snssi 
 |-  ( i e. I -> { i } C_ I )
55 54 adantl 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> { i } C_ I )
56 55 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ f = ( ( _Ind ` I ) ` { i } ) ) -> { i } C_ I )
57 indsupp 
 |-  ( ( I e. Fin /\ { i } C_ I ) -> ( ( ( _Ind ` I ) ` { i } ) supp 0 ) = { i } )
58 53 56 57 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ f = ( ( _Ind ` I ) ` { i } ) ) -> ( ( ( _Ind ` I ) ` { i } ) supp 0 ) = { i } )
59 50 51 58 3eqtr3rd 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ f = ( ( _Ind ` I ) ` { i } ) ) -> { i } = { j } )
60 vex 
 |-  i e. _V
61 60 sneqr 
 |-  ( { i } = { j } -> i = j )
62 59 61 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) /\ f = ( ( _Ind ` I ) ` { i } ) ) -> i = j )
63 48 62 impbida 
 |-  ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> ( i = j <-> f = ( ( _Ind ` I ) ` { i } ) ) )
64 indsn 
 |-  ( ( I e. Fin /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
65 52 64 sylan 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
66 65 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
67 66 eqeq2d 
 |-  ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> ( f = ( ( _Ind ` I ) ` { i } ) <-> f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) )
68 63 67 bitr2d 
 |-  ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) <-> i = j ) )
69 26 30 68 3bitr4rd 
 |-  ( ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) <-> i = U. ( f supp 0 ) ) )
70 ovexd 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( f supp 0 ) e. _V )
71 simpr 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( # ` ( f supp 0 ) ) = 1 )
72 hash1snb 
 |-  ( ( f supp 0 ) e. _V -> ( ( # ` ( f supp 0 ) ) = 1 <-> E. j ( f supp 0 ) = { j } ) )
73 72 biimpa 
 |-  ( ( ( f supp 0 ) e. _V /\ ( # ` ( f supp 0 ) ) = 1 ) -> E. j ( f supp 0 ) = { j } )
74 70 71 73 syl2anc 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> E. j ( f supp 0 ) = { j } )
75 exsnrex 
 |-  ( E. j ( f supp 0 ) = { j } <-> E. j e. ( f supp 0 ) ( f supp 0 ) = { j } )
76 74 75 sylib 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> E. j e. ( f supp 0 ) ( f supp 0 ) = { j } )
77 76 adantr 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> E. j e. ( f supp 0 ) ( f supp 0 ) = { j } )
78 19 23 69 77 r19.29af2 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) <-> i = U. ( f supp 0 ) ) )
79 78 ifbid 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( i = U. ( f supp 0 ) , ( 1r ` R ) , ( 0g ` R ) ) )
80 79 mpteq2dva 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( i e. I |-> if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( i e. I |-> if ( i = U. ( f supp 0 ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
81 80 oveq2d 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( R gsum ( i e. I |-> if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( R gsum ( i e. I |-> if ( i = U. ( f supp 0 ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
82 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
83 5 82 syl 
 |-  ( ph -> R e. Mnd )
84 83 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> R e. Mnd )
85 suppssdm 
 |-  ( f supp 0 ) C_ dom f
86 37 fdmd 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> dom f = I )
87 86 ad4antr 
 |-  ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> dom f = I )
88 85 87 sseqtrid 
 |-  ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> ( f supp 0 ) C_ I )
89 simplr 
 |-  ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> j e. ( f supp 0 ) )
90 88 89 sseldd 
 |-  ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> j e. I )
91 24 90 eqeltrid 
 |-  ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> U. { j } e. I )
92 28 91 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) /\ j e. ( f supp 0 ) ) /\ ( f supp 0 ) = { j } ) -> U. ( f supp 0 ) e. I )
93 92 76 r19.29a 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> U. ( f supp 0 ) e. I )
94 eqid 
 |-  ( i e. I |-> if ( i = U. ( f supp 0 ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( i e. I |-> if ( i = U. ( f supp 0 ) , ( 1r ` R ) , ( 0g ` R ) ) )
95 eqid 
 |-  ( Base ` R ) = ( Base ` R )
96 95 9 5 ringidcld 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
97 96 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( 1r ` R ) e. ( Base ` R ) )
98 8 84 52 93 94 97 gsummptif1n0 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( R gsum ( i e. I |-> if ( i = U. ( f supp 0 ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( 1r ` R ) )
99 18 81 98 3eqtrrd 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( 1r ` R ) = ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) )
100 99 anasss 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) ) -> ( 1r ` R ) = ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) )
101 83 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) -> R e. Mnd )
102 4 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) -> I e. Fin )
103 8 gsumz 
 |-  ( ( R e. Mnd /\ I e. Fin ) -> ( R gsum ( i e. I |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
104 101 102 103 syl2anc 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) -> ( R gsum ( i e. I |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
105 14 an32s 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) -> ( ( V ` i ) ` f ) = if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
106 105 adantlr 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) /\ i e. I ) -> ( ( V ` i ) ` f ) = if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
107 simpr 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> f = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
108 107 rneqd 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ran f = ran ( j e. I |-> if ( j = i , 1 , 0 ) ) )
109 nfv 
 |-  F/ j ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I )
110 109 21 nfan 
 |-  F/ j ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
111 eqid 
 |-  ( j e. I |-> if ( j = i , 1 , 0 ) ) = ( j e. I |-> if ( j = i , 1 , 0 ) )
112 1nn0 
 |-  1 e. NN0
113 prid2g 
 |-  ( 1 e. NN0 -> 1 e. { 0 , 1 } )
114 112 113 mp1i 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) /\ j e. I ) -> 1 e. { 0 , 1 } )
115 0nn0 
 |-  0 e. NN0
116 prid1g 
 |-  ( 0 e. NN0 -> 0 e. { 0 , 1 } )
117 115 116 mp1i 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) /\ j e. I ) -> 0 e. { 0 , 1 } )
118 114 117 ifcld 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) /\ j e. I ) -> if ( j = i , 1 , 0 ) e. { 0 , 1 } )
119 110 111 118 rnmptssd 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ran ( j e. I |-> if ( j = i , 1 , 0 ) ) C_ { 0 , 1 } )
120 108 119 eqsstrd 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ran f C_ { 0 , 1 } )
121 120 adantllr 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ran f C_ { 0 , 1 } )
122 simpllr 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> -. ran f C_ { 0 , 1 } )
123 121 122 pm2.65da 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) /\ i e. I ) -> -. f = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
124 123 iffalsed 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) /\ i e. I ) -> if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
125 106 124 eqtr2d 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) /\ i e. I ) -> ( 0g ` R ) = ( ( V ` i ) ` f ) )
126 125 mpteq2dva 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) -> ( i e. I |-> ( 0g ` R ) ) = ( i e. I |-> ( ( V ` i ) ` f ) ) )
127 126 oveq2d 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) -> ( R gsum ( i e. I |-> ( 0g ` R ) ) ) = ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) )
128 104 127 eqtr3d 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) -> ( 0g ` R ) = ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) )
129 128 adantlr 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) ) /\ -. ran f C_ { 0 , 1 } ) -> ( 0g ` R ) = ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) )
130 83 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) -> R e. Mnd )
131 4 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) -> I e. Fin )
132 130 131 103 syl2anc 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) -> ( R gsum ( i e. I |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
133 105 adantlr 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> ( ( V ` i ) ` f ) = if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
134 simpr 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> f = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
135 4 64 sylan 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
136 135 ad5ant14 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
137 134 136 eqtr4d 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> f = ( ( _Ind ` I ) ` { i } ) )
138 137 oveq1d 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ( f supp 0 ) = ( ( ( _Ind ` I ) ` { i } ) supp 0 ) )
139 131 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> I e. Fin )
140 54 ad2antlr 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> { i } C_ I )
141 139 140 57 syl2anc 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ( ( ( _Ind ` I ) ` { i } ) supp 0 ) = { i } )
142 138 141 eqtrd 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ( f supp 0 ) = { i } )
143 142 fveq2d 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ( # ` ( f supp 0 ) ) = ( # ` { i } ) )
144 hashsng 
 |-  ( i e. I -> ( # ` { i } ) = 1 )
145 144 ad2antlr 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ( # ` { i } ) = 1 )
146 143 145 eqtrd 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> ( # ` ( f supp 0 ) ) = 1 )
147 simpllr 
 |-  ( ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) /\ f = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) -> -. ( # ` ( f supp 0 ) ) = 1 )
148 146 147 pm2.65da 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> -. f = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
149 148 iffalsed 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> if ( f = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
150 133 149 eqtr2d 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> ( 0g ` R ) = ( ( V ` i ) ` f ) )
151 150 mpteq2dva 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) -> ( i e. I |-> ( 0g ` R ) ) = ( i e. I |-> ( ( V ` i ) ` f ) ) )
152 151 oveq2d 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) -> ( R gsum ( i e. I |-> ( 0g ` R ) ) ) = ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) )
153 132 152 eqtr3d 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) -> ( 0g ` R ) = ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) )
154 153 adantlr 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) -> ( 0g ` R ) = ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) )
155 pm3.13 
 |-  ( -. ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( -. ran f C_ { 0 , 1 } \/ -. ( # ` ( f supp 0 ) ) = 1 ) )
156 155 adantl 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) ) -> ( -. ran f C_ { 0 , 1 } \/ -. ( # ` ( f supp 0 ) ) = 1 ) )
157 129 154 156 mpjaodan 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) ) -> ( 0g ` R ) = ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) )
158 100 157 ifeqda 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) , ( 1r ` R ) , ( 0g ` R ) ) = ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) )
159 158 mpteq2dva 
 |-  ( ph -> ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) ) )
160 3 fveq1i 
 |-  ( E ` 1 ) = ( ( I eSymPoly R ) ` 1 )
161 112 a1i 
 |-  ( ph -> 1 e. NN0 )
162 6 4 5 161 8 9 esplyfval3 
 |-  ( ph -> ( ( I eSymPoly R ) ` 1 ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
163 160 162 eqtrid 
 |-  ( ph -> ( E ` 1 ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
164 eqid 
 |-  ( Base ` W ) = ( Base ` W )
165 1 2 164 4 5 mvrf2 
 |-  ( ph -> V : I --> ( Base ` W ) )
166 1 164 5 4 6 4 165 mplgsum 
 |-  ( ph -> ( W gsum V ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) ) )
167 159 163 166 3eqtr4d 
 |-  ( ph -> ( E ` 1 ) = ( W gsum V ) )