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 ) )