Tristan Needham's Visual Complex Analysis contains a proof that the symbolic (i.e. $(a+ib)(c+id) = (ac-bd) + i(bc+ad)$) and geometric (i.e. "multiply the lengths and add the angles") rules for complex multiplication are equivalent (pages 8-10). The proof goes like this:
- Geometric to symbolic: The symbolic rule is determined as soon as we say that $i^2=-1$ and that the distributive property holds, so it suffices to show that these two properties hold. The former is true since $i$ has length $1$ and angle $\pi/2$, so squaring it produces length $1$ and angle $\pi$, i.e. $-1$. The latter is true since rotations and dilations preserve parallelograms.
- Symbolic to geometric: $iz = i(x+iy) = -y + ix$ according to the symbolic rule, so multiplication by $i$ is equivalent to a right-angle rotation. Using the distributive property we then have $(x'+y'i)z = x'z + y'(iz) = x'z + y'(z \text{ rotated by right angle})$. Drawing the picture, the triangle formed by points $(0,0), (x',0), (x',y')$ is now similar to the triangle formed by points $(0,0), x'z, (x'+y'i)z$, which shows that the length has been multiplied by the length of $x'+y'i$ and that the angle has been rotated by the angle of $x'+y'i$.
My basic question is something like: In what sense was the above a proof? How can we formalize what must be shown, and how does the above prove that?
One basic confusion I have is that the structure of the theorem at a high level looks like $A=B$ (symbolic=geometric), and yet we are having to show the equivalence in both directions. If we want to show $A=B$, we only need to show $A=B$ and not $B=A$ also. Maybe another way to state this is that it seems we just need to define complex multiplication in one way, then prove the other rule as a theorem, which seems to require only one direction. So in one sense by showing two directions the above proof seems overkill.
Okay so what are we trying to show? It seems like we have two representations of complex numbers, the algebraic/symbolic one $\mathbf C$ and the geometric one $\mathbf C'$. And we have multiplication $\cdot$ defined on $\mathbf C$, and multiplication $\cdot'$ defined on $\mathbf C'$. We want to show that there is some bijection $f : \mathbf C \to \mathbf C'$ such that $f(z\cdot w) = f(z)\cdot' f(w)$ for all $z,w\in \mathbf C$.
How does the above proof produce such an $f$? The "Geometric to symbolic" direction first shows that $f(i)^2 = f(-1)$. It then shows that $f(z)(f(w) + f(u)) = f(z)f(w) + f(z)f(u)$. If we assume $f$ interacts well with addition and multiplication by real numbers, we have $f(a+ib)f(c+id) = f((ac-bd) + i(ad+bc))$. But are we allowed to assume this? If so it sounds like we are done, and if not then I'm not sure how this direction of the proof is useful. For "Symbolic to geometric" direction I'm not sure how to translate it in terms of $f$.