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 ⊢φ→E∈ℂ∧F∈ℂ∧G∈ℂ
sumtp.v ⊢φ→A∈V∧B∈W∧C∈X
sumtp.1 ⊢φ→A≠B
sumtp.2 ⊢φ→A≠C
sumtp.3 ⊢φ→B≠C
Assertion sumtp ⊢φ→∑k∈ABCD=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 ⊢φ→E∈ℂ∧F∈ℂ∧G∈ℂ
5 sumtp.v ⊢φ→A∈V∧B∈W∧C∈X
6 sumtp.1 ⊢φ→A≠B
7 sumtp.2 ⊢φ→A≠C
8 sumtp.3 ⊢φ→B≠C
9 7 necomd ⊢φ→C≠A
10 8 necomd ⊢φ→C≠B
11 9 10 nelprd ⊢φ→¬C∈AB
12 disjsn ⊢AB∩C=∅↔¬C∈AB
13 11 12 sylibr ⊢φ→AB∩C=∅
14 df-tp ⊢ABC=AB∪C
15 14 a1i ⊢φ→ABC=AB∪C
16 tpfi ⊢ABC∈Fin
17 16 a1i ⊢φ→ABC∈Fin
18 1 eleq1d ⊢k=A→D∈ℂ↔E∈ℂ
19 2 eleq1d ⊢k=B→D∈ℂ↔F∈ℂ
20 3 eleq1d ⊢k=C→D∈ℂ↔G∈ℂ
21 18 19 20 raltpg ⊢A∈V∧B∈W∧C∈X→∀k∈ABCD∈ℂ↔E∈ℂ∧F∈ℂ∧G∈ℂ
22 5 21 syl ⊢φ→∀k∈ABCD∈ℂ↔E∈ℂ∧F∈ℂ∧G∈ℂ
23 4 22 mpbird ⊢φ→∀k∈ABCD∈ℂ
24 23 r19.21bi ⊢φ∧k∈ABC→D∈ℂ
25 13 15 17 24 fsumsplit ⊢φ→∑k∈ABCD=∑k∈ABD+∑k∈CD
26 3simpa ⊢E∈ℂ∧F∈ℂ∧G∈ℂ→E∈ℂ∧F∈ℂ
27 4 26 syl ⊢φ→E∈ℂ∧F∈ℂ
28 3simpa ⊢A∈V∧B∈W∧C∈X→A∈V∧B∈W
29 5 28 syl ⊢φ→A∈V∧B∈W
30 1 2 27 29 6 sumpr ⊢φ→∑k∈ABD=E+F
31 5 simp3d ⊢φ→C∈X
32 4 simp3d ⊢φ→G∈ℂ
33 3 sumsn ⊢C∈X∧G∈ℂ→∑k∈CD=G
34 31 32 33 syl2anc ⊢φ→∑k∈CD=G
35 30 34 oveq12d ⊢φ→∑k∈ABD+∑k∈CD=E+F+G
36 25 35 eqtrd ⊢φ→∑k∈ABCD=E+F+G