LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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 skew-matrix/cross-product correspondence $[ω]_{\times} z = ω \times z$ and its conjugation law $R [ω]_{\times} R^{T} = [R ω]_{\times}$

Statement

Use the standard basis $(e_{1}, e_{2}, e_{3})$ of $R^{3}$ and coordinates $ω = ω_{1} e_{1} + ω_{2} e_{2} + ω_{3} e_{3}$ (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ , A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis). Define the map $[\cdot]_{\times} : R^{3} \to M_{3} (R)$ by $[ω]_{\times} : = (\begin{array}{ccc} 0 & - ω_{3} & ω_{2} \\ ω_{3} & 0 & - ω_{1} \\ - ω_{2} & ω_{1} & 0 \end{array}) .$ Then:

$[ω]_{\times} z = ω \times z$ for all $ω, z \in R^{3}$ , the cross product being that of The cross product in $R^{3}$ .
$[ω]_{\times}^{T} = - [ω]_{\times}$ for every $ω$ ; the map $ω \mapsto [ω]_{\times}$ is linear and injective, and its image is exactly the set of skew-symmetric matrices of $M_{3} (R)$ . Consequently every skew-symmetric $Ω \in M_{3} (R)$ equals $[ω]_{\times}$ for exactly one $ω$ , namely $ω = (Ω_{32}, Ω_{13}, Ω_{21})$ .
For every $R \in S O (3)$ (The orthogonal group $O (3)$ and the rotation group $S O (3)$ ) and every $ω \in R^{3}$ , $R [ω]_{\times} R^{T} = [R ω]_{\times} .$

Facts & Assumptions

Given: Vectors $ω, z \in R^{3}$ , a skew-symmetric matrix $Ω \in M_{3} (R)$ and a rotation $R \in S O (3)$ .

[L1]

The cross product has coordinates $(u \times v)_{1} = u_{2} v_{3} - u_{3} v_{2}$ , $(u \times v)_{2} = u_{3} v_{1} - u_{1} v_{3}$ , $(u \times v)_{3} = u_{1} v_{2} - u_{2} v_{1}$ in the standard basis, and satisfies $⟨ u \times v, w ⟩ = \det [u v w]$ , where $[u v w]$ is the matrix with these three vectors as columns; moreover $u \times v$ is orthogonal to $u$ and to $v$ The cross product in $R^{3}$ , The cross product is bilinear, alternating, and orthogonal to both factors.

[L2]

Use the owning page's one-based labels: $u_{j} : = u (j - 1)$ , $M_{i j} : = M (i - 1, j - 1)$ , and $e_{j}$ is the standard unit vector at the actual index $j - 1$ , for $i, j \in {1, 2, 3}$ . Relabelling the supplier's product formula gives $(A B)_{i j} = \sum_{k = 1}^{3} A_{i k} B_{k j} = \sum_{r = 0}^{2} A (i - 1, r) B (r, j - 1)$ . Sums are entrywise and $(A^{T})_{i j} = A_{j i}$ ; the transpose is involutive and reverses products The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The transpose $A^{T}$ of a matrix, Transpose is linear and involutive, and $(A B)^{T} = B^{T} A^{T}$ , The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ .

[L3]

The determinant is multiplicative, $\det (A B) = \det A \det B$ , and $\det I_{3} = 1$ For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes.

[L4]

For $R \in S O (3)$ one has $R^{T} R = I_{3}$ , $R R^{T} = I_{3}$ , $\det R = 1$ and $R$ invertible; for all $x, y \in R^{3}$ therefore $⟨ R x, R y ⟩ = ⟨ x, y ⟩$ , since $(R x)^{T} (R y) = x^{T} R^{T} R y = x^{T} y$ The orthogonal group $O (3)$ and the rotation group $S O (3)$ , $S O (3)$ is a subgroup of the general linear group, with $R^{- 1} = R^{T}$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ .

[L5]

The Euclidean inner product is positive definite: if $⟨ x, w ⟩ = 0$ for all $w \in R^{3}$ then $x = 0$ Real and complex inner product spaces, with the inner product linear in the first argument, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ .

[L6]

A matrix is determined by its values on the standard basis: if $B, C \in M_{3} (R)$ satisfy $B z = C z$ for all $z \in R^{3}$ , then $B = C$ , since the $j$ -th column of $B$ is $B e_{j}$ by the product formula [L2] and $(e_{1}, e_{2}, e_{3})$ is a basis The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ , A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis.

Proof

technique · direct

1.1givenL1L2algebra

Comparing coordinates, $([ω]_{\times} z)_{1} = - ω_{3} z_{2} + ω_{2} z_{3} = ω_{2} z_{3} - ω_{3} z_{2} = (ω \times z)_{1}$ , and likewise $([ω]_{\times} z)_{2} = ω_{3} z_{1} - ω_{1} z_{3} = (ω \times z)_{2}$ and $([ω]_{\times} z)_{3} = ω_{1} z_{2} - ω_{2} z_{1} = (ω \times z)_{3}$ , all by [L1] and [L2]; this is clause 1.

1.2givenL2algebra

The displayed matrix is manifestly antisymmetric: $([ω]_{\times}^{T})_{i j} = ([ω]_{\times})_{j i} = - ([ω]_{\times})_{i j}$ for every $i, j$ by [L2]. Hence $[ω]_{\times}^{T} = - [ω]_{\times}$ . Entries are linear functions of $ω$ , so $ω \mapsto [ω]_{\times}$ is linear. If $[ω]_{\times} = 0$ , then the $(1, 3)$ entry gives $ω_{2} = 0$ , the $(2, 3)$ entry gives $ω_{1} = 0$ and the $(1, 2)$ entry gives $ω_{3} = 0$ , so $ω = 0$ : the map is injective.

1.3givenL1L2L3L4L5algebra

Let $u, v, w \in R^{3}$ . By [L4], $⟨ R (u \times v), R w ⟩ = ⟨ u \times v, w ⟩ = \det [u v w]$ by [L1]; by [L2] and [L3], $\det [u v w] = \det (R) \det [u v w] = \det (R [u v w]) = \det [R u R v R w] = ⟨ R u \times R v, R w ⟩$ by [L1] again. Since $R$ is invertible, $R w$ ranges over all of $R^{3}$ as $w$ does, so [L5] gives $R (u \times v) = R u \times R v$ .

2.1step 1.2givenL2algebra

Let $Ω$ be skew-symmetric and put $ω : = (Ω_{32}, Ω_{13}, Ω_{21})$ . Comparing entries with the definition of $[ω]_{\times}$ and using $Ω_{i j} = - Ω_{j i}$ and $Ω_{i i} = 0$ : $[ω]_{\times}$ has $(1, 2)$ entry $- ω_{3} = - Ω_{21} = Ω_{12}$ , $(1, 3)$ entry $ω_{2} = Ω_{13}$ , $(2, 3)$ entry $- ω_{1} = - Ω_{32} = Ω_{23}$ , and the lower-triangular entries follow by skew-symmetry of both matrices; so $Ω = [ω]_{\times}$ . Together with step 1.2 this shows that the image of $ω \mapsto [ω]_{\times}$ is the set of skew-symmetric matrices, with the stated unique preimage; this proves clause 2.

3.1step 1.11.3givenL2L4L6algebra∎

For every $z \in R^{3}$ , $R [ω]_{\times} R^{T} z = R (ω \times (R^{T} z))$ by step 1.1, $= (R ω) \times (R R^{T} z)$ by step 1.3, $= (R ω) \times z$ by [L4], $= [R ω]_{\times} z$ by step 1.1. Hence $R [ω]_{\times} R^{T} = [R ω]_{\times}$ by [L6]; this is clause 3.

The skew-matrix/cross-product correspondence $[ω]_{\times} z = ω \times z$ and its conjugation law $R [ω]_{\times} R^{T} = [R ω]_{\times}$

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

The skew-matrix/cross-product correspondence [ω]×z=ω×z[ω]×​z=ω×z and its conjugation law R[ω]×RT=[Rω]×R[ω]×​RT=[Rω]×​

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

The skew-matrix/cross-product correspondence $[ω]_{\times} z = ω \times z$ and its conjugation law $R [ω]_{\times} R^{T} = [R ω]_{\times}$