1: \begin{proof}

2: Apply the controller  \eqref{PID:rigid} to  \eqref{rigid:Z:sys}  to get

3: \begin{align*}

4: \dot Z_s &= -2\coV Z_s,\\

5: \dot Z_k^\vee &=  \Omega, \\

6: \dot \Omega  &=  - K_PZ_k^\vee - K_D\Omega - K_I\int_0^tZ_k^\vee(\tau) d\tau,

7: \end{align*}

8: which is transformed, by differentiation, to

9: \begin{align*}

10: \dot Z_s &= -2\coV Z_s,\\

11: \dddot Z_k^\vee &+ K_D \ddot Z_k^\vee + K_P\dot Z_k^\vee + K_I  Z_k^\vee = 0.

12: \end{align*}

13: It is easy to prove that this linear system is exponentially stable by the Hurwitz condition on the polynomial in \eqref{PID:poly}.

14: This proves the first statement of the theorem. 

15: 

16: The second statement of the theorem can be proven by treating the PID controller \eqref{PID:rigid} as dynamic feedback to the nonlinear system \eqref{rigid:eq}  and then applying  the first statement of this theorem and Theorem \ref{theorem:linear:point:stab}. In this way, the Lyapunov linearization method is rigorously applied.  

17: \end{proof}

18: