Theorem sumpr

Description: A sum over a pair is the sum of the elements. (Contributed by Thierry Arnoux, 12-Dec-2016)

	Ref	Expression
Hypotheses	sumpr.1	|- ( k = A -> C = D )
	sumpr.2	|- ( k = B -> C = E )
	sumpr.3	|- ( ph -> ( D e. CC /\ E e. CC ) )
	sumpr.4	|- ( ph -> ( A e. V /\ B e. W ) )
	sumpr.5	|- ( ph -> A =/= B )
Assertion	sumpr	|- ( ph -> sum_ k e. { A , B } C = ( D + E ) )

Proof

Step	Hyp	Ref	Expression
1		sumpr.1	|- ( k = A -> C = D )
2		sumpr.2	|- ( k = B -> C = E )
3		sumpr.3	|- ( ph -> ( D e. CC /\ E e. CC ) )
4		sumpr.4	|- ( ph -> ( A e. V /\ B e. W ) )
5		sumpr.5	|- ( ph -> A =/= B )
6		disjsn2	|- ( A =/= B -> ( { A } i^i { B } ) = (/) )
7	5 6	syl	|- ( ph -> ( { A } i^i { B } ) = (/) )
8		df-pr	|- { A , B } = ( { A } u. { B } )
9	8	a1i	|- ( ph -> { A , B } = ( { A } u. { B } ) )
10		prfi	|- { A , B } e. Fin
11	10	a1i	|- ( ph -> { A , B } e. Fin )
12	1	eleq1d	|- ( k = A -> ( C e. CC <-> D e. CC ) )
13	2	eleq1d	|- ( k = B -> ( C e. CC <-> E e. CC ) )
14	12 13	ralprg	|- ( ( A e. V /\ B e. W ) -> ( A. k e. { A , B } C e. CC <-> ( D e. CC /\ E e. CC ) ) )
15	4 14	syl	|- ( ph -> ( A. k e. { A , B } C e. CC <-> ( D e. CC /\ E e. CC ) ) )
16	3 15	mpbird	|- ( ph -> A. k e. { A , B } C e. CC )
17	16	r19.21bi	|- ( ( ph /\ k e. { A , B } ) -> C e. CC )
18	7 9 11 17	fsumsplit	|- ( ph -> sum_ k e. { A , B } C = ( sum_ k e. { A } C + sum_ k e. { B } C ) )
19	4	simpld	|- ( ph -> A e. V )
20	3	simpld	|- ( ph -> D e. CC )
21	1	sumsn	|- ( ( A e. V /\ D e. CC ) -> sum_ k e. { A } C = D )
22	19 20 21	syl2anc	|- ( ph -> sum_ k e. { A } C = D )
23	4	simprd	|- ( ph -> B e. W )
24	3	simprd	|- ( ph -> E e. CC )
25	2	sumsn	|- ( ( B e. W /\ E e. CC ) -> sum_ k e. { B } C = E )
26	23 24 25	syl2anc	|- ( ph -> sum_ k e. { B } C = E )
27	22 26	oveq12d	|- ( ph -> ( sum_ k e. { A } C + sum_ k e. { B } C ) = ( D + E ) )
28	18 27	eqtrd	|- ( ph -> sum_ k e. { A , B } C = ( D + E ) )