Step |
Hyp |
Ref |
Expression |
1 |
|
elmapi |
|- ( h e. ( NN0 ^m { (/) } ) -> h : { (/) } --> NN0 ) |
2 |
1
|
feqmptd |
|- ( h e. ( NN0 ^m { (/) } ) -> h = ( x e. { (/) } |-> ( h ` x ) ) ) |
3 |
2
|
oveq2d |
|- ( h e. ( NN0 ^m { (/) } ) -> ( CCfld gsum h ) = ( CCfld gsum ( x e. { (/) } |-> ( h ` x ) ) ) ) |
4 |
|
cnring |
|- CCfld e. Ring |
5 |
|
ringmnd |
|- ( CCfld e. Ring -> CCfld e. Mnd ) |
6 |
4 5
|
mp1i |
|- ( h e. ( NN0 ^m { (/) } ) -> CCfld e. Mnd ) |
7 |
|
0ex |
|- (/) e. _V |
8 |
7
|
a1i |
|- ( h e. ( NN0 ^m { (/) } ) -> (/) e. _V ) |
9 |
7
|
snid |
|- (/) e. { (/) } |
10 |
|
ffvelrn |
|- ( ( h : { (/) } --> NN0 /\ (/) e. { (/) } ) -> ( h ` (/) ) e. NN0 ) |
11 |
1 9 10
|
sylancl |
|- ( h e. ( NN0 ^m { (/) } ) -> ( h ` (/) ) e. NN0 ) |
12 |
11
|
nn0cnd |
|- ( h e. ( NN0 ^m { (/) } ) -> ( h ` (/) ) e. CC ) |
13 |
|
cnfldbas |
|- CC = ( Base ` CCfld ) |
14 |
|
fveq2 |
|- ( x = (/) -> ( h ` x ) = ( h ` (/) ) ) |
15 |
13 14
|
gsumsn |
|- ( ( CCfld e. Mnd /\ (/) e. _V /\ ( h ` (/) ) e. CC ) -> ( CCfld gsum ( x e. { (/) } |-> ( h ` x ) ) ) = ( h ` (/) ) ) |
16 |
6 8 12 15
|
syl3anc |
|- ( h e. ( NN0 ^m { (/) } ) -> ( CCfld gsum ( x e. { (/) } |-> ( h ` x ) ) ) = ( h ` (/) ) ) |
17 |
3 16
|
eqtrd |
|- ( h e. ( NN0 ^m { (/) } ) -> ( CCfld gsum h ) = ( h ` (/) ) ) |
18 |
|
df1o2 |
|- 1o = { (/) } |
19 |
18
|
oveq2i |
|- ( NN0 ^m 1o ) = ( NN0 ^m { (/) } ) |
20 |
17 19
|
eleq2s |
|- ( h e. ( NN0 ^m 1o ) -> ( CCfld gsum h ) = ( h ` (/) ) ) |
21 |
20
|
eqcomd |
|- ( h e. ( NN0 ^m 1o ) -> ( h ` (/) ) = ( CCfld gsum h ) ) |
22 |
21
|
mpteq2ia |
|- ( h e. ( NN0 ^m 1o ) |-> ( h ` (/) ) ) = ( h e. ( NN0 ^m 1o ) |-> ( CCfld gsum h ) ) |