The theorem you are looking for is setsum_delta
:
finite ?S ⟹
(∑k∈?S. if k = ?a then ?b k else 0) =
(if ?a ∈ ?S then ?b ?a else 0)
If you write k = i
instead of i = k
in your sum, it can even be solved automatically:
have "(∑k∈UNIV. if k = i then (B $ i $ j) else 0) = B $ i $ j"
by (simp add: setsum_delta)
The find_theorems
command is very useful for this. If you type
find_theorems "∑_∈_. if _ then _ else _"
You get setsum_delta
as one of the matches – that's how I found it.