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 1ex 
 |-  1 e. _V
91 90 prid2 
 |-  1 e. { 0 , 1 }
92 89 91 eqeltrdi 
 |-  ( ( ph /\ j e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) e. { 0 , 1 } )
93 92 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 } )
94 50 51 93 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 } )
95 94 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 } )
96 49 95 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 } )
97 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 ) )
98 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 ) ) ) )
99 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
100 99 a1i 
 |-  ( ( ph /\ j e. I ) -> NN0 e. ( SubMnd ` CCfld ) )
101 25 a1i 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> 0 e. NN0 )
102 27 a1i 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> 1 e. NN0 )
103 101 102 prssd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> { 0 , 1 } C_ NN0 )
104 indf 
 |-  ( ( I e. Fin /\ { k } C_ I ) -> ( ( _Ind ` I ) ` { k } ) : I --> { 0 , 1 } )
105 59 60 104 syl2anc 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( _Ind ` I ) ` { k } ) : I --> { 0 , 1 } )
106 105 61 ffvelcdmd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` j ) e. { 0 , 1 } )
107 103 106 sseldd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` j ) e. NN0 )
108 58 107 eqeltrd 
 |-  ( ( ( ph /\ j e. I ) /\ k e. I ) -> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) e. NN0 )
109 108 fmpttd 
 |-  ( ( ph /\ j e. I ) -> ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) : I --> NN0 )
110 25 a1i 
 |-  ( ( ph /\ j e. I ) -> 0 e. NN0 )
111 109 81 110 fdmfifsupp 
 |-  ( ( ph /\ j e. I ) -> ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) finSupp 0 )
112 72 79 81 100 109 111 gsumsubmcl 
 |-  ( ( ph /\ j e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) e. NN0 )
113 51 112 dmmptd 
 |-  ( ph -> dom ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) = I )
114 98 113 sseqtrid 
 |-  ( ph -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) supp 0 ) C_ I )
115 nfv 
 |-  F/ j ( ph /\ i e. I )
116 ovexd 
 |-  ( ( ( ph /\ i e. I ) /\ j e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) e. _V )
117 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 ) ) ) )
118 115 116 117 fnmptd 
 |-  ( ( ph /\ i e. I ) -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) Fn I )
119 simpr 
 |-  ( ( ph /\ i e. I ) -> i e. I )
120 fveq2 
 |-  ( j = i -> ( ( ( _Ind ` I ) ` { k } ) ` j ) = ( ( ( _Ind ` I ) ` { k } ) ` i ) )
121 120 mpteq2dv 
 |-  ( j = i -> ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) = ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) )
122 121 oveq2d 
 |-  ( j = i -> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) = ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) ) )
123 ovexd 
 |-  ( ( ph /\ i e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) ) e. _V )
124 117 122 119 123 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 ) ) ) )
125 4 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> I e. Fin )
126 simpr 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> k e. I )
127 126 snssd 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> { k } C_ I )
128 simplr 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> i e. I )
129 indfval 
 |-  ( ( I e. Fin /\ { k } C_ I /\ i e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` i ) = if ( i e. { k } , 1 , 0 ) )
130 125 127 128 129 syl3anc 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` i ) = if ( i e. { k } , 1 , 0 ) )
131 velsn 
 |-  ( i e. { k } <-> i = k )
132 equcom 
 |-  ( i = k <-> k = i )
133 131 132 bitri 
 |-  ( i e. { k } <-> k = i )
134 133 a1i 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> ( i e. { k } <-> k = i ) )
135 134 ifbid 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> if ( i e. { k } , 1 , 0 ) = if ( k = i , 1 , 0 ) )
136 130 135 eqtrd 
 |-  ( ( ( ph /\ i e. I ) /\ k e. I ) -> ( ( ( _Ind ` I ) ` { k } ) ` i ) = if ( k = i , 1 , 0 ) )
137 136 mpteq2dva 
 |-  ( ( ph /\ i e. I ) -> ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) = ( k e. I |-> if ( k = i , 1 , 0 ) ) )
138 137 oveq2d 
 |-  ( ( ph /\ i e. I ) -> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` i ) ) ) = ( CCfld gsum ( k e. I |-> if ( k = i , 1 , 0 ) ) ) )
139 73 78 mp1i 
 |-  ( ( ph /\ i e. I ) -> CCfld e. CMnd )
140 139 cmnmndd 
 |-  ( ( ph /\ i e. I ) -> CCfld e. Mnd )
141 eqid 
 |-  ( k e. I |-> if ( k = i , 1 , 0 ) ) = ( k e. I |-> if ( k = i , 1 , 0 ) )
142 86 a1i 
 |-  ( ( ph /\ i e. I ) -> 1 e. ( Base ` CCfld ) )
143 72 140 21 119 141 142 gsummptif1n0 
 |-  ( ( ph /\ i e. I ) -> ( CCfld gsum ( k e. I |-> if ( k = i , 1 , 0 ) ) ) = 1 )
144 124 138 143 3eqtrd 
 |-  ( ( ph /\ i e. I ) -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) ` i ) = 1 )
145 ax-1ne0 
 |-  1 =/= 0
146 145 a1i 
 |-  ( ( ph /\ i e. I ) -> 1 =/= 0 )
147 144 146 eqnetrd 
 |-  ( ( ph /\ i e. I ) -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) ` i ) =/= 0 )
148 118 21 26 119 147 elsuppfnd 
 |-  ( ( ph /\ i e. I ) -> i e. ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) supp 0 ) )
149 148 ex 
 |-  ( ph -> ( i e. I -> i e. ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) supp 0 ) ) )
150 149 ssrdv 
 |-  ( ph -> I C_ ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) ) ) supp 0 ) )
151 58 mpteq2dva 
 |-  ( ( ph /\ j e. I ) -> ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) = ( k e. I |-> ( ( ( _Ind ` I ) ` { k } ) ` j ) ) )
152 151 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 ) ) ) )
153 152 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 ) ) ) ) )
154 153 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 ) )
155 150 154 sseqtrrd 
 |-  ( ph -> I C_ ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) supp 0 ) )
156 114 155 eqssd 
 |-  ( ph -> ( ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) supp 0 ) = I )
157 156 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 )
158 97 157 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 )
159 158 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 ) )
160 159 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 )
161 96 160 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 ) )
162 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 } )
163 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 )
164 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 )
165 ssrab2 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I )
166 165 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I ) )
167 166 sselda 
 |-  ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> u e. ( NN0 ^m I ) )
168 167 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 ) )
169 163 164 168 elmaprd 
 |-  ( ( ( ( ph /\ u e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ran u C_ { 0 , 1 } ) /\ ( # ` ( u supp 0 ) ) = N ) -> u : I --> NN0 )
170 169 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 )
171 170 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 )
172 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 )
173 171 172 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 )
174 162 173 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 } )
175 163 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 )
176 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 )
177 suppssdm 
 |-  ( u supp 0 ) C_ dom u
178 177 170 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 )
179 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 )
180 179 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 ) ) )
181 175 178 180 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 ) )
182 172 181 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 ) )
183 elsuppfn 
 |-  ( ( u Fn I /\ I e. Fin /\ 0 e. NN0 ) -> ( j e. ( u supp 0 ) <-> ( j e. I /\ ( u ` j ) =/= 0 ) ) )
184 183 simplbda 
 |-  ( ( ( u Fn I /\ I e. Fin /\ 0 e. NN0 ) /\ j e. ( u supp 0 ) ) -> ( u ` j ) =/= 0 )
185 171 175 176 182 184 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 )
186 elprn1 
 |-  ( ( ( u ` j ) e. { 0 , 1 } /\ ( u ` j ) =/= 0 ) -> ( u ` j ) = 1 )
187 174 185 186 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 )
188 187 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 ) )
189 169 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 ) ) )
190 89 mpteq2dva 
 |-  ( ph -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) = ( j e. I |-> 1 ) )
191 190 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 ) )
192 188 189 191 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 ) ) ) ) )
193 192 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 ) ) ) ) )
194 161 193 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 ) ) )
195 194 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 ) ) )
196 195 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 ) ) ) )
197 rneq 
 |-  ( u = f -> ran u = ran f )
198 197 sseq1d 
 |-  ( u = f -> ( ran u C_ { 0 , 1 } <-> ran f C_ { 0 , 1 } ) )
199 oveq1 
 |-  ( u = f -> ( u supp 0 ) = ( f supp 0 ) )
200 199 fveqeq2d 
 |-  ( u = f -> ( ( # ` ( u supp 0 ) ) = N <-> ( # ` ( f supp 0 ) ) = N ) )
201 198 200 anbi12d 
 |-  ( u = f -> ( ( ran u C_ { 0 , 1 } /\ ( # ` ( u supp 0 ) ) = N ) <-> ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = N ) ) )
202 201 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 ) ) )
203 202 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 ) ) )
204 196 203 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 ) ) ) )
205 47 204 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 ) ) ) )
206 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 ) )
207 19 a1i 
 |-  ( ph -> NN0 e. _V )
208 112 fmpttd 
 |-  ( ph -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) : I --> NN0 )
209 207 4 208 elmapdd 
 |-  ( ph -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) e. ( NN0 ^m I ) )
210 25 a1i 
 |-  ( ph -> 0 e. NN0 )
211 208 4 210 fidmfisupp 
 |-  ( ph -> ( j e. I |-> ( CCfld gsum ( k e. I |-> ( ( ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) ` k ) ` j ) ) ) ) finSupp 0 )
212 206 209 211 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 } )
213 ovex 
 |-  ( NN0 ^m I ) e. _V
214 213 rabex 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V
215 214 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
216 215 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 )
217 44 205 212 216 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 ) ) ) )
218 43 217 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 ) ) ) )
219 indval 
 |-  ( ( I e. Fin /\ { i } C_ I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j e. { i } , 1 , 0 ) ) )
220 4 22 219 syl2an 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j e. { i } , 1 , 0 ) ) )
221 velsn 
 |-  ( j e. { i } <-> j = i )
222 221 a1i 
 |-  ( ( ( ph /\ i e. I ) /\ j e. I ) -> ( j e. { i } <-> j = i ) )
223 222 ifbid 
 |-  ( ( ( ph /\ i e. I ) /\ j e. I ) -> if ( j e. { i } , 1 , 0 ) = if ( j = i , 1 , 0 ) )
224 223 mpteq2dva 
 |-  ( ( ph /\ i e. I ) -> ( j e. I |-> if ( j e. { i } , 1 , 0 ) ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
225 220 224 eqtrd 
 |-  ( ( ph /\ i e. I ) -> ( ( _Ind ` I ) ` { i } ) = ( j e. I |-> if ( j = i , 1 , 0 ) ) )
226 225 eqeq2d 
 |-  ( ( ph /\ i e. I ) -> ( u = ( ( _Ind ` I ) ` { i } ) <-> u = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) )
227 226 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 ) ) )
228 227 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 ) ) ) )
229 eqeq1 
 |-  ( t = u -> ( t = ( j e. I |-> if ( j = i , 1 , 0 ) ) <-> u = ( j e. I |-> if ( j = i , 1 , 0 ) ) ) )
230 229 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 ) ) )
231 230 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 ) ) )
232 228 231 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 ) ) ) )
233 232 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 ) ) ) ) )
234 eqidd 
 |-  ( ph -> ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) = ( i e. I |-> ( ( _Ind ` I ) ` { i } ) ) )
235 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 ) ) ) ) )
236 eqeq2 
 |-  ( t = ( ( _Ind ` I ) ` { i } ) -> ( u = t <-> u = ( ( _Ind ` I ) ` { i } ) ) )
237 236 ifbid 
 |-  ( t = ( ( _Ind ` I ) ` { i } ) -> if ( u = t , ( 1r ` R ) , ( 0g ` R ) ) = if ( u = ( ( _Ind ` I ) ` { i } ) , ( 1r ` R ) , ( 0g ` R ) ) )
238 237 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 ) ) ) )
239 33 234 235 238 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 ) ) ) ) )
240 9 psrbasfsupp 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
241 2 240 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 ) ) ) ) )
242 233 239 241 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 )
243 242 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 ) )
244 16 218 243 3eqtr2d 
 |-  ( ph -> ( ( I eSymPoly R ) ` N ) = ( M gsum V ) )
245 8 244 eqtrid 
 |-  ( ph -> ( E ` N ) = ( M gsum V ) )