Metamath Proof Explorer

Theorem fsumconst

Description: The sum of constant terms ( k is not free in B ). (Contributed by NM, 24-Dec-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Assertion fsumconst 
|- ( ( A e. Fin /\ B e. CC ) -> sum_ k e. A B = ( ( # ` A ) x. B ) )

Proof

Step Hyp Ref Expression
1 mul02 
 |-  ( B e. CC -> ( 0 x. B ) = 0 )
2 1 adantl 
 |-  ( ( A e. Fin /\ B e. CC ) -> ( 0 x. B ) = 0 )
3 2 eqcomd 
 |-  ( ( A e. Fin /\ B e. CC ) -> 0 = ( 0 x. B ) )
4 sumeq1 
 |-  ( A = (/) -> sum_ k e. A B = sum_ k e. (/) B )
5 sum0 
 |-  sum_ k e. (/) B = 0
6 4 5 eqtrdi 
 |-  ( A = (/) -> sum_ k e. A B = 0 )
7 fveq2 
 |-  ( A = (/) -> ( # ` A ) = ( # ` (/) ) )
8 hash0 
 |-  ( # ` (/) ) = 0
9 7 8 eqtrdi 
 |-  ( A = (/) -> ( # ` A ) = 0 )
10 9 oveq1d 
 |-  ( A = (/) -> ( ( # ` A ) x. B ) = ( 0 x. B ) )
11 6 10 eqeq12d 
 |-  ( A = (/) -> ( sum_ k e. A B = ( ( # ` A ) x. B ) <-> 0 = ( 0 x. B ) ) )
12 3 11 syl5ibrcom 
 |-  ( ( A e. Fin /\ B e. CC ) -> ( A = (/) -> sum_ k e. A B = ( ( # ` A ) x. B ) ) )
13 eqidd 
 |-  ( k = ( f ` n ) -> B = B )
14 simprl 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN )
15 simprr 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
16 simpllr 
 |-  ( ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ k e. A ) -> B e. CC )
17 simplr 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> B e. CC )
18 elfznn 
 |-  ( n e. ( 1 ... ( # ` A ) ) -> n e. NN )
19 fvconst2g 
 |-  ( ( B e. CC /\ n e. NN ) -> ( ( NN X. { B } ) ` n ) = B )
20 17 18 19 syl2an 
 |-  ( ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( NN X. { B } ) ` n ) = B )
21 13 14 15 16 20 fsum 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ k e. A B = ( seq 1 ( + , ( NN X. { B } ) ) ` ( # ` A ) ) )
22 ser1const 
 |-  ( ( B e. CC /\ ( # ` A ) e. NN ) -> ( seq 1 ( + , ( NN X. { B } ) ) ` ( # ` A ) ) = ( ( # ` A ) x. B ) )
23 22 ad2ant2lr 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( seq 1 ( + , ( NN X. { B } ) ) ` ( # ` A ) ) = ( ( # ` A ) x. B ) )
24 21 23 eqtrd 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ k e. A B = ( ( # ` A ) x. B ) )
25 24 expr 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> sum_ k e. A B = ( ( # ` A ) x. B ) ) )
26 25 exlimdv 
 |-  ( ( ( A e. Fin /\ B e. CC ) /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> sum_ k e. A B = ( ( # ` A ) x. B ) ) )
27 26 expimpd 
 |-  ( ( A e. Fin /\ B e. CC ) -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> sum_ k e. A B = ( ( # ` A ) x. B ) ) )
28 fz1f1o 
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
29 28 adantr 
 |-  ( ( A e. Fin /\ B e. CC ) -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
30 12 27 29 mpjaod 
 |-  ( ( A e. Fin /\ B e. CC ) -> sum_ k e. A B = ( ( # ` A ) x. B ) )