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

Metamath Proof Explorer

Theorem sumpair

Description: Sum of two distinct complex values. The class expression for A and B normally contain free variable k to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses sumpair.1 
|- ( ph -> F/_ k D )
sumpair.3 
|- ( ph -> F/_ k E )
sumupair.1 
|- ( ph -> A e. V )
sumupair.2 
|- ( ph -> B e. W )
sumupair.3 
|- ( ph -> D e. CC )
sumupair.4 
|- ( ph -> E e. CC )
sumupair.5 
|- ( ph -> A =/= B )
sumupair.8 
|- ( ( ph /\ k = A ) -> C = D )
sumupair.9 
|- ( ( ph /\ k = B ) -> C = E )
Assertion sumpair 
|- ( ph -> sum_ k e. { A , B } C = ( D + E ) )

Proof

Step Hyp Ref Expression
1 sumpair.1 
 |-  ( ph -> F/_ k D )
2 sumpair.3 
 |-  ( ph -> F/_ k E )
3 sumupair.1 
 |-  ( ph -> A e. V )
4 sumupair.2 
 |-  ( ph -> B e. W )
5 sumupair.3 
 |-  ( ph -> D e. CC )
6 sumupair.4 
 |-  ( ph -> E e. CC )
7 sumupair.5 
 |-  ( ph -> A =/= B )
8 sumupair.8 
 |-  ( ( ph /\ k = A ) -> C = D )
9 sumupair.9 
 |-  ( ( ph /\ k = B ) -> C = E )
10 disjsn2 
 |-  ( A =/= B -> ( { A } i^i { B } ) = (/) )
11 7 10 syl 
 |-  ( ph -> ( { A } i^i { B } ) = (/) )
12 df-pr 
 |-  { A , B } = ( { A } u. { B } )
13 12 a1i 
 |-  ( ph -> { A , B } = ( { A } u. { B } ) )
14 prfi 
 |-  { A , B } e. Fin
15 14 a1i 
 |-  ( ph -> { A , B } e. Fin )
16 elpri 
 |-  ( k e. { A , B } -> ( k = A \/ k = B ) )
17 5 adantr 
 |-  ( ( ph /\ k = A ) -> D e. CC )
18 8 17 eqeltrd 
 |-  ( ( ph /\ k = A ) -> C e. CC )
19 6 adantr 
 |-  ( ( ph /\ k = B ) -> E e. CC )
20 9 19 eqeltrd 
 |-  ( ( ph /\ k = B ) -> C e. CC )
21 18 20 jaodan 
 |-  ( ( ph /\ ( k = A \/ k = B ) ) -> C e. CC )
22 16 21 sylan2 
 |-  ( ( ph /\ k e. { A , B } ) -> C e. CC )
23 11 13 15 22 fsumsplit 
 |-  ( ph -> sum_ k e. { A , B } C = ( sum_ k e. { A } C + sum_ k e. { B } C ) )
24 nfv 
 |-  F/ k ph
25 1 24 8 3 5 sumsnd 
 |-  ( ph -> sum_ k e. { A } C = D )
26 2 24 9 4 6 sumsnd 
 |-  ( ph -> sum_ k e. { B } C = E )
27 25 26 oveq12d 
 |-  ( ph -> ( sum_ k e. { A } C + sum_ k e. { B } C ) = ( D + E ) )
28 23 27 eqtrd 
 |-  ( ph -> sum_ k e. { A , B } C = ( D + E ) )