Theorem esumpr

Description: Extended sum over a pair. (Contributed by Thierry Arnoux, 2-Jan-2017)

	Ref	Expression
Hypotheses	esumpr.1	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐶 = 𝐷 )
	esumpr.2	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐸 )
	esumpr.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	esumpr.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	esumpr.5	⊢ ( 𝜑 → 𝐷 ∈ ( 0 [,] +∞ ) )
	esumpr.6	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,] +∞ ) )
	esumpr.7	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion	esumpr	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 +e 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		esumpr.1	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐶 = 𝐷 )
2		esumpr.2	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐶 = 𝐸 )
3		esumpr.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		esumpr.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5		esumpr.5	⊢ ( 𝜑 → 𝐷 ∈ ( 0 [,] +∞ ) )
6		esumpr.6	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,] +∞ ) )
7		esumpr.7	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
8		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
9		esumeq1	⊢ ( { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } ) → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = Σ* 𝑘 ∈ ( { 𝐴 } ∪ { 𝐵 } ) 𝐶 )
10	8 9	mp1i	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = Σ* 𝑘 ∈ ( { 𝐴 } ∪ { 𝐵 } ) 𝐶 )
11		nfv	⊢ Ⅎ 𝑘 𝜑
12		nfcv	⊢ Ⅎ 𝑘 { 𝐴 }
13		nfcv	⊢ Ⅎ 𝑘 { 𝐵 }
14		snex	⊢ { 𝐴 } ∈ V
15	14	a1i	⊢ ( 𝜑 → { 𝐴 } ∈ V )
16		snex	⊢ { 𝐵 } ∈ V
17	16	a1i	⊢ ( 𝜑 → { 𝐵 } ∈ V )
18		disjsn2	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
19	7 18	syl	⊢ ( 𝜑 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
20		elsni	⊢ ( 𝑘 ∈ { 𝐴 } → 𝑘 = 𝐴 )
21	20 1	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 } ) → 𝐶 = 𝐷 )
22	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 } ) → 𝐷 ∈ ( 0 [,] +∞ ) )
23	21 22	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 } ) → 𝐶 ∈ ( 0 [,] +∞ ) )
24		elsni	⊢ ( 𝑘 ∈ { 𝐵 } → 𝑘 = 𝐵 )
25	24 2	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐵 } ) → 𝐶 = 𝐸 )
26	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐵 } ) → 𝐸 ∈ ( 0 [,] +∞ ) )
27	25 26	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐵 } ) → 𝐶 ∈ ( 0 [,] +∞ ) )
28	11 12 13 15 17 19 23 27	esumsplit	⊢ ( 𝜑 → Σ* 𝑘 ∈ ( { 𝐴 } ∪ { 𝐵 } ) 𝐶 = ( Σ* 𝑘 ∈ { 𝐴 } 𝐶 +e Σ* 𝑘 ∈ { 𝐵 } 𝐶 ) )
29	1 3 5	esumsn	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝐴 } 𝐶 = 𝐷 )
30	2 4 6	esumsn	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝐵 } 𝐶 = 𝐸 )
31	29 30	oveq12d	⊢ ( 𝜑 → ( Σ* 𝑘 ∈ { 𝐴 } 𝐶 +e Σ* 𝑘 ∈ { 𝐵 } 𝐶 ) = ( 𝐷 +e 𝐸 ) )
32	10 28 31	3eqtrd	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 +e 𝐸 ) )