Understanding the Sipser-Gacs-Lautemann theorem
First of all, it's not clear to me that every language of the form given by your last formula is in BPP. Fortunately, we only need the reverse direction: every language in BPP can be written in this form. This will show that BPP is contained in $\Sigma_2$. Since BPP is closed under complementation, this will complete the proof. 

Start with a BPP machine with some small error probability. For appropriate $k$ (depending on the error probability), a union bound shows that the formula doesn't hold. The other direction looks more complicated, and this is probably where the other results they prove come in. Basically, you have a set of good random strings covering almost all strings, and you want to cover all of them by finitely many translates of the set. Perhaps that's what these lemmas show.