LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The divergence and curl of a cross product

Statement

Let $U \subseteq R^{3}$ be open and let $F, G : U \to R^{3}$ be $C^{1}$ . Then $F \times G$ is $C^{1}$ on $U$ and

$div (F \times G) = ⟨ curl F, G ⟩ - ⟨ F, curl G ⟩,$

$curl (F \times G) = (div G) F - (div F) G + D F G - D G F .$

Here $D F G$ denotes the map $U \to R^{3}$ whose $i$ th coordinate at $p$ is $\sum_{j < 3} \partial_{j} F_{i} (p) G_{j} (p)$ , that is, the Jacobian matrix of $F$ at $p$ applied to the vector $G (p)$ , and $D G F$ is defined the same way with the roles of $F$ and $G$ exchanged. The operators are those of Divergence and curl of a $C^{1}$ vector field, the cross product is that of The cross product in $R^{3}$ , the inner product that of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and the Jacobian matrix that of The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case.

Facts & Assumptions

Given: The open set $U \subseteq R^{3}$ and the $C^{1}$ maps $F, G : U \to R^{3}$ of the Statement, with coordinates named $x, y, z$ .

[F1]

For $u = (u_{x}, u_{y}, u_{z})$ and $v = (v_{x}, v_{y}, v_{z})$ in $R^{3}$ , $u \times v = (u_{y} v_{z} - u_{z} v_{y}, u_{z} v_{x} - u_{x} v_{z}, u_{x} v_{y} - u_{y} v_{x})$ (The cross product in $R^{3}$ ).

[F2]

The divergence of a $C^{1}$ field $F$ on an open $U \subseteq R^{n}$ is $div F = \sum_{i < n} \partial_{i} F_{i}$ (Divergence and curl of a $C^{1}$ vector field).

[F3]

The curl of a $C^{1}$ field $F$ on an open $U \subseteq R^{3}$ is $curl F = (\partial_{y} F_{z} - \partial_{z} F_{y}, \partial_{z} F_{x} - \partial_{x} F_{z}, \partial_{x} F_{y} - \partial_{y} F_{x})$ (Divergence and curl of a $C^{1}$ vector field).

[F4]

For $x, y \in R^{m}$ , $⟨ x, y ⟩ = \sum_{k < m} x_{k} y_{k}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F5]

If every partial derivative $\partial_{j} f_{i} (a)$ of $f : U \to R^{n}$ exists, the Jacobian matrix is $J f (a) = (\partial_{j} f_{i} (a))_{i < n, j < m}$ (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[L1]

For real functions of one real variable differentiable at a point, $f g$ is differentiable there and $(f g)^{'} = f^{'} g + f g^{'}$ (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L2]

If $f$ is totally differentiable at $a$ then $\partial_{j} f (a) = D f (a) e_{j}$ , and the matrix of $D f (a)$ is $J f (a)$ (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[L3]

The cross product is bilinear and alternating (The cross product is bilinear, alternating, and orthogonal to both factors).

Proof

technique · direct

1.1

By [F1] the three coordinates of $F \times G$ are $F_{y} G_{z} - F_{z} G_{y}$ , $F_{z} G_{x} - F_{x} G_{z}$ and $F_{x} G_{y} - F_{y} G_{x}$ . Each is a difference of products of $C^{1}$ scalars, so by [L1] applied in each coordinate direction each has continuous first partial derivatives, given by $\partial_{j} (F_{a} G_{b}) = (\partial_{j} F_{a}) G_{b} + F_{a} \partial_{j} G_{b}$ ; hence $F \times G$ is $C^{1}$ and both sides of both identities are defined.

givenF1L1

2.1

Expanding $div (F \times G) = \partial_{x} (F_{y} G_{z} - F_{z} G_{y}) + \partial_{y} (F_{z} G_{x} - F_{x} G_{z}) + \partial_{z} (F_{x} G_{y} - F_{y} G_{x})$ by step 1.1 gives twelve terms. Those carrying a derivative of $F$ are $(\partial_{y} F_{z} - \partial_{z} F_{y}) G_{x} + (\partial_{z} F_{x} - \partial_{x} F_{z}) G_{y} + (\partial_{x} F_{y} - \partial_{y} F_{x}) G_{z}$ , which is $⟨ curl F, G ⟩$ by [F3] and [F4]; those carrying a derivative of $G$ are $- F_{x} (\partial_{y} G_{z} - \partial_{z} G_{y}) - F_{y} (\partial_{z} G_{x} - \partial_{x} G_{z}) - F_{z} (\partial_{x} G_{y} - \partial_{y} G_{x})$ , which is $- ⟨ F, curl G ⟩$ . This is the first identity.

step 1.1L1F2F3F4algebra

2.2

By [F3] and step 1.1 the first coordinate of $curl (F \times G)$ is $\partial_{y} (F_{x} G_{y} - F_{y} G_{x}) - \partial_{z} (F_{z} G_{x} - F_{x} G_{z})$ , that is $(\partial_{y} F_{x}) G_{y} + F_{x} \partial_{y} G_{y} - (\partial_{y} F_{y}) G_{x} - F_{y} \partial_{y} G_{x} - (\partial_{z} F_{z}) G_{x} - F_{z} \partial_{z} G_{x} + (\partial_{z} F_{x}) G_{z} + F_{x} \partial_{z} G_{z}$ . Adding and subtracting $F_{x} \partial_{x} G_{x}$ and $G_{x} \partial_{x} F_{x}$ regroups this as $F_{x} div G - G_{x} div F + ((\partial_{x} F_{x}) G_{x} + (\partial_{y} F_{x}) G_{y} + (\partial_{z} F_{x}) G_{z}) - (F_{x} \partial_{x} G_{x} + F_{y} \partial_{y} G_{x} + F_{z} \partial_{z} G_{x})$ , using [F2] for the two divergences and [F5] for the two bracketed sums.

step 1.1L1F3F2F5L2algebra

2.3

The same computation in the second coordinate gives $\partial_{z} (F_{y} G_{z} - F_{z} G_{y}) - \partial_{x} (F_{x} G_{y} - F_{y} G_{x})$ , which after adding and subtracting $F_{y} \partial_{y} G_{y}$ and $G_{y} \partial_{y} F_{y}$ is $F_{y} div G - G_{y} div F + \sum_{j < 3} (\partial_{j} F_{y}) G_{j} - \sum_{j < 3} F_{j} \partial_{j} G_{y}$ ; in the third coordinate it gives $\partial_{x} (F_{z} G_{x} - F_{x} G_{z}) - \partial_{y} (F_{y} G_{z} - F_{z} G_{y})$ , which after adding and subtracting $F_{z} \partial_{z} G_{z}$ and $G_{z} \partial_{z} F_{z}$ is $F_{z} div G - G_{z} div F + \sum_{j < 3} (\partial_{j} F_{z}) G_{j} - \sum_{j < 3} F_{j} \partial_{j} G_{z}$ .

step 1.1L1F3F2F5L2algebra

3.1

In steps 2.2 and 2.3 the sums $\sum_{j < 3} (\partial_{j} F_{i}) G_{j}$ and $\sum_{j < 3} F_{j} \partial_{j} G_{i}$ are the $i$ th coordinates of $D F G$ and of $D G F$ : by [F5] the $i$ th row of the Jacobian matrix of $F$ is $(\partial_{j} F_{i})_{j < 3}$ , and by [L2] that matrix is the matrix of the total derivative, so applying it to the vector $G$ produces exactly that sum coordinate by coordinate.

step 2.2step 2.3F5L2algebra

4.1

Substituting step 3.1 into steps 2.2 and 2.3 gives the three coordinates of $(div G) F - (div F) G + D F G - D G F$ , which is the second identity; with step 2.1 both assertions hold at every point of $U$ , and by [L3] both sides of each are unchanged in form when $F$ and $G$ are replaced by linear combinations, since the cross product is bilinear.

step 2.1step 3.1L3∎

Remarks

Where the alternating law is visible. Taking $G = F$ makes $F \times F = 0$ by [L3], and both identities then read $0 = 0$ : in the first because $⟨ curl F, F ⟩ - ⟨ F, curl F ⟩ = 0$ , and in the second because the four terms cancel in pairs.
Only first derivatives are used. Both identities hold for $C^{1}$ fields; nothing here interchanges two partial derivatives, which is why no $C^{2}$ hypothesis appears.

Depends on

Used by

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. Feldman, A. Rechnitzer and E. Yeager, CLP-4 Vector Calculus (University of British Columbia), Theorem 4.1.5 (standard reference, not scraped)
M. Corral, Vector Calculus, chapter 4 (LibreTexts) (standard reference, not scraped)