Theorem sumpair

Description: Sum of two distinct complex values. The class expression for A and B normally contain free variable k to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		sumpair.1	|- ( ph -> F/_ k D )
2		sumpair.3	|- ( ph -> F/_ k E )
3		sumupair.1	|- ( ph -> A e. V )
4		sumupair.2	|- ( ph -> B e. W )
5		sumupair.3	|- ( ph -> D e. CC )
6		sumupair.4	|- ( ph -> E e. CC )
7		sumupair.5	|- ( ph -> A =/= B )
8		sumupair.8	|- ( ( ph /\ k = A ) -> C = D )
9		sumupair.9	|- ( ( ph /\ k = B ) -> C = E )
10		disjsn2	|- ( A =/= B -> ( { A } i^i { B } ) = (/) )
11	7 10	syl	|- ( ph -> ( { A } i^i { B } ) = (/) )
12		df-pr	|- { A , B } = ( { A } u. { B } )
13	12	a1i	|- ( ph -> { A , B } = ( { A } u. { B } ) )
14		prfi	|- { A , B } e. Fin
15	14	a1i	|- ( ph -> { A , B } e. Fin )
16		elpri	|- ( k e. { A , B } -> ( k = A \/ k = B ) )
17	5	adantr	|- ( ( ph /\ k = A ) -> D e. CC )
18	8 17	eqeltrd	|- ( ( ph /\ k = A ) -> C e. CC )
19	6	adantr	|- ( ( ph /\ k = B ) -> E e. CC )
20	9 19	eqeltrd	|- ( ( ph /\ k = B ) -> C e. CC )
21	18 20	jaodan	|- ( ( ph /\ ( k = A \/ k = B ) ) -> C e. CC )
22	16 21	sylan2	|- ( ( ph /\ k e. { A , B } ) -> C e. CC )
23	11 13 15 22	fsumsplit	|- ( ph -> sum_ k e. { A , B } C = ( sum_ k e. { A } C + sum_ k e. { B } C ) )
24		nfv	|- F/ k ph
25	1 24 8 3 5	sumsnd	|- ( ph -> sum_ k e. { A } C = D )
26	2 24 9 4 6	sumsnd	|- ( ph -> sum_ k e. { B } C = E )
27	25 26	oveq12d	|- ( ph -> ( sum_ k e. { A } C + sum_ k e. { B } C ) = ( D + E ) )
28	23 27	eqtrd	|- ( ph -> sum_ k e. { A , B } C = ( D + E ) )