A videotaped proof that $e^xe^y$ is a Lie series in $x$ and $y$ is at http://katlas.math.toronto.edu/drorbn/dbnvp/wClips-120418.php, starting around minute 10 and ending near the end of the lecture. You may want to stare at the blackboard shots on the right column before viewing the video.

That proof is very short; it takes an hour mostly because all relevant background is presented. A key ingredient that takes the most time is the computation of the differential of the exponential function, which is not obvious in the non-commutative case, and is worth knowing anyway.

The proof uses the "Euler Trick", which again, is useful elsewhere and worth knowing anyway.

A videotaped proof that $\log e^xe^y$ is a Lie series in $x$ and $y$ is at http://katlas.math.toronto.edu/drorbn/dbnvp/wClips-120418.php, starting around minute 10 and ending near the end of the lecture. You may want to stare at the blackboard shots on the right column before viewing the video.

That proof is very short; it takes an hour mostly because all relevant background is presented. A key ingredient that takes the most time is the computation of the differential of the exponential function, which is not obvious in the non-commutative case, and is worth knowing anyway.

The proof uses the "Euler Trick", which again, is useful elsewhere and worth knowing anyway.