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

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 4 adantr 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> I e. Fin )
35 nn0ex 
 |-  NN0 e. _V
36 35 a1i 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> NN0 e. _V )
37 ssrab2 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I )
38 37 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I ) )
39 38 sselda 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> f e. ( NN0 ^m I ) )
40 34 36 39 elmaprd 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> f : I --> NN0 )
41 40 adantr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> f : I --> NN0 )
42 ffrn 
 |-  ( f : I --> NN0 -> f : I --> ran f )
43 41 42 syl 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> f : I --> ran f )
44 simpr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> ran f C_ { 0 , 1 } )
45 43 44 fssd 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> f : I --> { 0 , 1 } )
46 33 45 indfsid 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) -> f = ( ( _Ind ` I ) ` ( f supp 0 ) ) )
47 46 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 ) ) )
48 sneq 
 |-  ( i = j -> { i } = { j } )
49 48 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 } )
50 49 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 } ) )
51 32 47 50 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 } ) )
52 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 } ) )
53 52 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 ) )
54 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 } )
55 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 )
56 55 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 )
57 snssi 
 |-  ( i e. I -> { i } C_ I )
58 57 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 )
59 58 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 )
60 indsupp 
 |-  ( ( I e. Fin /\ { i } C_ I ) -> ( ( ( _Ind ` I ) ` { i } ) supp 0 ) = { i } )
61 56 59 60 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 } )
62 53 54 61 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 } )
63 vex 
 |-  i e. _V
64 63 sneqr 
 |-  ( { i } = { j } -> i = j )
65 62 64 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 )
66 51 65 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 } ) ) )
67 indsn 
 |-  ( ( I e. Fin /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
68 55 67 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 ) ) )
69 68 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 ) ) )
70 69 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 ) ) ) )
71 66 70 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 ) )
72 26 30 71 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 ) ) )
73 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 )
74 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 )
75 hash1snb 
 |-  ( ( f supp 0 ) e. _V -> ( ( # ` ( f supp 0 ) ) = 1 <-> E. j ( f supp 0 ) = { j } ) )
76 75 biimpa 
 |-  ( ( ( f supp 0 ) e. _V /\ ( # ` ( f supp 0 ) ) = 1 ) -> E. j ( f supp 0 ) = { j } )
77 73 74 76 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 } )
78 exsnrex 
 |-  ( E. j ( f supp 0 ) = { j } <-> E. j e. ( f supp 0 ) ( f supp 0 ) = { j } )
79 77 78 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 } )
80 79 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 } )
81 19 23 72 80 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 ) ) )
82 81 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 ) ) )
83 82 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 ) ) ) )
84 83 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 ) ) ) ) )
85 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
86 5 85 syl 
 |-  ( ph -> R e. Mnd )
87 86 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran f C_ { 0 , 1 } ) /\ ( # ` ( f supp 0 ) ) = 1 ) -> R e. Mnd )
88 suppssdm 
 |-  ( f supp 0 ) C_ dom f
89 40 fdmd 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> dom f = I )
90 89 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 )
91 88 90 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 )
92 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 ) )
93 91 92 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 )
94 24 93 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 )
95 28 94 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 )
96 95 79 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 )
97 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 ) ) )
98 eqid 
 |-  ( Base ` R ) = ( Base ` R )
99 98 9 5 ringidcld 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
100 99 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 ) )
101 8 87 55 96 97 100 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 ) )
102 18 84 101 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 ) ) ) )
103 102 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 ) ) ) )
104 86 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) -> R e. Mnd )
105 4 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ran f C_ { 0 , 1 } ) -> I e. Fin )
106 8 gsumz 
 |-  ( ( R e. Mnd /\ I e. Fin ) -> ( R gsum ( i e. I |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
107 104 105 106 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 ) )
108 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 ) ) )
109 108 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 ) ) )
110 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 ) ) )
111 110 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 ) ) )
112 nfv 
 |-  F/ j ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I )
113 112 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 ) ) )
114 eqid 
 |-  ( j e. I |-> if ( j = i , 1 , 0 ) ) = ( j e. I |-> if ( j = i , 1 , 0 ) )
115 1nn0 
 |-  1 e. NN0
116 prid2g 
 |-  ( 1 e. NN0 -> 1 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 ) -> 1 e. { 0 , 1 } )
118 0nn0 
 |-  0 e. NN0
119 prid1g 
 |-  ( 0 e. NN0 -> 0 e. { 0 , 1 } )
120 118 119 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 } )
121 117 120 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 } )
122 113 114 121 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 } )
123 111 122 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 } )
124 123 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 } )
125 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 } )
126 124 125 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 ) ) )
127 126 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 ) )
128 109 127 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 ) )
129 128 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 ) ) )
130 129 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 ) ) ) )
131 107 130 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 ) ) ) )
132 131 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 ) ) ) )
133 86 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) -> R e. Mnd )
134 4 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) -> I e. Fin )
135 133 134 106 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 ) )
136 108 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 ) ) )
137 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 ) ) )
138 4 67 sylan 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
139 138 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 ) ) )
140 137 139 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 } ) )
141 140 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 ) )
142 134 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 )
143 57 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 )
144 142 143 60 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 } )
145 141 144 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 } )
146 145 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 } ) )
147 hashsng 
 |-  ( i e. I -> ( # ` { i } ) = 1 )
148 147 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 )
149 146 148 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 )
150 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 )
151 149 150 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 ) ) )
152 151 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 ) )
153 136 152 eqtr2d 
 |-  ( ( ( ( ph /\ f e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ -. ( # ` ( f supp 0 ) ) = 1 ) /\ i e. I ) -> ( 0g ` R ) = ( ( V ` i ) ` f ) )
154 153 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 ) ) )
155 154 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 ) ) ) )
156 135 155 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 ) ) ) )
157 156 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 ) ) ) )
158 pm3.13 
 |-  ( -. ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = 1 ) -> ( -. ran f C_ { 0 , 1 } \/ -. ( # ` ( f supp 0 ) ) = 1 ) )
159 158 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 ) )
160 132 157 159 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 ) ) ) )
161 103 160 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 ) ) ) )
162 161 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 ) ) ) ) )
163 3 fveq1i 
 |-  ( E ` 1 ) = ( ( I eSymPoly R ) ` 1 )
164 115 a1i 
 |-  ( ph -> 1 e. NN0 )
165 6 4 5 164 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 ) ) ) )
166 163 165 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 ) ) ) )
167 eqid 
 |-  ( Base ` W ) = ( Base ` W )
168 1 2 167 4 5 mvrf2 
 |-  ( ph -> V : I --> ( Base ` W ) )
169 1 167 5 4 6 4 168 mplgsum 
 |-  ( ph -> ( W gsum V ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( i e. I |-> ( ( V ` i ) ` f ) ) ) ) )
170 162 166 169 3eqtr4d 
 |-  ( ph -> ( E ` 1 ) = ( W gsum V ) )