Metamath Proof Explorer

Theorem sumtp

Description: A sum over a triple is the sum of the elements. (Contributed by AV, 24-Jul-2020)

Ref Expression
Hypotheses sumtp.e 
|- ( k = A -> D = E )
sumtp.f 
|- ( k = B -> D = F )
sumtp.g 
|- ( k = C -> D = G )
sumtp.c 
|- ( ph -> ( E e. CC /\ F e. CC /\ G e. CC ) )
sumtp.v 
|- ( ph -> ( A e. V /\ B e. W /\ C e. X ) )
sumtp.1 
|- ( ph -> A =/= B )
sumtp.2 
|- ( ph -> A =/= C )
sumtp.3 
|- ( ph -> B =/= C )
Assertion sumtp 
|- ( ph -> sum_ k e. { A , B , C } D = ( ( E + F ) + G ) )

Proof

Step Hyp Ref Expression
1 sumtp.e 
 |-  ( k = A -> D = E )
2 sumtp.f 
 |-  ( k = B -> D = F )
3 sumtp.g 
 |-  ( k = C -> D = G )
4 sumtp.c 
 |-  ( ph -> ( E e. CC /\ F e. CC /\ G e. CC ) )
5 sumtp.v 
 |-  ( ph -> ( A e. V /\ B e. W /\ C e. X ) )
6 sumtp.1 
 |-  ( ph -> A =/= B )
7 sumtp.2 
 |-  ( ph -> A =/= C )
8 sumtp.3 
 |-  ( ph -> B =/= C )
9 7 necomd 
 |-  ( ph -> C =/= A )
10 8 necomd 
 |-  ( ph -> C =/= B )
11 9 10 nelprd 
 |-  ( ph -> -. C e. { A , B } )
12 disjsn 
 |-  ( ( { A , B } i^i { C } ) = (/) <-> -. C e. { A , B } )
13 11 12 sylibr 
 |-  ( ph -> ( { A , B } i^i { C } ) = (/) )
14 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
15 14 a1i 
 |-  ( ph -> { A , B , C } = ( { A , B } u. { C } ) )
16 tpfi 
 |-  { A , B , C } e. Fin
17 16 a1i 
 |-  ( ph -> { A , B , C } e. Fin )
18 1 eleq1d 
 |-  ( k = A -> ( D e. CC <-> E e. CC ) )
19 2 eleq1d 
 |-  ( k = B -> ( D e. CC <-> F e. CC ) )
20 3 eleq1d 
 |-  ( k = C -> ( D e. CC <-> G e. CC ) )
21 18 19 20 raltpg 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A. k e. { A , B , C } D e. CC <-> ( E e. CC /\ F e. CC /\ G e. CC ) ) )
22 5 21 syl 
 |-  ( ph -> ( A. k e. { A , B , C } D e. CC <-> ( E e. CC /\ F e. CC /\ G e. CC ) ) )
23 4 22 mpbird 
 |-  ( ph -> A. k e. { A , B , C } D e. CC )
24 23 r19.21bi 
 |-  ( ( ph /\ k e. { A , B , C } ) -> D e. CC )
25 13 15 17 24 fsumsplit 
 |-  ( ph -> sum_ k e. { A , B , C } D = ( sum_ k e. { A , B } D + sum_ k e. { C } D ) )
26 3simpa 
 |-  ( ( E e. CC /\ F e. CC /\ G e. CC ) -> ( E e. CC /\ F e. CC ) )
27 4 26 syl 
 |-  ( ph -> ( E e. CC /\ F e. CC ) )
28 3simpa 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A e. V /\ B e. W ) )
29 5 28 syl 
 |-  ( ph -> ( A e. V /\ B e. W ) )
30 1 2 27 29 6 sumpr 
 |-  ( ph -> sum_ k e. { A , B } D = ( E + F ) )
31 5 simp3d 
 |-  ( ph -> C e. X )
32 4 simp3d 
 |-  ( ph -> G e. CC )
33 3 sumsn 
 |-  ( ( C e. X /\ G e. CC ) -> sum_ k e. { C } D = G )
34 31 32 33 syl2anc 
 |-  ( ph -> sum_ k e. { C } D = G )
35 30 34 oveq12d 
 |-  ( ph -> ( sum_ k e. { A , B } D + sum_ k e. { C } D ) = ( ( E + F ) + G ) )
36 25 35 eqtrd 
 |-  ( ph -> sum_ k e. { A , B , C } D = ( ( E + F ) + G ) )