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 coordinate rotation matrices $R_{z} (a)$ and $R_{y} (a)$ : values in $S O (3)$ , composition law, and derivatives

Statement

For $a \in R$ define, in the standard basis of $R^{3}$ , $R_{z} (a) : = (\begin{array}{ccc} \cos a & - \sin a & 0 \\ \sin a & \cos a & 0 \\ 0 & 0 & 1 \end{array}), R_{y} (a) : = (\begin{array}{ccc} \cos a & 0 & \sin a \\ 0 & 1 & 0 \\ - \sin a & 0 & \cos a \end{array}) \in M_{3} (R) .$ Then:

$R_{z} (a) \in S O (3)$ and $R_{y} (a) \in S O (3)$ for every $a$ (The orthogonal group $O (3)$ and the rotation group $S O (3)$ ), $R_{z} (a) e_{3} = e_{3}$ and $R_{y} (a) e_{2} = e_{2}$ , and $R_{z} (0) = R_{y} (0) = I_{3}$ .
$R_{z} (a) R_{z} (b) = R_{z} (a + b)$ and $R_{y} (a) R_{y} (b) = R_{y} (a + b)$ for all $a, b \in R$ .
For every differentiable $a : I \to R$ on an interval $I \subseteq R$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), the matrix-valued curves $t \mapsto R_{z} (a (t))$ and $t \mapsto R_{y} (a (t))$ are differentiable with $(R_{z} \circ a)^{'} = a^{'} R_{z} (a) [e_{3}]_{\times} = a^{'} [e_{3}]_{\times} R_{z} (a), (R_{y} \circ a)^{'} = a^{'} R_{y} (a) [e_{2}]_{\times} = a^{'} [e_{2}]_{\times} R_{y} (a),$ where $[e_{3}]_{\times}, [e_{2}]_{\times}$ are the cross-product matrices of The skew-matrix/cross-product correspondence $[ω]_{\times} z = ω \times z$ and its conjugation law $R [ω]_{\times} R^{T} = [R ω]_{\times}$ .

Facts & Assumptions

Given: Reals $a, b$ , matrices $R_{z} (a), R_{y} (a)$ as displayed, and a differentiable $a : I \to R$ .

[L1]

$\sin$ and $\cos$ are differentiable with $(\sin)^{'} = \cos$ , $(\cos)^{'} = - \sin$ , and satisfy the addition formulas $\sin (a + b) = \sin a \cos b + \cos a \sin b$ , $\cos (a + b) = \cos a \cos b - \sin a \sin b$ and the Pythagorean identity $\sin^{2} a + \cos^{2} a = 1$ ; also $\sin (- a) = - \sin a$ and $\cos (- a) = \cos a$ The derivatives of sine and cosine are cosine and minus sine, The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine, Sine and cosine defined by their real power series.

[L2]

Matrix product and transpose are entrywise operations: $(A B)_{i j} = \sum_{k} A_{i k} B_{k j}$ and $(A^{T})_{i j} = A_{j i}$ ; $S O (3) = {R : R^{T} R = I_{3}, \det R = 1}$ and these elements form a subgroup of $G L_{3} (R)$ 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 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}$ .

[L3]

The determinant is multiplicative and $\det I_{3} = 1$ ; for a block-triangular matrix the determinant is the product of the determinant of the leading block and the remaining diagonal entry For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix.

[L4]

The chain rule and the algebra of derivatives hold for real functions; a matrix-valued curve is differentiable exactly when all entries are, and its derivative is the entrywise derivative The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , 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$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations.

[L5]

$[e_{3}]_{\times}$ and $[e_{2}]_{\times}$ are the skew matrices of $ω = e_{3}$ and $ω = e_{2}$ ; in particular $[e_{3}]_{\times} = (\begin{array}{ccc} 0 & - 1 & 0 \\ 1 & 0 & 0 \\ 0 & 0 & 0 \end{array})$ and $[e_{2}]_{\times} = (\begin{array}{ccc} 0 & 0 & 1 \\ 0 & 0 & 0 \\ - 1 & 0 & 0 \end{array})$ The skew-matrix/cross-product correspondence $[ω]_{\times} z = ω \times z$ and its conjugation law $R [ω]_{\times} R^{T} = [R ω]_{\times}$ , The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations.

Proof

technique · direct

1.1givenL1L2L3algebra

Entrywise, $R_{z} (a)^{T} R_{z} (a)$ has diagonal entries $\cos^{2} a + \sin^{2} a = 1$ , $1$ , $1$ and off-diagonal entries $\mp \cos a \sin a \pm \sin a \cos a = 0$ ; hence $R_{z} (a) \in O (3)$ , and expanding the determinant along the third row gives $\det R_{z} (a) = \det (\begin{array}{cc} \cos a & - \sin a \\ \sin a & \cos a \end{array}) = (\cos a) (\cos a) - (- \sin a) (\sin a) = 1$ , so $R_{z} (a) \in S O (3)$ , with $R_{z} (a) e_{3} = e_{3}$ read off the third column.

1.2givenL1L2L3algebra

Similarly $R_{y} (a)^{T} R_{y} (a) = I_{3}$ and $\det R_{y} (a) = \det (\begin{array}{cc} \cos a & \sin a \\ - \sin a & \cos a \end{array}) = 1$ , so $R_{y} (a) \in S O (3)$ , and $R_{y} (a) e_{2} = e_{2}$ is its second column. $R_{z} (0) = R_{y} (0) = I_{3}$ because $\cos 0 = 1$ and $\sin 0 = 0$ .

1.3givenL1L2algebra

The $(1, 1)$ entry of $R_{z} (a) R_{z} (b)$ is $\cos a \cos b - \sin a \sin b = \cos (a + b)$ , the $(1, 2)$ entry is $- \cos a \sin b - \sin a \cos b = - \sin (a + b)$ , the $(2, 1)$ entry is $\sin a \cos b + \cos a \sin b = \sin (a + b)$ , the $(2, 2)$ entry is $- \sin a \sin b + \cos a \cos b = \cos (a + b)$ , and the remaining entries are $0, 0, 1$ ; hence $R_{z} (a) R_{z} (b) = R_{z} (a + b)$ by [L1].

1.4givenL1L2algebra

The analogous four planar entries of $R_{y} (a) R_{y} (b)$ equal $\cos (a + b), 0, \sin (a + b)$ and $1$ in the corresponding positions, so $R_{y} (a) R_{y} (b) = R_{y} (a + b)$ by [L1].

1.5givenL1L4L5algebra

If $a : I \to R$ is differentiable, entrywise differentiation using [L1] and [L4] gives $(R_{z} \circ a)^{'} = a^{'} (\begin{array}{ccc} - \sin a & - \cos a & 0 \\ \cos a & - \sin a & 0 \\ 0 & 0 & 0 \end{array}) .$ Direct multiplication of $a^{'} R_{z} (a)$ with $[e_{3}]_{\times}$ from [L5] gives the same matrix: its $(1, 1), (1, 2), (2, 1), (2, 2)$ entries are respectively $- a^{'} \sin a, - a^{'} \cos a, a^{'} \cos a, - a^{'} \sin a$ , and all remaining entries are zero. Thus $(R_{z} \circ a)^{'} = a^{'} R_{z} (a) [e_{3}]_{\times}$ .

1.6givenL1L4L5algebra

The same comparison for $R_{y} (a (t))$ : the derivative matrix has entries $- a^{'} \sin a$ at $(1, 1)$ , $a^{'} \cos a$ at $(1, 3)$ , $- a^{'} \cos a$ at $(3, 1)$ , $- a^{'} \sin a$ at $(3, 3)$ and $0$ in the second row and column, which is exactly $a^{'} R_{y} (a) [e_{2}]_{\times}$ by [L5]; hence $(R_{y} \circ a)^{'} = a^{'} R_{y} (a) [e_{2}]_{\times}$ .

2.1step 1.51.6givenL1L2L5algebra∎

Since $R_{z} (a)$ commutes with $[e_{3}]_{\times}$ and $R_{y} (a)$ commutes with $[e_{2}]_{\times}$ , as direct entrywise multiplication using [L1] shows, the two alternative forms $a^{'} [e_{3}]_{\times} R_{z} (a)$ and $a^{'} [e_{2}]_{\times} R_{y} (a)$ of clause 3 hold as well.

The coordinate rotation matrices $R_{z} (a)$ and $R_{y} (a)$ : values in $S O (3)$ , composition law, and derivatives

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

The coordinate rotation matrices Rz(a)Rz​(a) and Ry(a)Ry​(a): values in SO(3)SO(3), composition law, and derivatives

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

The coordinate rotation matrices $R_{z} (a)$ and $R_{y} (a)$ : values in $S O (3)$ , composition law, and derivatives