Linear dependence of two vectors is a necessary and sufficient condition for an equality

Question

This is an example in the textbook.

To prove: for any real number** $a_1, a_2, \cdots, a_n, b_1, b_2, \cdots b_n$, linear dependence of the two vectors $\left(a_1, a_2, \cdots, a_n\right)$ and $\left(b_1, b_2, \cdots, b_n\right)$ is a necessary and sufficient condition for the equality:

$\left(a_1^2+a_2^2+\cdots+a_n^2\right)\left(b_1^2+b_2^2+\cdots+b_n^2\right)=\left(a_1 b_1+a_2 b_2+\cdots+a_n b_n\right)^2$

I take a three-dimensional vector as an example to prove its necessity:

Clear["Global`*"];
listA = Table[a[i], {i, 1, 3}];
listB = m*listA;

Refine[Reduce[
  Sum[a[i]^2, {i, 1, 3}]*Sum[(m*a[j])^2, {j, 1, 3}] == 
   Sum[a[k]*m*a[k], {k, 1, 3}]^2], 
 m ∈ Reals && a[1] ∈ Reals && 
  a[2] ∈ Reals && a[3] ∈ Reals]

True

But I cannot prove its sufficiency:

Clear["Global`*"];
listA = Table[a[i], {i, 1, 3}];
listB = Table[b[i], {i, 1, 3}];
sol = Solve[
   Sum[a[i]^2, {i, 1, 3}]*Sum[b[j]^2, {j, 1, 3}] == 
    Sum[a[k]*b[k], {k, 1, 3}]^2, listA, Reals][[1]]
ResourceFunction["LinearlyIndependent"][{listA, listB}] /. sol

$\left\{\mathrm{a}[2] \rightarrow \frac{\mathrm{a}[1] \times \mathrm{b}[2]}{\mathrm{b}[1]}, \mathrm{a}[3] \rightarrow \frac{\mathrm{a}[1] \times \mathrm{b}[1] \times \mathrm{b}[3]+\frac{a[1] b[2]^2 \mathrm{~b}[3]}{\mathrm{b}[1]}}{\mathrm{b}[1]^2+\mathrm{b}[2]^2}\right\}$

True if condition...

ResourceFunction["LinearlyIndependent"][{listA, listB}] /. sol should give False to prove that listA and listB are linearly dependent.

How can I modify this code?

Answer 1

You can do some simplifications before computing matrix rank

u = {listA, listB} /. sol // Simplify
MatrixRank[u]
(*1*)

Matrix rank is smaller than the number of vectors, therefore, they are linearly dependent.

Answer 2

Create two linearly dependent symbolic vectors:

va = Array[Subscript[a, #] &, 3];
vb = lam  va;

Now, the left side of your equation is the product of the norm square of va and vb. The right side is the square of the scalar product:

(va . va) (vb . vb) == (va . vb)^2 // Simplify

(* True *)