I'm trying to prove the Lagrange identity. There seem to be multiple results with this name, some with slight variations, but the exact identity I have in mind is $$ \left(\sum\limits_{i=1}^n a_i b_i \right)^2 = \left(\sum\limits_{i=1}^n a_i^2\right) \cdot \left(\sum\limits_{i=1}^n b_i^2\right) - \frac{1}{2} \sum\limits_{i=1}^n \sum\limits_{j=1}^n (a_i b_j - a_j b_i)^2. $$ Some versions leave out the factor of $\frac{1}{2}$ and start the second sum at $j=i+1$. I assume these are equivalent, but I haven't checked.
The proof I wrote is: \begin{align*} & \left(\sum\limits_{i=1}^n a_i^2\right) \left(\sum\limits_{i=1}^n b_i^2\right) - \frac{1}{2} \sum\limits_{i=1}^n \sum\limits_{j=1}^n (a_i b_j - a_j b_i)^2 = \left(\sum\limits_{i=1}^n a_i^2\right) \left(\sum\limits_{j=1}^n b_j^2\right) - \frac{1}{2} \sum\limits_{i=1}^n \sum\limits_{j=1}^n (a_i^2 b_j^2 - 2a_i b_j a_j b_i + a_j^2 b_i^2) \\ & = \sum\limits_{i=1}^n \sum\limits_{j=1}^n a_i^2 b_j^2 - \frac{1}{2} \sum\limits_{i=1}^n \sum\limits_{j=1}^n a_i^2 b_j^2 + \sum\limits_{i=1}^n \sum\limits_{j=1}^n a_i a_j b_j b_i - \frac{1}{2} \sum\limits_{i=1}^n \sum\limits_{j=1}^n a_j^2 b_i^2 \\ & = \frac{1}{2} \sum\limits_{i=1}^n \sum\limits_{j=1}^n a_i^2 b_j^2 + \sum\limits_{i=1}^n a_i b_i \sum\limits_{j=1}^n a_j b_j - \frac{1}{2} \sum\limits_{i=1}^n \sum\limits_{j=1}^n a_j^2 b_i^2 \\ & = \left(\sum\limits_{i=1}^n a_i b_i\right)^2. \end{align*}
My biggest concern is from the third line to the fourth. The first and the third sums are identical, except for the choice of indexing, but that doesn't seem to matter. I could have rewrote the product in the first line using $j$ for the sum over $a_j^2$ and $i$ for the sum over $b_i^2$, and I believe the indexing would come out the same. By symmetry, these sums should be equivalent. Is that logic correct?
