How might one actually prove, in a rigorous way, that the area of a parallelogram is given by the magnitude of the cross product?

Question

In $3$-dimensions, we can compute areas of a parallelograms using the cross product, like so: $$H_2(\{ax+by : a \in [0,1],b \in [0,1]\}) = |x \times y|,$$ where $H_2$ is the $2$-dimensional Hausdorff measure. Of course, it's rarely formalized like this. So much of elementary geometry is never formalized. In any event, the above formula seems like the most reasonable interpretation of this well-known fact.

Question. How would you actually prove such a formula rigorously?

By "prove rigorously" I do not mean draw a persuasive geometric diagram and make a reasonable-sounding argument. Rather, I mean something that could, in principle at least, be formalized in a sufficiently powerful interactive theorem prover one day. A diagram is fine, but please explain how you would actually implement the proof implicitly contained in that diagram.

Answer 1

By elementary linear algebra, the cross product is preserved by rotations. Since rotations are isometries, they also preserve Hausdorff measure, so we may apply a rotation to assume that $x=(u,0,0)$ and $y=(v,w,0)$ for some $u,v,w\in\mathbb{R}$. Similarly, we can multiply by a scalar to assume that $u=1$, since multiplying by a scalar $r$ scales both $H_2$ and the cross product by $r^2$ (if $u=0$ then the parallelogram is just a line segment so it has $2$-dimensional measure $0$). So we may assume we are actually in $\mathbb{R}^2$ rather than $\mathbb{R}^3$ and we want to show the parallelogram spanned by $(1,0)$ and $(v,w)$ has $2$-dimensional measure $|w|$. Also, $2$-dimensional Hausdorff measure on $\mathbb{R}^2$ is just Lebesgue measure.

There are now many ways to proceed. For instance, classical geometric arguments show you can decompose such a parallelogram as a disjoint union of finitely many triangles and then apply isometries to the triangles to get a decomposition of a $|w|\times 1$ rectangle, modulo finitely many line segments. Since line segments have measure zero, this shows that the parallelogram has the same measure as the rectangle. Alternatively, you could use Fubini's theorem: the measure of the parallelogram is the integral of the 1-dimensional measures of its horizontal cross-sections. The cross-section consisting of points whose second coordinate is $t$ is empty unless $t$ is between $0$ and $w$, in which case it is the interval $[vt/w,vt/w+1]$. Since these intervals all have measure $1$, and $t$ can range over an interval of length $|w|$, the measure of the parallelogram is $|w|$.

Answer 2

Here is a possible approach. First, check that for any two vectors $u$, $v$, in $3$-space we have $$|u|^2 \cdot |v|^2 = (u\cdot v)^2 + |u\times v|^2$$ That can be shown using the definitions involving the coordinates of $u$ and $v$. Now, if you also know that $u\cdot v = |u|\cdot |v| \cdot \cos \theta$, and also using $\cos^2 \theta + \sin^2 \theta = 1$ we conclude $$|u\times v | = |u|\cdot |v| \cdot \sin \theta$$ ( $\theta$, the angle between $u$ and $v$, lies in the interval $[0, \pi]$). From here, it may be almost done, assuming that we know what the area of a parallelogram is.