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 ⊢ ( 𝑘 = 𝐴 → 𝐷 = 𝐸 )
sumtp.f ⊢ ( 𝑘 = 𝐵 → 𝐷 = 𝐹 )
sumtp.g ⊢ ( 𝑘 = 𝐶 → 𝐷 = 𝐺 )
sumtp.c ⊢ ( 𝜑 → ( 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ ) )
sumtp.v ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) )
sumtp.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
sumtp.2 ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
sumtp.3 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion sumtp ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝐷 = ( ( 𝐸 + 𝐹 ) + 𝐺 ) )

Proof

Step Hyp Ref Expression
1 sumtp.e ⊢ ( 𝑘 = 𝐴 → 𝐷 = 𝐸 )
2 sumtp.f ⊢ ( 𝑘 = 𝐵 → 𝐷 = 𝐹 )
3 sumtp.g ⊢ ( 𝑘 = 𝐶 → 𝐷 = 𝐺 )
4 sumtp.c ⊢ ( 𝜑 → ( 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ ) )
5 sumtp.v ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) )
6 sumtp.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
7 sumtp.2 ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
8 sumtp.3 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
9 7 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
10 8 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
11 9 10 nelprd ⊢ ( 𝜑 → ¬ 𝐶 ∈ { 𝐴 , 𝐵 } )
12 disjsn ⊢ ( ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ ↔ ¬ 𝐶 ∈ { 𝐴 , 𝐵 } )
13 11 12 sylibr ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ )
14 df-tp ⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
15 14 a1i ⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) )
16 tpfi ⊢ { 𝐴 , 𝐵 , 𝐶 } ∈ Fin
17 16 a1i ⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ∈ Fin )
18 1 eleq1d ⊢ ( 𝑘 = 𝐴 → ( 𝐷 ∈ ℂ ↔ 𝐸 ∈ ℂ ) )
19 2 eleq1d ⊢ ( 𝑘 = 𝐵 → ( 𝐷 ∈ ℂ ↔ 𝐹 ∈ ℂ ) )
20 3 eleq1d ⊢ ( 𝑘 = 𝐶 → ( 𝐷 ∈ ℂ ↔ 𝐺 ∈ ℂ ) )
21 18 19 20 raltpg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝐷 ∈ ℂ ↔ ( 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ ) ) )
22 5 21 syl ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝐷 ∈ ℂ ↔ ( 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ ) ) )
23 4 22 mpbird ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝐷 ∈ ℂ )
24 23 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ) → 𝐷 ∈ ℂ )
25 13 15 17 24 fsumsplit ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝐷 = ( Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐷 + Σ 𝑘 ∈ { 𝐶 } 𝐷 ) )
26 3simpa ⊢ ( ( 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 𝐺 ∈ ℂ ) → ( 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) )
27 4 26 syl ⊢ ( 𝜑 → ( 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ ) )
28 3simpa ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) )
29 5 28 syl ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) )
30 1 2 27 29 6 sumpr ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐷 = ( 𝐸 + 𝐹 ) )
31 5 simp3d ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
32 4 simp3d ⊢ ( 𝜑 → 𝐺 ∈ ℂ )
33 3 sumsn ⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐺 ∈ ℂ ) → Σ 𝑘 ∈ { 𝐶 } 𝐷 = 𝐺 )
34 31 32 33 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐶 } 𝐷 = 𝐺 )
35 30 34 oveq12d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐷 + Σ 𝑘 ∈ { 𝐶 } 𝐷 ) = ( ( 𝐸 + 𝐹 ) + 𝐺 ) )
36 25 35 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝐷 = ( ( 𝐸 + 𝐹 ) + 𝐺 ) )