Metamath Proof Explorer

Theorem isummulc2

Description: An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005) (Revised by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses isumcl.1 
|- Z = ( ZZ>= ` M )
isumcl.2 
|- ( ph -> M e. ZZ )
isumcl.3 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
isumcl.4 
|- ( ( ph /\ k e. Z ) -> A e. CC )
isumcl.5 
|- ( ph -> seq M ( + , F ) e. dom ~~> )
summulc.6 
|- ( ph -> B e. CC )
Assertion isummulc2 
|- ( ph -> ( B x. sum_ k e. Z A ) = sum_ k e. Z ( B x. A ) )

Proof

Step Hyp Ref Expression
1 isumcl.1 
 |-  Z = ( ZZ>= ` M )
2 isumcl.2 
 |-  ( ph -> M e. ZZ )
3 isumcl.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4 isumcl.4 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
5 isumcl.5 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
6 summulc.6 
 |-  ( ph -> B e. CC )
7 eqidd 
 |-  ( ( ph /\ m e. Z ) -> ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( ( k e. Z |-> ( B x. A ) ) ` m ) )
8 6 adantr 
 |-  ( ( ph /\ k e. Z ) -> B e. CC )
9 8 4 mulcld 
 |-  ( ( ph /\ k e. Z ) -> ( B x. A ) e. CC )
10 9 fmpttd 
 |-  ( ph -> ( k e. Z |-> ( B x. A ) ) : Z --> CC )
11 10 ffvelrnda 
 |-  ( ( ph /\ m e. Z ) -> ( ( k e. Z |-> ( B x. A ) ) ` m ) e. CC )
12 1 2 3 4 5 isumclim2 
 |-  ( ph -> seq M ( + , F ) ~~> sum_ k e. Z A )
13 3 4 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
14 13 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` k ) e. CC )
15 fveq2 
 |-  ( k = m -> ( F ` k ) = ( F ` m ) )
16 15 eleq1d 
 |-  ( k = m -> ( ( F ` k ) e. CC <-> ( F ` m ) e. CC ) )
17 16 rspccva 
 |-  ( ( A. k e. Z ( F ` k ) e. CC /\ m e. Z ) -> ( F ` m ) e. CC )
18 14 17 sylan 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) e. CC )
19 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
20 ovex 
 |-  ( B x. A ) e. _V
21 eqid 
 |-  ( k e. Z |-> ( B x. A ) ) = ( k e. Z |-> ( B x. A ) )
22 21 fvmpt2 
 |-  ( ( k e. Z /\ ( B x. A ) e. _V ) -> ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. A ) )
23 19 20 22 sylancl 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. A ) )
24 3 oveq2d 
 |-  ( ( ph /\ k e. Z ) -> ( B x. ( F ` k ) ) = ( B x. A ) )
25 23 24 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. ( F ` k ) ) )
26 25 ralrimiva 
 |-  ( ph -> A. k e. Z ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. ( F ` k ) ) )
27 nffvmpt1 
 |-  F/_ k ( ( k e. Z |-> ( B x. A ) ) ` m )
28 27 nfeq1 
 |-  F/ k ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( B x. ( F ` m ) )
29 fveq2 
 |-  ( k = m -> ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( ( k e. Z |-> ( B x. A ) ) ` m ) )
30 15 oveq2d 
 |-  ( k = m -> ( B x. ( F ` k ) ) = ( B x. ( F ` m ) ) )
31 29 30 eqeq12d 
 |-  ( k = m -> ( ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. ( F ` k ) ) <-> ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( B x. ( F ` m ) ) ) )
32 28 31 rspc 
 |-  ( m e. Z -> ( A. k e. Z ( ( k e. Z |-> ( B x. A ) ) ` k ) = ( B x. ( F ` k ) ) -> ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( B x. ( F ` m ) ) ) )
33 26 32 mpan9 
 |-  ( ( ph /\ m e. Z ) -> ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( B x. ( F ` m ) ) )
34 1 2 6 12 18 33 isermulc2 
 |-  ( ph -> seq M ( + , ( k e. Z |-> ( B x. A ) ) ) ~~> ( B x. sum_ k e. Z A ) )
35 1 2 7 11 34 isumclim 
 |-  ( ph -> sum_ m e. Z ( ( k e. Z |-> ( B x. A ) ) ` m ) = ( B x. sum_ k e. Z A ) )
36 sumfc 
 |-  sum_ m e. Z ( ( k e. Z |-> ( B x. A ) ) ` m ) = sum_ k e. Z ( B x. A )
37 35 36 eqtr3di 
 |-  ( ph -> ( B x. sum_ k e. Z A ) = sum_ k e. Z ( B x. A ) )