# Prove $R^\top R = I_3$ and find skew-symmetric matrix $R^\top \dot R$

Consider the following operator defined over unit vectors of $$\mathbb{R}^3$$:

$$R(u,v) = (u\cdot v)I_3 + hat(u\times v) + \dfrac{(u\times v)\otimes (u\times v)}{1+u\cdot v}$$

R = Dot[u, v]*I3 + Hat[Cross[u, v]] + TensorProduct[Cross[u, v], Cross[u, v]]/(1 + Dot[u, v])


where $$hat$$ or Hat is the hat operator.

It can be shown that for $$u,v$$ on the unit sphere, $$R\in SO(3)$$. That means that $$R^\top R = I_3$$. Now, assume $$u,v$$ depends on time $$t$$, such that $$\forall t\in\mathbb{R},\ u(t),v(t)$$ remain in the unit sphere of $$\mathbb{R}^3$$. Let $$\dot R$$ denote the derivative of $$t\mapsto R(u(t),v(t))$$. Taking the derivative of $$R^\top R = I_3$$ wrt $$t$$ yields that $$\dot R^\top R$$ is a skew-symmetric matrix. It can hence be written in the form $$\dot R^\top R= \hat{\omega}$$ with $$\omega\in\mathbb{R}^3$$.

My goal is to find such a $$\omega$$. I managed to express $$\omega$$ by providing explicitly the components of $$u,v$$ (u = {u1, u2, u3}; v = {v1, v2, v3}) but that is a very long expression, that would be more compact with the non-explicit form of u,v.

I am not even able to show have Mathematica show that Transpose[R].R is the identity matrix of $$\mathbb{R}^3$$, probably because I don't manage to use the fact the u, v are unit vectors.

Here is how far I got:

$Assumptions = Flatten[{{(u | v) \[Element] Vectors[3, Reals], Dot[u, v] \[Element] Reals, I3 \[Element] Matrices[{3, 3}, Reals, Symmetric[{1, 2}]], Hat[Cross[u, v]] \[Element] Matrices[{3, 3}, Reals, Antisymmetric[{1, 2}]]}}] r = Dot[u, v]*I3 + Hat[Cross[u, v]] + TensorProduct[Cross[u, v], Cross[u, v]]/(1 + Dot[u, v]) TensorReduce[Transpose[r].r] //. m___.I3 :> m //. I3.m___ :> m //. MatrixPower[I3, n_Integer] :> I3 (* should simplify to Identity when u and v are unit vectors *) So: • How to show that $$R^\top R = I_3$$? • How to compute $$R^\top \dot R$$? (without expanding the expressions of unit vectors u,v.) Edit For those interested: thanks to Andrea's answer, I was able to find a compact formula: $$R^\top \dot R = \hat{\omega}$$ with $$\omega = \Big(-w [v\ \ u] + ((a-1)I_3 - \dfrac{1}{a} \hat{w} + \dfrac{1}{a}\hat{w}^\top \hat{w})[-\hat v\ \ \hat u]\Big)\begin{bmatrix} u' \\ v'\end{bmatrix},$$ where $$a=1+u\cdot v$$. That would be so nice if there were a way of having Mathematica compute that directly! • This is likely not the solution you want: With[{u = {u1, u2, u3}/Sqrt[u1^2 + u2^2 + u3^2], v = {v1, v2, v3}/Sqrt[v1^2 + v2^2 + v3^2]}, Transpose[#] . # &[Dot[u, v] IdentityMatrix + HodgeDual[Cross[u, v]] + TensorProduct[Cross[u, v], Cross[u, v]]/(1 + Dot[u, v])]] // FullSimplify; it might be a good start for someone else, tho. – J. M.'s ennui Feb 22 at 16:09 • @J.M. Thanks for pointing out HodgeDual. There should be a minus sign before HodgeDual but that gives$I_3$in both cases because of symmetry in$u, v$. Actually the "explicit approach" might work provided it is possible to go back to a compact form, which I have not managed yet. – anderstood Feb 22 at 17:19 • This problem is best solved with pencil and paper. You will just get frustrated attempting to formalize, but even if you manage, the method will not be general enough to use for other problems. – yarchik Feb 22 at 22:05 • @yarchik Indeed, I think I am getting good progress by hand. Mathematica can be useful to check the final result. But I find it very frustrating that I cannot have it compute the result for me! – anderstood Feb 22 at 23:13 • @J.M. Edited for clarification. – anderstood Feb 24 at 12:28 ## 2 Answers My method of solving this in a manner, that does not require loads of computation and with an acceptable number of terms is using a little bit of tensor algebra. The fundamental steps are: 1. Express $$R, R'$$ as tensors 2. Calculate $$R^T \otimes R'$$ 3. Expand the expression 4. Take the traces between the 2nd and 3rd vector of each 4-tensor 5. Calculate the vector $$\omega$$ by projecting the resulting 2-tensor onto the ($$SO(3)$$-irreducable) subspace of skew-symmetric 2-tensors (i.e. matrices) with the standard scalar product. Steps 1 and 3 are equivalent to a matrix-matrix multiplication. Using the tensor product instead of writing everything in terms of matrices allows us to keep the calculation coordinate-free as long as possible, which greatly simplifies the endeavour. Step 0: We start with some definitions: • $$w:= u\times v$$ • Identity matrix as tensor (i.e. the casimir element): $$\Omega:= \sum_{i=1}^3 b_i \otimes b_i$$ for any orthonormal basis set $$\{b_1,b_2,b_3\}$$, which looks basis dependent at first, but actually is not • $$u.v$$ shall be a variable called udotv some calculations: • $$\frac{\partial}{\partial t}hat(w(t)) = hat(\frac{\partial}{\partial t}w(t))$$ for $$w(t) \in \mathbb{R}^3$$ • $$hat(v)^T = - hat(v)$$ • except for the $$hat$$-operator, $$R(u,v)$$ consists of symmetric tensors, so transposing it only changes the sign of the $$hat$$-operator to arrive with the variables • hat[_] as stand-in for HodgeDual[_], which will be used in the end (hence the $$+1=-1 \cdot -1$$ for $$R^T$$ in front of hat[_]) • rtensor as $$R^T$$ • rtensorprime as $$R'$$ at the initial definitions: rtensor[t_] = udotv[t] \[CapitalOmega] + hat[w[t]] + w[t]\[TensorProduct]w[t]/( 1 + udotv[t]) rtensorprime[t_] = D[ udotv[t] \[CapitalOmega] + w[t]\[TensorProduct]w[t]/(1 + udotv[t]), t] - hat[D[w[t], t] ]  Step 1 & Step 2 and some simplifications of the tensor product: Expand[rtensor[t]\[TensorProduct]rtensorprime[t] ]//. {(a_ + b_)\[TensorProduct] c_ -> a\[TensorProduct]c + b\[TensorProduct]c, a_\[TensorProduct](b_ + c_) -> a\[TensorProduct]b + a\[TensorProduct]c}  Step 3 I have done by hand. Identify all 4th-order tensors and calculate their traces. Mathematically, it is sufficient to identify the following equalities ($$w,w_1,w_2,w_3,w_4\in\mathbb{R}^3$$): • $$tr_{2,3}(\Omega \otimes w) = w$$, $$tr_{2,3}(\Omega \otimes \Omega)= \Omega$$ • $$tr_{2,3}(w_1\otimes w_2\otimes w_3 \otimes w_4) = (w_2.w_3)\ w_1\otimes w_4$$ • $$tr_{2,3}(hat(w_1)\otimes w_3 \otimes w_4) = (w_1\times w_3)\otimes w_4$$, $$tr_{2,3}(w_1\otimes w_2\otimes hat(w_3)) = -w_1\otimes(w_3\times w_2)$$ Telling Mathematica, that these expressions hold, is a bit more finnicky. In principle, one could calculate all possibilities, or try some generalized expressions. But since the expression from Step 2 is not too complex, I was happy by just defining specific replacement rules: omegatraces = {(\[CapitalOmega] udotv[t])\[TensorProduct]a_ -> udotv[t] a, a_\[TensorProduct](\[CapitalOmega] Derivative[udotv][t]) -> Derivative[udotv][t] a }; wtraces = {w[t]\[TensorProduct]w[t]\[TensorProduct] (w[t]\[TensorProduct]w[t] Derivative[udotv][t]) -> Derivative[udotv][t] wdotw w[t]\[TensorProduct]w[t], w[t]\[TensorProduct]w[t]\[TensorProduct]w[ t]\[TensorProduct]Derivative[w][t] -> wdotw w[t]\[TensorProduct]Derivative[w][t], w[t]\[TensorProduct]w[t]\[TensorProduct]Derivative[w][ t]\[TensorProduct]w[t] -> wdotwprime w[t]\[TensorProduct]w[t]}; hattraces = {hat[ w[t]]\[TensorProduct](w[t]\[TensorProduct]w[t] Derivative[ udotv][t]) -> Derivative[udotv][t] cross[w[t], w[t]]\[TensorProduct]w[t], hat[w[t]]\[TensorProduct]w[t]\[TensorProduct]Derivative[w][ t] -> cross[w[t], w[t]]\[TensorProduct]Derivative[w][t], hat[w[t]]\[TensorProduct]Derivative[w][t]\[TensorProduct]w[ t] -> cross[w[t], Derivative[w][t]]\[TensorProduct]w[t], w[t]\[TensorProduct]w[t]\[TensorProduct]hat[ Derivative[w][t]] -> -w[t]\[TensorProduct]cross[ Derivative[w][t], w[t]]};  I intentionally used the undefined function cross instead of Cross due to personal preference whilst looking at the output and so I can immediately use $$w\times w = 0$$ (which holds for any vector). This will also be replaced in the very end. Applying the replacement lists in two steps: rptensr = FullSimplify[ Expand[rtensor[t]\[TensorProduct]rtensorprime[ t] ] //. {(a_ + b_)\[TensorProduct] c_ -> a\[TensorProduct]c + b\[TensorProduct]c, a_\[TensorProduct](b_ + c_) -> a\[TensorProduct]b + a\[TensorProduct]c} /. omegatraces /. wtraces] rptensr2 = rptensr /. hattraces /. cross[a_, a_] -> 0  The result is -hat[w[t]]\[TensorProduct]hat[Derivative[w][t]] + (1/((1 + udotv[t])^3))(-(1 + udotv[t]) (-wdotwprime w[t]\[TensorProduct]w[t] - w[t]\[TensorProduct]Derivative[w][t] (wdotw + udotv[t] + udotv[t]^2) + (1 + udotv[t]) (-cross[w[t], Derivative[w][t]]\[TensorProduct]w[t] - w[t]\[TensorProduct]cross[Derivative[w][t], w[t]] + udotv[t] (-Derivative[w][t]\[TensorProduct]w[t] + hat[Derivative[w][t]] (1 + udotv[t])))) + (hat[ w[t]] (1 + udotv[t])^3 + \[CapitalOmega] udotv[ t] (1 + udotv[t])^3 + w[t]\[TensorProduct]w[t] (1 - wdotw + udotv[t])) Derivative[ udotv][t])  which I rewrote by hand in preparation for the next step: (-HodgeDual[w].HodgeDual[wp] + 1/(1 + udotv)^3 (-(1 + udotv) (-wdotwprime w\[TensorProduct]w - (udotv + udotv^2 + wdotw) w\[TensorProduct]wp + (1 + udotv) (-w\[TensorProduct]Cross[wp, w] - Cross[w, wp]\[TensorProduct]w + udotv ((1 + udotv) HodgeDual[wp] - wp\[TensorProduct]w))) + (udotv (1 + udotv)^3 \[CapitalOmega] + (1 + udotv)^3 HodgeDual[ w] + (1 + udotv - wdotw) w\[TensorProduct]w) Derivative[ udotv]))  Here I finally took the trace between the two $$hat$$-tensors. Step 4: Look at the output of MatrixForm[HodgeDual[{\[Omega]1[t], \[Omega]2[t], \[Omega]3[t]}]]. It is clear, that this matrix can be seen as the linear combination of three basis matrices, each with coefficients $$\omega_i$$. Since we know, that $$R^T R'$$ must be from the same subspace of matrices, we will now calculate its coordinates with an orthogonal projection. Since our subspace is irreducable, any scalar product can be used for this, so we will simply use the standard scalar product for tensors. \[Omega]3[t] = 1/2 FullSimplify[ With[{w = {w1, w2, w3}, \[CapitalOmega] = IdentityMatrix, wp = {wp1, wp2, wp3}}, TensorContract[ TensorProduct[ Normal[(-HodgeDual[w].HodgeDual[wp] + 1/(1 + udotv)^3 (-(1 + udotv) (-wdotwprime w\[TensorProduct]w - (udotv + udotv^2 + wdotw) w\[TensorProduct]wp + (1 + udotv) (-w\[TensorProduct]Cross[wp, w] - Cross[w, wp]\[TensorProduct]w + udotv ((1 + udotv) HodgeDual[wp] - wp\[TensorProduct]w))) + (udotv (1 + udotv)^3 \[CapitalOmega] + (1 + udotv)^3 HodgeDual[ w] + (1 + udotv - wdotw) w\[TensorProduct]w) Derivative[udotv]))] , {{0, 1, 0}, {-1, 0, 0}, {0, 0, 0}}], {{1, 3}, {2, 4}}] ]] \[Omega]2[t] = 1/2 FullSimplify[ With[{w = {w1, w2, w3}, \[CapitalOmega] = IdentityMatrix, wp = {wp1, wp2, wp3}}, TensorContract[ TensorProduct[ Normal[(-HodgeDual[w].HodgeDual[wp] + 1/(1 + udotv)^3 (-(1 + udotv) (-wdotwprime w\[TensorProduct]w - (udotv + udotv^2 + wdotw) w\[TensorProduct]wp + (1 + udotv) (-w\[TensorProduct]Cross[wp, w] - Cross[w, wp]\[TensorProduct]w + udotv ((1 + udotv) HodgeDual[wp] - wp\[TensorProduct]w))) + (udotv (1 + udotv)^3 \[CapitalOmega] + (1 + udotv)^3 HodgeDual[ w] + (1 + udotv - wdotw) w\[TensorProduct]w) Derivative[udotv]))] , {{0, 0, -1}, {0, 0, 0}, {1, 0, 0}}], {{1, 3}, {2, 4}}] ]] \[Omega]1[t] = 1/2 FullSimplify[ With[{w = {w1, w2, w3}, \[CapitalOmega] = IdentityMatrix, wp = {wp1, wp2, wp3}}, TensorContract[ TensorProduct[ Normal[(-HodgeDual[w].HodgeDual[wp] + 1/(1 + udotv)^3 (-(1 + udotv) (-wdotwprime w\[TensorProduct]w - (udotv + udotv^2 + wdotw) w\[TensorProduct]wp + (1 + udotv) (-w\[TensorProduct]Cross[wp, w] - Cross[w, wp]\[TensorProduct]w + udotv ((1 + udotv) HodgeDual[wp] - wp\[TensorProduct]w))) + (udotv (1 + udotv)^3 \[CapitalOmega] + (1 + udotv)^3 HodgeDual[ w] + (1 + udotv - wdotw) w\[TensorProduct]w) Derivative[udotv]))] , {{0, 0, 0}, {0, 0, 1}, {0, -1, 0}}], {{1, 3}, {2, 4}}] ]]  The factors $$1/2$$ are needed, since the matrices I chose are not normalized. You probably want to simplify the obtained coordinates a bit further, for example: FullSimplify[ FullSimplify[ 2 (1 + udotv)^2 \[Omega]3[t]] /. w2^2 -> wdotw - w1^2 - w3^2 /. w1 w3 wp1 -> wdotwp - w2 w3 wp2 - w3 w3 wp3] /. (w2 wp1 - w1 wp2) -> wpcrossw3  which yields -2 (1 + udotv) wdotwp - 2 (1 + udotv) (udotv + udotv^2 - wdotw) wp3 - ((1 + udotv)^2 + wdotw) wpcrossw3 + 2 (1 + udotv)^2 w3 Derivative[udotv]  I hope this method helps. It certainly is prone to typos and while the approach is somewhat general, the actual implementation requires quite some fenagling by hand. On the plus side: The expressions are still small enough and mostly coordinate-independent. • Very helpful. i) hat[_] as stand-in for HodgeDual[_] -> with that definition of the hat operator, there should be a minus sign. ii) Shouldn't$\omega_1$and$\omega_3$be exchanged, so that$hat([1,0,0]) = E_{1}$(instead of$E_3$) where$E_{1}$is the first element of the basis of antisymmetric matrices? iii) I still do not manage to match the result with the "direct" approach (such as JM's in the comments), even with not sure why yet. – anderstood Feb 28 at 21:42 • iv) Introducing$a=1+u\cdot v$, the whole formula simplifies drastically! It becomes something like$\omega= J.[u', v']$with$J=w.[v,u] + ((1-a)I_3-1/a \hat{w} + \hat{w}^\top \hat{w}).[-\hat{v}, \hat{u}]$. I just need to find the mistake, probably a minor one, and adapt the formula. Note: the brackets denote concatenation. – anderstood Feb 28 at 21:45 • For i), I think you took the minus sign into account since you rtensor is$R^\top$, my bad. – anderstood Feb 28 at 22:07 • regarding ii) You are right, apparently I got the two mixed up somehow – Andrea Mar 1 at 13:49 • Wonderful, it works! The correct expression is:$\omega=\Big(-w.[v,u] + ((a-1)I_3 - 1/a \hat{w} + \hat{w}^\top \hat{w}).[-\hat v, \hat u]\Big).[u'; v']$with$a=1+u\cdot v\$. Note: brackets denote concatenation. That would be so great if Mathematica could find it by itself! – anderstood Mar 1 at 20:40

Starting with suitable definitions of unit vectors, Mathematica allows a fairly direct confirmation of ortogonality

u = {Cos[a] Cos[b], Sin[a] Cos[b], Sin[b]};
v = {Cos[c] Cos[d], Cos[d] Sin[c], Sin[d]};


Confirm that the vectors are indeed units

{u . u, v . v} // Simplify
(* {1, 1} *)


Define the matrix R

R =
u . v IdentityMatrix + HodgeDual[Cross[u, v]] +
TensorProduct[Cross[u, v], Cross[u, v]]/(1 + u . v) // Normal //
Simplify;


Confirm orthogonality

R . Transpose[R] // Simplify
(* {{1, 0, 0}, {0, 1, 0}, {0, 0, 1}} *)

• Very straightforward answer. With a->a[t], b->b[t],... it's possible to evaluate omega=R^t.R'  – Ulrich Neumann Mar 3 at 18:44