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

Metamath Proof Explorer

Theorem fsumneg

Description: Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumneg.1 
|- ( ph -> A e. Fin )
fsumneg.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fsumneg 
|- ( ph -> sum_ k e. A -u B = -u sum_ k e. A B )

Proof

Step Hyp Ref Expression
1 fsumneg.1 
 |-  ( ph -> A e. Fin )
2 fsumneg.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 neg1cn 
 |-  -u 1 e. CC
4 3 a1i 
 |-  ( ph -> -u 1 e. CC )
5 1 4 2 fsummulc2 
 |-  ( ph -> ( -u 1 x. sum_ k e. A B ) = sum_ k e. A ( -u 1 x. B ) )
6 1 2 fsumcl 
 |-  ( ph -> sum_ k e. A B e. CC )
7 6 mulm1d 
 |-  ( ph -> ( -u 1 x. sum_ k e. A B ) = -u sum_ k e. A B )
8 2 mulm1d 
 |-  ( ( ph /\ k e. A ) -> ( -u 1 x. B ) = -u B )
9 8 sumeq2dv 
 |-  ( ph -> sum_ k e. A ( -u 1 x. B ) = sum_ k e. A -u B )
10 5 7 9 3eqtr3rd 
 |-  ( ph -> sum_ k e. A -u B = -u sum_ k e. A B )