This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsummulc1

Description: A finite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsummulc2.1 
|- ( ph -> A e. Fin )
fsummulc2.2 
|- ( ph -> C e. CC )
fsummulc2.3 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fsummulc1 
|- ( ph -> ( sum_ k e. A B x. C ) = sum_ k e. A ( B x. C ) )

Proof

Step Hyp Ref Expression
1 fsummulc2.1 
 |-  ( ph -> A e. Fin )
2 fsummulc2.2 
 |-  ( ph -> C e. CC )
3 fsummulc2.3 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 1 2 3 fsummulc2 
 |-  ( ph -> ( C x. sum_ k e. A B ) = sum_ k e. A ( C x. B ) )
5 1 3 fsumcl 
 |-  ( ph -> sum_ k e. A B e. CC )
6 5 2 mulcomd 
 |-  ( ph -> ( sum_ k e. A B x. C ) = ( C x. sum_ k e. A B ) )
7 2 adantr 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
8 3 7 mulcomd 
 |-  ( ( ph /\ k e. A ) -> ( B x. C ) = ( C x. B ) )
9 8 sumeq2dv 
 |-  ( ph -> sum_ k e. A ( B x. C ) = sum_ k e. A ( C x. B ) )
10 4 6 9 3eqtr4d 
 |-  ( ph -> ( sum_ k e. A B x. C ) = sum_ k e. A ( B x. C ) )