Metamath Proof Explorer


Theorem fsumsplitsndif

Description: Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 31-Aug-2018)

Ref Expression
Assertion fsumsplitsndif A Fin X A k A B k A B = k A X B + X / k B

Proof

Step Hyp Ref Expression
1 neldifsnd A Fin X A k A B ¬ X A X
2 disjsn A X X = ¬ X A X
3 1 2 sylibr A Fin X A k A B A X X =
4 uncom A X X = X A X
5 simp2 A Fin X A k A B X A
6 5 snssd A Fin X A k A B X A
7 undif X A X A X = A
8 6 7 sylib A Fin X A k A B X A X = A
9 4 8 eqtr2id A Fin X A k A B A = A X X
10 simp1 A Fin X A k A B A Fin
11 rspcsbela x A k A B x / k B
12 11 zcnd x A k A B x / k B
13 12 expcom k A B x A x / k B
14 13 3ad2ant3 A Fin X A k A B x A x / k B
15 14 imp A Fin X A k A B x A x / k B
16 3 9 10 15 fsumsplit A Fin X A k A B x A x / k B = x A X x / k B + x X x / k B
17 nfcv _ x B
18 nfcsb1v _ k x / k B
19 csbeq1a k = x B = x / k B
20 17 18 19 cbvsumi k A B = x A x / k B
21 17 18 19 cbvsumi k A X B = x A X x / k B
22 17 18 19 cbvsumi k X B = x X x / k B
23 21 22 oveq12i k A X B + k X B = x A X x / k B + x X x / k B
24 16 20 23 3eqtr4g A Fin X A k A B k A B = k A X B + k X B
25 rspcsbela X A k A B X / k B
26 25 zcnd X A k A B X / k B
27 26 3adant1 A Fin X A k A B X / k B
28 sumsns X A X / k B k X B = X / k B
29 5 27 28 syl2anc A Fin X A k A B k X B = X / k B
30 29 oveq2d A Fin X A k A B k A X B + k X B = k A X B + X / k B
31 24 30 eqtrd A Fin X A k A B k A B = k A X B + X / k B