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 ∈ 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 ⊢ φ → 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 ∈ A B
12 disjsn ⊢ A B ∩ C = ∅ ↔ ¬ C ∈ A B
13 11 12 sylibr ⊢ φ → A B ∩ C = ∅
14 df-tp ⊢ A B C = A B ∪ C
15 14 a1i ⊢ φ → A B C = A B ∪ C
16 tpfi ⊢ A B C ∈ Fin
17 16 a1i ⊢ φ → A B C ∈ 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 ∈ A B C D ∈ ℂ ↔ E ∈ ℂ ∧ F ∈ ℂ ∧ G ∈ ℂ
22 5 21 syl ⊢ φ → ∀ k ∈ A B C D ∈ ℂ ↔ E ∈ ℂ ∧ F ∈ ℂ ∧ G ∈ ℂ
23 4 22 mpbird ⊢ φ → ∀ k ∈ A B C D ∈ ℂ
24 23 r19.21bi ⊢ φ ∧ k ∈ A B C → D ∈ ℂ
25 13 15 17 24 fsumsplit ⊢ φ → ∑ k ∈ A B C D = ∑ k ∈ A B D + ∑ k ∈ C D
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 ∈ A B D = E + F
31 5 simp3d ⊢ φ → C ∈ X
32 4 simp3d ⊢ φ → G ∈ ℂ
33 3 sumsn ⊢ C ∈ X ∧ G ∈ ℂ → ∑ k ∈ C D = G
34 31 32 33 syl2anc ⊢ φ → ∑ k ∈ C D = G
35 30 34 oveq12d ⊢ φ → ∑ k ∈ A B D + ∑ k ∈ C D = E + F + G
36 25 35 eqtrd ⊢ φ → ∑ k ∈ A B C D = E + F + G