Metamath Proof Explorer


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 φ _ k D
sumpair.3 φ _ k E
sumupair.1 φ A V
sumupair.2 φ B W
sumupair.3 φ D
sumupair.4 φ E
sumupair.5 φ A B
sumupair.8 φ k = A C = D
sumupair.9 φ k = B C = E
Assertion sumpair φ k A B C = D + E

Proof

Step Hyp Ref Expression
1 sumpair.1 φ _ k D
2 sumpair.3 φ _ k E
3 sumupair.1 φ A V
4 sumupair.2 φ B W
5 sumupair.3 φ D
6 sumupair.4 φ E
7 sumupair.5 φ A B
8 sumupair.8 φ k = A C = D
9 sumupair.9 φ k = B C = E
10 disjsn2 A B A B =
11 7 10 syl φ A B =
12 df-pr A B = A B
13 12 a1i φ A B = A B
14 prfi A B Fin
15 14 a1i φ A B Fin
16 elpri k A B k = A k = B
17 5 adantr φ k = A D
18 8 17 eqeltrd φ k = A C
19 6 adantr φ k = B E
20 9 19 eqeltrd φ k = B C
21 18 20 jaodan φ k = A k = B C
22 16 21 sylan2 φ k A B C
23 11 13 15 22 fsumsplit φ k A B C = k A C + k B C
24 nfv k φ
25 1 24 8 3 5 sumsnd φ k A C = D
26 2 24 9 4 6 sumsnd φ k B C = E
27 25 26 oveq12d φ k A C + k B C = D + E
28 23 27 eqtrd φ k A B C = D + E