Metamath Proof Explorer

Theorem esplyfvaln

Description: The last elementary symmetric polynomial is the product 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 )
esplyfvaln.r 
|- ( ph -> R e. CRing )
esplyfvaln.n 
|- N = ( # ` I )
esplyfvaln.m 
|- M = ( mulGrp ` W )
Assertion esplyfvaln 
|- ( ph -> ( E ` N ) = ( M 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 esplyfvaln.r 
 |-  ( ph -> R e. CRing )
6 esplyfvaln.n 
 |-  N = ( # ` I )
7 esplyfvaln.m 
 |-  M = ( mulGrp ` W )
8 3 fveq1i 
 |-  ( E ` N ) = ( ( I eSymPoly R ) ` N )
9 eqid 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 }
10 5 crngringd 
 |-  ( ph -> R e. Ring )
11 hashcl 
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
12 4 11 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
13 6 12 eqeltrid 
 |-  ( ph -> N e. NN0 )
14 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
15 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
16 9 4 10 13 14 15 esplyfval3 
 |-  ( ph -> ( ( I eSymPoly R ) ` N ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
17 eqid 
 |-  ( Base ` W ) = ( Base ` W )
18 breq1 
 |-  ( h = ( ( _Ind ` I ) ` { i } ) -> ( h finSupp 0 <-> ( ( _Ind ` I ) ` { i } ) finSupp 0 ) )
19 nn0ex 
 |-  NN0 e. _V
20 19 a1i 
 |-  ( ( ph /\ i e. I ) -> NN0 e. _V )
21 4 adantr 
 |-  ( ( ph /\ i e. I ) -> I e. Fin )
22 snssi 
 |-  ( i e. I -> { i } C_ I )
23 indf 
 |-  ( ( I e. Fin /\ { i } C_ I ) -> ( ( _Ind ` I ) ` { i } ) : I --> { 0 , 1 } )
24 4 22 23 syl2an 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) : I --> { 0 , 1 } )
25 0nn0 
 |-  0 e. NN0
26 25 a1i 
 |-  ( ( ph /\ i e. I ) -> 0 e. NN0 )
27 1nn0 
 |-  1 e. NN0
28 27 a1i 
 |-  ( ( ph /\ i e. I ) -> 1 e. NN0 )
29 26 28 prssd 
 |-  ( ( ph /\ i e. I ) -> { 0 , 1 } C_ NN0 )
30 24 29 fssd 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) : I --> NN0 )
31 20 21 30 elmapdd 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) e. ( NN0 ^m I ) )
32 24 21 26 fidmfisupp 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) finSupp 0 )
33 18 31 32 elrabd 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
34 33 fmpttd 
 |-  ( ph -> ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) : I --> { h e. ( NN0 ^m I ) | h finSupp 0 } )
35 eqeq2 
 |-  ( t = y -> ( u = t <-> u = y ) )
36 35 ifbid 
 |-  ( t = y -> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) = if ( u = y , ( 1r ` R ) , ( 0g ` R ) ) )
37 36 mpteq2dv 
 |-  ( t = y -> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) = ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
38 eqeq1 
 |-  ( u = z -> ( u = y <-> z = y ) )
39 38 ifbid 
 |-  ( u = z -> if ( u = y , ( 1r ` R ) , ( 0g ` R ) ) = if ( z = y , ( 1r ` R ) , ( 0g ` R ) ) )
40 39 cbvmptv 
 |-  ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = y , ( 1r ` R ) , ( 0g ` R ) ) ) = ( z e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( z = y , ( 1r ` R ) , ( 0g ` R ) ) )
41 37 40 eqtrdi 
 |-  ( t = y -> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) = ( z e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( z = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
42 41 cbvmptv 
 |-  ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( z e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( z = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
43 1 17 5 4 9 4 34 15 14 7 42 mplmonprod 
 |-  ( ph -> ( M gsum ( ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) o. ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ) ) = ( ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) ` ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) )
44 eqid 
 |-  ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) )
45 eqeq2 
 |-  ( t = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) -> ( u = t <-> u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) )
46 45 ifbid 
 |-  ( t = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) -> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) = if ( u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
47 46 mpteq2dv 
 |-  ( t = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) -> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) = ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
48 simpr 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) )
49 48 rneqd 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> ran u = ran ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) )
50 nfv 
 |-  F/ j ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
51 eqid 
 |-  ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) )
52 eqid 
 |-  ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) = ( i e. I |-> ( ( _Ind ` I ) ` { i } ) )
53 sneq 
 |-  ( i = k -> { i } = { k } )
54 53 fveq2d 
 |-  ( i = k -> ( ( _Ind ` I ) ` { i } ) = ( ( _Ind ` I ) ` { k } ) )
55 simpr 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> k e. I )
56 fvexd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( _Ind ` I ) ` { k } ) e. _V )
57 52 54 55 56 fvmptd3 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) = ( ( _Ind ` I ) ` { k } ) )
58 57 fveq1d 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) = ( ( ( _Ind ` I ) ` { k } ) ` j ) )
59 4 ad2antrr 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> I e. Fin )
60 55 snssd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> { k } C_ I )
61 simplr 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> j e. I )
62 indfval 
 |-  ( ( I e. Fin /\ { k } C_ I /\ j e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` j ) = if ( j e. { k } , 1 , 0 ) )
63 59 60 61 62 syl3anc 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` j ) = if ( j e. { k } , 1 , 0 ) )
64 velsn 
 |-  ( j e. { k } <-> j = k )
65 equcom 
 |-  ( j = k <-> k = j )
66 64 65 bitri 
 |-  ( j e. { k } <-> k = j )
67 66 a1i 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( j e. { k } <-> k = j ) )
68 67 ifbid 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> if ( j e. { k } , 1 , 0 ) = if ( k = j , 1 , 0 ) )
69 58 63 68 3eqtrd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) = if ( k = j , 1 , 0 ) )
70 69 mpteq2dva 
 |-  ( ( ph /\ j e. I ) -> ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) = ( k e. I |-> if ( k = j , 1 , 0 ) ) )
71 70 oveq2d 
 |-  ( ( ph /\ j e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) = ( CCfld gsum ( k e. I |-> if ( k = j , 1 , 0 ) ) ) )
72 cnfld0 
 |-  0 = ( 0g ` CCfld )
73 cnfldfld 
 |-  CCfld e. Field
74 id 
 |-  ( CCfld e. Field -> CCfld e. Field )
75 74 fldcrngd 
 |-  ( CCfld e. Field -> CCfld e. CRing )
76 crngring 
 |-  ( CCfld e. CRing -> CCfld e. Ring )
77 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
78 75 76 77 3syl 
 |-  ( CCfld e. Field -> CCfld e. CMnd )
79 73 78 mp1i 
 |-  ( ( ph /\ j e. I ) -> CCfld e. CMnd )
80 79 cmnmndd 
 |-  ( ( ph /\ j e. I ) -> CCfld e. Mnd )
81 4 adantr 
 |-  ( ( ph /\ j e. I ) -> I e. Fin )
82 simpr 
 |-  ( ( ph /\ j e. I ) -> j e. I )
83 eqid 
 |-  ( k e. I |-> if ( k = j , 1 , 0 ) ) = ( k e. I |-> if ( k = j , 1 , 0 ) )
84 ax-1cn 
 |-  1 e. CC
85 cnfldbas 
 |-  CC = ( Base ` CCfld )
86 84 85 eleqtri 
 |-  1 e. ( Base ` CCfld )
87 86 a1i 
 |-  ( ( ph /\ j e. I ) -> 1 e. ( Base ` CCfld ) )
88 72 80 81 82 83 87 gsummptif1n0 
 |-  ( ( ph /\ j e. I ) -> ( CCfld gsum ( k e. I |-> if ( k = j , 1 , 0 ) ) ) = 1 )
89 71 88 eqtrd 
 |-  ( ( ph /\ j e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) = 1 )
90 1elpr01 
 |-  1 e. { 0 , 1 }
91 89 90 eqeltrdi 
 |-  ( ( ph /\ j e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) e. { 0 , 1 } )
92 91 adantlr 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ j e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) e. { 0 , 1 } )
93 50 51 92 rnmptssd 
 |-  ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ran ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) C_ { 0 , 1 } )
94 93 adantr 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> ran ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) C_ { 0 , 1 } )
95 49 94 eqsstrd 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> ran u C_ { 0 , 1 } )
96 48 oveq1d 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> ( u supp 0 ) = ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) supp 0 ) )
97 suppssdm 
 |-  ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) supp 0 ) C_ dom ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) )
98 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
99 98 a1i 
 |-  ( ( ph /\ j e. I ) -> NN0 e. ( SubMnd ` CCfld ) )
100 25 a1i 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> 0 e. NN0 )
101 27 a1i 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> 1 e. NN0 )
102 100 101 prssd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> { 0 , 1 } C_ NN0 )
103 indf 
 |-  ( ( I e. Fin /\ { k } C_ I ) -> ( ( _Ind ` I ) ` { k } ) : I --> { 0 , 1 } )
104 59 60 103 syl2anc 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( _Ind ` I ) ` { k } ) : I --> { 0 , 1 } )
105 104 61 ffvelcdmd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` j ) e. { 0 , 1 } )
106 102 105 sseldd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` j ) e. NN0 )
107 58 106 eqeltrd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) e. NN0 )
108 107 fmpttd 
 |-  ( ( ph /\ j e. I ) -> ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) : I --> NN0 )
109 25 a1i 
 |-  ( ( ph /\ j e. I ) -> 0 e. NN0 )
110 108 81 109 fdmfifsupp 
 |-  ( ( ph /\ j e. I ) -> ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) finSupp 0 )
111 72 79 81 99 108 110 gsumsubmcl 
 |-  ( ( ph /\ j e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) e. NN0 )
112 51 111 dmmptd 
 |-  ( ph -> dom ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) = I )
113 97 112 sseqtrid 
 |-  ( ph -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) supp 0 ) C_ I )
114 nfv 
 |-  F/ j ( ph /\ i e. I )
115 ovexd 
 |-  ( ( ( ph /\ i e. I ) /\ j e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) e. _V )
116 eqid 
 |-  ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) )
117 114 115 116 fnmptd 
 |-  ( ( ph /\ i e. I ) -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) Fn I )
118 simpr 
 |-  ( ( ph /\ i e. I ) -> i e. I )
119 fveq2 
 |-  ( j = i -> ( ( ( _Ind ` I ) ` { k } ) ` j ) = ( ( ( _Ind ` I ) ` { k } ) ` i ) )
120 119 mpteq2dv 
 |-  ( j = i -> ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) = ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) )
121 120 oveq2d 
 |-  ( j = i -> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) = ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) ) )
122 ovexd 
 |-  ( ( ph /\ i e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) ) e. _V )
123 116 121 118 122 fvmptd3 
 |-  ( ( ph /\ i e. I ) -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) ` i ) = ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) ) )
124 4 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> I e. Fin )
125 simpr 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> k e. I )
126 125 snssd 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> { k } C_ I )
127 simplr 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> i e. I )
128 indfval 
 |-  ( ( I e. Fin /\ { k } C_ I /\ i e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` i ) = if ( i e. { k } , 1 , 0 ) )
129 124 126 127 128 syl3anc 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` i ) = if ( i e. { k } , 1 , 0 ) )
130 velsn 
 |-  ( i e. { k } <-> i = k )
131 equcom 
 |-  ( i = k <-> k = i )
132 130 131 bitri 
 |-  ( i e. { k } <-> k = i )
133 132 a1i 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> ( i e. { k } <-> k = i ) )
134 133 ifbid 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> if ( i e. { k } , 1 , 0 ) = if ( k = i , 1 , 0 ) )
135 129 134 eqtrd 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` i ) = if ( k = i , 1 , 0 ) )
136 135 mpteq2dva 
 |-  ( ( ph /\ i e. I ) -> ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) = ( k e. I |-> if ( k = i , 1 , 0 ) ) )
137 136 oveq2d 
 |-  ( ( ph /\ i e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) ) = ( CCfld gsum ( k e. I |-> if ( k = i , 1 , 0 ) ) ) )
138 73 78 mp1i 
 |-  ( ( ph /\ i e. I ) -> CCfld e. CMnd )
139 138 cmnmndd 
 |-  ( ( ph /\ i e. I ) -> CCfld e. Mnd )
140 eqid 
 |-  ( k e. I |-> if ( k = i , 1 , 0 ) ) = ( k e. I |-> if ( k = i , 1 , 0 ) )
141 86 a1i 
 |-  ( ( ph /\ i e. I ) -> 1 e. ( Base ` CCfld ) )
142 72 139 21 118 140 141 gsummptif1n0 
 |-  ( ( ph /\ i e. I ) -> ( CCfld gsum ( k e. I |-> if ( k = i , 1 , 0 ) ) ) = 1 )
143 123 137 142 3eqtrd 
 |-  ( ( ph /\ i e. I ) -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) ` i ) = 1 )
144 ax-1ne0 
 |-  1 =/= 0
145 144 a1i 
 |-  ( ( ph /\ i e. I ) -> 1 =/= 0 )
146 143 145 eqnetrd 
 |-  ( ( ph /\ i e. I ) -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) ` i ) =/= 0 )
147 117 21 26 118 146 elsuppfnd 
 |-  ( ( ph /\ i e. I ) -> i e. ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) supp 0 ) )
148 147 ex 
 |-  ( ph -> ( i e. I -> i e. ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) supp 0 ) ) )
149 148 ssrdv 
 |-  ( ph -> I C_ ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) supp 0 ) )
150 58 mpteq2dva 
 |-  ( ( ph /\ j e. I ) -> ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) = ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) )
151 150 oveq2d 
 |-  ( ( ph /\ j e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) = ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) )
152 151 mpteq2dva 
 |-  ( ph -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) )
153 152 oveq1d 
 |-  ( ph -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) supp 0 ) = ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) supp 0 ) )
154 149 153 sseqtrrd 
 |-  ( ph -> I C_ ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) supp 0 ) )
155 113 154 eqssd 
 |-  ( ph -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) supp 0 ) = I )
156 155 ad2antrr 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) supp 0 ) = I )
157 96 156 eqtrd 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> ( u supp 0 ) = I )
158 157 fveq2d 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> ( # ` ( u supp 0 ) ) = ( # ` I ) )
159 158 6 eqtr4di 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> ( # ` ( u supp 0 ) ) = N )
160 95 159 jca 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> ( ran u C_ { 0 , 1 } /\ ( # ` ( u supp 0 ) ) = N ) )
161 simpllr 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> ran u C_ { 0 , 1 } )
162 4 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) -> I e. Fin )
163 19 a1i 
 |-  ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) -> NN0 e. _V )
164 ssrab2 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I )
165 164 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I ) )
166 165 sselda 
 |-  ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> u e. ( NN0 ^m I ) )
167 166 ad2antrr 
 |-  ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) -> u e. ( NN0 ^m I ) )
168 162 163 167 elmaprd 
 |-  ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) -> u : I --> NN0 )
169 168 adantr 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> u : I --> NN0 )
170 169 ffnd 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> u Fn I )
171 simpr 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> j e. I )
172 170 171 fnfvelrnd 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> ( u ` j ) e. ran u )
173 161 172 sseldd 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> ( u ` j ) e. { 0 , 1 } )
174 162 adantr 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> I e. Fin )
175 25 a1i 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> 0 e. NN0 )
176 suppssdm 
 |-  ( u supp 0 ) C_ dom u
177 176 169 fssdm 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> ( u supp 0 ) C_ I )
178 simplr 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> ( # ` ( u supp 0 ) ) = N )
179 178 6 eqtr2di 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> ( # ` I ) = ( # ` ( u supp 0 ) ) )
180 174 177 179 phphashd 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> I = ( u supp 0 ) )
181 171 180 eleqtrd 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> j e. ( u supp 0 ) )
182 elsuppfn 
 |-  ( ( u Fn I /\ I e. Fin /\ 0 e. NN0 ) -> ( j e. ( u supp 0 ) <-> ( j e. I /\ ( u ` j ) =/= 0 ) ) )
183 182 simplbda 
 |-  ( ( ( u Fn I /\ I e. Fin /\ 0 e. NN0 ) /\ j e. ( u supp 0 ) ) -> ( u ` j ) =/= 0 )
184 170 174 175 181 183 syl31anc 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> ( u ` j ) =/= 0 )
185 elprn1 
 |-  ( ( ( u ` j ) e. { 0 , 1 } /\ ( u ` j ) =/= 0 ) -> ( u ` j ) = 1 )
186 173 184 185 syl2anc 
 |-  ( ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) /\ j e. I ) -> ( u ` j ) = 1 )
187 186 mpteq2dva 
 |-  ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) -> ( j e. I |-> ( u ` j ) ) = ( j e. I |-> 1 ) )
188 168 feqmptd 
 |-  ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) -> u = ( j e. I |-> ( u ` j ) ) )
189 89 mpteq2dva 
 |-  ( ph -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) = ( j e. I |-> 1 ) )
190 189 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) = ( j e. I |-> 1 ) )
191 187 188 190 3eqtr4d 
 |-  ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) -> u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) )
192 191 anasss 
 |-  ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( ran u C_ { 0 , 1 } /\ ( # ` ( u supp 0 ) ) = N ) ) -> u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) )
193 160 192 impbida 
 |-  ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) <-> ( ran u C_ { 0 , 1 } /\ ( # ` ( u supp 0 ) ) = N ) ) )
194 193 ifbid 
 |-  ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> if ( u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( ran u C_ { 0 , 1 } /\ ( # ` ( u supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) )
195 194 mpteq2dva 
 |-  ( ph -> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran u C_ { 0 , 1 } /\ ( # ` ( u supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
196 rneq 
 |-  ( u = f -> ran u = ran f )
197 196 sseq1d 
 |-  ( u = f -> ( ran u C_ { 0 , 1 } <-> ran f C_ { 0 , 1 } ) )
198 oveq1 
 |-  ( u = f -> ( u supp 0 ) = ( f supp 0 ) )
199 198 fveqeq2d 
 |-  ( u = f -> ( ( # ` ( u supp 0 ) ) = N <-> ( # ` ( f supp 0 ) ) = N ) )
200 197 199 anbi12d 
 |-  ( u = f -> ( ( ran u C_ { 0 , 1 } /\ ( # ` ( u supp 0 ) ) = N ) <-> ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) ) )
201 200 ifbid 
 |-  ( u = f -> if ( ( ran u C_ { 0 , 1 } /\ ( # ` ( u supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) )
202 201 cbvmptv 
 |-  ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran u C_ { 0 , 1 } /\ ( # ` ( u supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) )
203 195 202 eqtrdi 
 |-  ( ph -> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
204 47 203 sylan9eqr 
 |-  ( ( ph /\ t = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) -> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
205 breq1 
 |-  ( h = ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) -> ( h finSupp 0 <-> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) finSupp 0 ) )
206 19 a1i 
 |-  ( ph -> NN0 e. _V )
207 111 fmpttd 
 |-  ( ph -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) : I --> NN0 )
208 206 4 207 elmapdd 
 |-  ( ph -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) e. ( NN0 ^m I ) )
209 25 a1i 
 |-  ( ph -> 0 e. NN0 )
210 207 4 209 fidmfisupp 
 |-  ( ph -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) finSupp 0 )
211 205 208 210 elrabd 
 |-  ( ph -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
212 ovex 
 |-  ( NN0 ^m I ) e. _V
213 212 rabex 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V
214 213 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
215 214 mptexd 
 |-  ( ph -> ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V )
216 44 204 211 215 fvmptd2 
 |-  ( ph -> ( ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) ` ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
217 43 216 eqtrd 
 |-  ( ph -> ( M gsum ( ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) o. ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ) ) = ( f e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
218 indval 
 |-  ( ( I e. Fin /\ { i } C_ I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j e. { i } , 1 , 0 ) ) )
219 4 22 218 syl2an 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j e. { i } , 1 , 0 ) ) )
220 velsn 
 |-  ( j e. { i } <-> j = i )
221 220 a1i 
 |-  ( ( ( ph /\ i e. I ) /\ j e. I ) -> ( j e. { i } <-> j = i ) )
222 221 ifbid 
 |-  ( ( ( ph /\ i e. I ) /\ j e. I ) -> if ( j e. { i } , 1 , 0 ) = if ( j = i , 1 , 0 ) )
223 222 mpteq2dva 
 |-  ( ( ph /\ i e. I ) -> ( j e. I |-> if ( j e. { i } , 1 , 0 ) ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
224 219 223 eqtrd 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
225 224 eqeq2d 
 |-  ( ( ph /\ i e. I ) -> ( u = ( ( _Ind ` I ) ` { i } ) <-> u = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) )
226 225 ifbid 
 |-  ( ( ph /\ i e. I ) -> if ( u = ( ( _Ind ` I ) ` { i } ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( u = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
227 226 mpteq2dv 
 |-  ( ( ph /\ i e. I ) -> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = ( ( _Ind ` I ) ` { i } ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
228 eqeq1 
 |-  ( t = u -> ( t = ( j e. I |-> if ( j = i , 1 , 0 ) ) <-> u = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) )
229 228 ifbid 
 |-  ( t = u -> if ( t = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( u = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
230 229 cbvmptv 
 |-  ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( t = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
231 227 230 eqtr4di 
 |-  ( ( ph /\ i e. I ) -> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = ( ( _Ind ` I ) ` { i } ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( t = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
232 231 mpteq2dva 
 |-  ( ph -> ( i e. I |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = ( ( _Ind ` I ) ` { i } ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( i e. I |-> ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( t = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
233 eqidd 
 |-  ( ph -> ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) = ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) )
234 eqidd 
 |-  ( ph -> ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
235 eqeq2 
 |-  ( t = ( ( _Ind ` I ) ` { i } ) -> ( u = t <-> u = ( ( _Ind ` I ) ` { i } ) ) )
236 235 ifbid 
 |-  ( t = ( ( _Ind ` I ) ` { i } ) -> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) = if ( u = ( ( _Ind ` I ) ` { i } ) , ( 1r ` R ) , ( 0g ` R ) ) )
237 236 mpteq2dv 
 |-  ( t = ( ( _Ind ` I ) ` { i } ) -> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) = ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = ( ( _Ind ` I ) ` { i } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
238 33 233 234 237 fmptco 
 |-  ( ph -> ( ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) o. ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ) = ( i e. I |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = ( ( _Ind ` I ) ` { i } ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
239 9 psrbasfsupp 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
240 2 239 14 15 4 5 mvrfval 
 |-  ( ph -> V = ( i e. I |-> ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( t = ( j e. I |-> if ( j = i , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
241 232 238 240 3eqtr4d 
 |-  ( ph -> ( ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) o. ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ) = V )
242 241 oveq2d 
 |-  ( ph -> ( M gsum ( ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) ) ) o. ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ) ) = ( M gsum V ) )
243 16 217 242 3eqtr2d 
 |-  ( ph -> ( ( I eSymPoly R ) ` N ) = ( M gsum V ) )
244 8 243 eqtrid 
 |-  ( ph -> ( E ` N ) = ( M gsum V ) )