Step |
Hyp |
Ref |
Expression |
1 |
|
gsumfsum.1 |
|- ( ph -> A e. Fin ) |
2 |
|
gsumfsum.2 |
|- ( ( ph /\ k e. A ) -> B e. CC ) |
3 |
|
mpteq1 |
|- ( A = (/) -> ( k e. A |-> B ) = ( k e. (/) |-> B ) ) |
4 |
|
mpt0 |
|- ( k e. (/) |-> B ) = (/) |
5 |
3 4
|
eqtrdi |
|- ( A = (/) -> ( k e. A |-> B ) = (/) ) |
6 |
5
|
oveq2d |
|- ( A = (/) -> ( CCfld gsum ( k e. A |-> B ) ) = ( CCfld gsum (/) ) ) |
7 |
|
cnfld0 |
|- 0 = ( 0g ` CCfld ) |
8 |
7
|
gsum0 |
|- ( CCfld gsum (/) ) = 0 |
9 |
|
sum0 |
|- sum_ k e. (/) B = 0 |
10 |
8 9
|
eqtr4i |
|- ( CCfld gsum (/) ) = sum_ k e. (/) B |
11 |
6 10
|
eqtrdi |
|- ( A = (/) -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. (/) B ) |
12 |
|
sumeq1 |
|- ( A = (/) -> sum_ k e. A B = sum_ k e. (/) B ) |
13 |
11 12
|
eqtr4d |
|- ( A = (/) -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) |
14 |
13
|
a1i |
|- ( ph -> ( A = (/) -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) ) |
15 |
|
cnfldbas |
|- CC = ( Base ` CCfld ) |
16 |
|
cnfldadd |
|- + = ( +g ` CCfld ) |
17 |
|
eqid |
|- ( Cntz ` CCfld ) = ( Cntz ` CCfld ) |
18 |
|
cnring |
|- CCfld e. Ring |
19 |
|
ringmnd |
|- ( CCfld e. Ring -> CCfld e. Mnd ) |
20 |
18 19
|
mp1i |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> CCfld e. Mnd ) |
21 |
1
|
adantr |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> A e. Fin ) |
22 |
2
|
fmpttd |
|- ( ph -> ( k e. A |-> B ) : A --> CC ) |
23 |
22
|
adantr |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> B ) : A --> CC ) |
24 |
|
ringcmn |
|- ( CCfld e. Ring -> CCfld e. CMnd ) |
25 |
18 24
|
mp1i |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> CCfld e. CMnd ) |
26 |
15 17 25 23
|
cntzcmnf |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ran ( k e. A |-> B ) C_ ( ( Cntz ` CCfld ) ` ran ( k e. A |-> B ) ) ) |
27 |
|
simprl |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN ) |
28 |
|
simprr |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) |
29 |
|
f1of1 |
|- ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) -1-1-> A ) |
30 |
28 29
|
syl |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-> A ) |
31 |
|
suppssdm |
|- ( ( k e. A |-> B ) supp 0 ) C_ dom ( k e. A |-> B ) |
32 |
31 23
|
fssdm |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) supp 0 ) C_ A ) |
33 |
|
f1ofo |
|- ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) -onto-> A ) |
34 |
|
forn |
|- ( f : ( 1 ... ( # ` A ) ) -onto-> A -> ran f = A ) |
35 |
28 33 34
|
3syl |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ran f = A ) |
36 |
32 35
|
sseqtrrd |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) supp 0 ) C_ ran f ) |
37 |
|
eqid |
|- ( ( ( k e. A |-> B ) o. f ) supp 0 ) = ( ( ( k e. A |-> B ) o. f ) supp 0 ) |
38 |
15 7 16 17 20 21 23 26 27 30 36 37
|
gsumval3 |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( CCfld gsum ( k e. A |-> B ) ) = ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) ) |
39 |
|
sumfc |
|- sum_ x e. A ( ( k e. A |-> B ) ` x ) = sum_ k e. A B |
40 |
|
fveq2 |
|- ( x = ( f ` n ) -> ( ( k e. A |-> B ) ` x ) = ( ( k e. A |-> B ) ` ( f ` n ) ) ) |
41 |
23
|
ffvelrnda |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. A ) -> ( ( k e. A |-> B ) ` x ) e. CC ) |
42 |
|
f1of |
|- ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A ) |
43 |
28 42
|
syl |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) --> A ) |
44 |
|
fvco3 |
|- ( ( f : ( 1 ... ( # ` A ) ) --> A /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) = ( ( k e. A |-> B ) ` ( f ` n ) ) ) |
45 |
43 44
|
sylan |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) = ( ( k e. A |-> B ) ` ( f ` n ) ) ) |
46 |
40 27 28 41 45
|
fsum |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ x e. A ( ( k e. A |-> B ) ` x ) = ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) ) |
47 |
39 46
|
syl5eqr |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ k e. A B = ( seq 1 ( + , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) ) |
48 |
38 47
|
eqtr4d |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) |
49 |
48
|
expr |
|- ( ( ph /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) ) |
50 |
49
|
exlimdv |
|- ( ( ph /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) ) |
51 |
50
|
expimpd |
|- ( ph -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) ) |
52 |
|
fz1f1o |
|- ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) ) |
53 |
1 52
|
syl |
|- ( ph -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) ) |
54 |
14 51 53
|
mpjaod |
|- ( ph -> ( CCfld gsum ( k e. A |-> B ) ) = sum_ k e. A B ) |