Theorem: Curl of Curl is Gradient of Divergence minus Laplacian

Let $\map {\R^3} {x, y, z}$ denote the real Cartesian space of $3$ dimensions.
Let $\mathbf V$ be a vector field on $\R^3$.
Then:
:$\curl \curl \mathbf V = \grad \operatorname {div} \mathbf V - \nabla^2 \mathbf V$
where:
:$\curl$ denotes the curl operator
:$\operatorname {div}$ denotes the divergence operator
:$\grad$ denotes the gradient operator
:$\nabla^2 \mathbf V$ denotes the Laplacian.

Proof:
From Curl Operator on Vector Space is Cross Product of Del Operator, and Divergence Operator on Vector Space is Dot Product of Del Operator and the definition of the gradient operator:
{{begin-eqn}}
{{eqn | l = \curl \mathbf V
      | r = \nabla \times \mathbf V
}}
{{eqn | l = \operatorname {div} \mathbf V
      | r = \nabla \cdot \mathbf V
}}
{{eqn | l = \grad \operatorname {div} \mathbf V
      | r = \map \nabla {\nabla \cdot \mathbf V}
}}
{{end-eqn}}
where $\nabla$ denotes the del operator.
Hence we are to demonstrate that:
:$\nabla \times \paren {\nabla \times \mathbf V} = \map \nabla {\nabla \cdot \mathbf V} - \nabla^2 \mathbf V$
Let $\mathbf V$ be expressed as a vector-valued function on $\mathbf V$:
:$\mathbf V := \tuple {\map {V_x} {\mathbf r}, \map {V_y} {\mathbf r}, \map {V_z} {\mathbf r} }$
where $\mathbf r = \tuple {x, y, z}$ is the position vector of an arbitrary point in $R$.
Let $\tuple {\mathbf i, \mathbf j, \mathbf k}$ be the standard ordered basis on $\R^3$.
{{begin-eqn}}
{{eqn | l = \nabla \times \paren {\nabla \times \mathbf V}
      | r = \nabla \times \paren {\paren {\dfrac {\partial V_z} {\partial y} - \dfrac {\partial V_y} {\partial z} } \mathbf i + \paren {\dfrac {\partial V_x} {\partial z} - \dfrac {\partial V_z} {\partial x} } \mathbf j + \paren {\dfrac {\partial V_y} {\partial x} - \dfrac {\partial V_x} {\partial y} } \mathbf k}
      | c = {{Defof|Curl Operator}}
}}
{{eqn | r = \paren {\map {\dfrac \partial {\partial y} } {\dfrac {\partial V_y} {\partial x}  - \dfrac {\partial V_x} {\partial y} } - \map {\dfrac \partial {\partial z} } {\dfrac {\partial V_x} {\partial z} - \dfrac {\partial V_z} {\partial x} } } \mathbf i
      | c = {{Defof|Curl Operator}}
}}
{{eqn | o = 
      | ro= +
      | r = \paren {\map {\dfrac \partial {\partial z} } {\dfrac {\partial V_z} {\partial y} - \dfrac {\partial V_y} {\partial z} } - \map {\dfrac \partial {\partial x} } {\dfrac {\partial V_y} {\partial x} - \dfrac {\partial V_x} {\partial y} } } \mathbf j
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {\map {\dfrac \partial {\partial x} } {\dfrac {\partial V_x} {\partial z} - \dfrac {\partial V_z} {\partial x} } - \map {\dfrac \partial {\partial y} } {\dfrac {\partial V_z} {\partial y} - \dfrac {\partial V_y} {\partial z} } } \mathbf k
      | c = 
}}
{{eqn | r = \paren {\dfrac {\partial^2 V_y} {\partial y \partial x} - \dfrac {\partial^2 V_x} {\partial y^2} - \dfrac {\partial^2 V_x} {\partial z^2} + \dfrac {\partial^2 V_z} {\partial z \partial x} } \mathbf i
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {\dfrac {\partial^2 V_z} {\partial z \partial y} - \dfrac {\partial^2 V_y} {\partial z^2} - \dfrac {\partial^2 V_y} {\partial x^2} + \dfrac {\partial^2 V_x} {\partial x \partial y} } \mathbf j
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {\dfrac {\partial^2 V_x} {\partial x \partial z} - \dfrac {\partial^2 V_z} {\partial x^2} - \dfrac {\partial^2 V_z} {\partial y^2} + \dfrac {\partial^2 V_y} {\partial y \partial z} } \mathbf k
      | c = 
}}
{{eqn | r = \paren {\paren {\dfrac {\partial^2 V_y} {\partial y \partial x} + \dfrac {\partial^2 V_z} {\partial z \partial x} } - \paren {\dfrac {\partial^2 V_x} {\partial y^2} + \dfrac {\partial^2 V_x} {\partial z^2} } } \mathbf i
      | c = rearranging
}}
{{eqn | o = 
      | ro= +
      | r = \paren {\paren {\dfrac {\partial^2 V_x} {\partial x \partial y} + \dfrac {\partial^2 V_z} {\partial z \partial y} } - \paren {\dfrac {\partial^2 V_y} {\partial x^2} + \dfrac {\partial^2 V_y} {\partial z^2} } } \mathbf j
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {\paren {\dfrac {\partial^2 V_x} {\partial x \partial z} + \dfrac {\partial^2 V_y} {\partial y \partial z} } - \paren {\dfrac {\partial^2 V_z} {\partial x^2} + \dfrac {\partial^2 V_z} {\partial y^2} } } \mathbf k
      | c = 
}}
{{eqn | r = \paren {\paren {\dfrac {\partial^2 V_x} {\partial x^2} + \dfrac {\partial^2 V_y} {\partial y \partial x} + \dfrac {\partial^2 V_z} {\partial z \partial x} } - \paren {\dfrac {\partial^2 V_x} {\partial x^2} + \dfrac {\partial^2 V_x} {\partial y^2} + \dfrac {\partial^2 V_x} {\partial z^2} } } \mathbf i
      | c = adding and subtracting equal terms
}}
{{eqn | o = 
      | ro= +
      | r = \paren {\paren {\dfrac {\partial^2 V_x} {\partial x \partial y} + \dfrac {\partial^2 V_y} {\partial y^2} + \dfrac {\partial^2 V_z} {\partial z \partial y} } - \paren {\dfrac {\partial^2 V_y} {\partial x^2} + \dfrac {\partial^2 V_y} {\partial y^2} + \dfrac {\partial^2 V_y} {\partial z^2} } } \mathbf j
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {\paren {\dfrac {\partial^2 V_x} {\partial x \partial z} + \dfrac {\partial^2 V_y} {\partial y \partial z} + \dfrac {\partial^2 V_z} {\partial z^2} } - \paren {\dfrac {\partial^2 V_z} {\partial x^2} + \dfrac {\partial^2 V_z} {\partial y^2} + \dfrac {\partial^2 V_z} {\partial z^2} } } \mathbf k
      | c = 
}}
{{eqn | r = \paren {\mathbf i \dfrac \partial {\partial x} + \mathbf j \dfrac \partial {\partial y} + \mathbf k \dfrac \partial {\partial z} } \paren {\dfrac {\partial V_x} {\partial x} + \dfrac {\partial V_y} {\partial y} + \dfrac {\partial V_z} {\partial z} }
      | c = factoring
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\paren {\dfrac {\partial^2} {\partial x^2} + \dfrac {\partial^2} {\partial y^2} + \dfrac {\partial^2} {\partial z^2} } \paren {V_x \mathbf i + V_y \mathbf j + V_z \mathbf k} }
      | c = 
}}
{{eqn | r = \map \nabla {\nabla \cdot \mathbf V} - \nabla^2 \mathbf V
      | c = {{Defof|Del Operator}}
}}
{{end-eqn}}
{{qed}}