Enveloping Algebra $U(L \oplus L')$ I'm having trouble understanding part of a proof of the following statement

Let $L,L'$ be Lie algebras and $L \oplus L'$ their direct sum.  Then $$ U(L \oplus L') \cong U(L) \otimes U(L')$$

Let $i_L : L \to U(L)$ denote the natural inclusion into the enveloping algebra, and similarly for $i_{L'}$ and $i_{L \oplus L'}$.  The proof begins by defining a morphism
$\varphi:U(L \oplus L') \to U(L) \otimes U(L')$ by first defining a Lie algebra morphism $f:L \oplus L' \to U(L) \otimes U(L')$ by
$$f(x,x') = i_L(x) \otimes 1 + 1 \otimes i_{L'}(x')$$
Then, $\varphi$ is defined so that $\varphi \circ i_{L \oplus L'} = f$ using the universality of the enveloping algebra.
The inverse map is defined $\psi:U(L) \otimes U(L') \to U(L \oplus L')$ by
$$\psi(a \otimes a') = \psi_1(a)\psi_2(a')$$ where $\psi_1(x) = i_{L \oplus L'}(x,0)$ and $\psi_2(x) = i_{L \oplus L'}(0,x)$
The part I have the problem with is when they show that $\psi \circ \varphi$ is the identity on the image of $L \oplus L'$ in $U(L \oplus L')$.   The calculation given is, for $x \in L, x' \in L'$,
$$\psi(\varphi(x,x')) = \psi(x \otimes 1) + \psi(1 \otimes x') = i_{L \oplus L'}((x,0) + (0,x')) = i_{L \oplus L'}(x,x')$$
I don't really get how the calculation of $\psi(x \otimes 1)$ is done.  If I attempt myself, it comes out
$$\psi(x \otimes 1) = \psi_1(x)\psi_2(1) = i_{L \oplus L'}((x,0) \otimes (0,1)) = ~?$$
so I guess I don't understand how the tensor product $(x,0) \otimes (0,1)$ is simplified in $U(L \oplus L')$.  I'm sure it's something completely basic, but I'd appreciate if someone could explain it.
 A: While general nonsense, as indicated by Qiaochu, does prove the statement, one can do something meaningful instead (as usual :-) )
For example, suppose that $B=\{v_i\}_{i\in I}$ and $B'=\{w_j\}_{j\in J}$ are vector-space bases of $L$ and $L'$, respectively, and that we pick arbitrary total orderings on the index sets $I$ and $J$. Then the Poincaré-Birkhoff-Witt theorem tells us that the set $\tilde B$ of elements of $U(L)$ of the form $$v_{i_1}v_{i_2}\cdots v_{i_p}$$ with $p\geq0$, all the $i_k$ in $I$ and $i_1\leq i_2\leq\cdots\leq i_p$, is a basis of $U(L)$. Of course, the same theorem gives us a similar basis $\tilde B'$ for $U(L)$, constructed from $L'$.
Now obviously $B''=B\cup B'$ is a basis for $L\oplus L'$, which we can totally order extending the orders of $B$ and $B'$ with $B'$ larger than $B$ (in other words, doing the «ordinal sum») and we can do the same construction to construct a basis $\tilde B''$ for $U(L\otimes L')$.
This makes it clear how to define a map $U(L\oplus L')\to U(L)\otimes U(L')$ which is an isomorphism of vector spaces, and it is easy to see that it is in fact a map of algebras.

A working general non-sense argument is the following: $\def\Lie{\operatorname{Lie}}$


*

*an algebra map $U(L)\otimes U(L')\to A$ to some algebra $A$ is the same (in view of universal properties of the tensor product of algebras0 as a pair of algebra maps $U(L)\to A$ and $U(L')\to A$ whose images commute, 

*which is the same (in view of the universal property of the
enveloping algebra) as a pair of Lie algebra maps $L\to \Lie(A)$ and
$L'\to \Lie(A)$ (where $\Lie(A)$ is $A$ viewed as a Lie algebra with
its commutator bracket) whose images commute

*which is the same as a Lie algebra map $L\oplus L'\to \Lie(A)$, in view of the universal product of the direct product of Lie algebras,

*which is the same as an associative algebra map $U(L\oplus L')\to A$.


From this one gets an isomorphism of functors from $\hom_{\mathrm{Alg}}(U(L)\otimes U(L'),\mathord-)$ to $\hom_{\mathrm{Alg}}(U(L\oplus L'),\mathord-)$. Yoneda's lemma then gives us an isomorphism like you want.
A: The maps $\psi_1$ and $\psi_2$ are supposed to be thought of as the obvious inclusions
$$\begin{cases}\psi_1:U(L)\,\hookrightarrow U(L\oplus L') \\ \psi_2: U(L')\hookrightarrow U(L\oplus L')\end{cases}$$
Thus e.g. $\psi(x\otimes 1_{U(L')})=\psi_1(x)\psi_2(1_{U(L')})=i_{L\oplus L'}(x,0)1_{U(L\oplus L')}=i_{L\oplus L'}(x,0)$.

Of course, the isomorphism $U(L\oplus L')\cong U(L)\otimes U(L')$ should be "obvious": an element in the first of the form $a_1\cdots a_n$ can be decomposed as $(u_1+v_1)\cdots(u_n+v_n)$ with $u_i\in L$, $v_i\in L'$, which can be expanded and rearranged into monomials of the form $u_{i_1}\cdots u_{i_l} v_{j_1}\cdots v_{j_r}$ (because we have the relation $[u,v]=0$ for all $u\in L,v\in L'$, allowing $u$s and $v$s to be slid across each other without issue), which corresponds to $u_{i_1}\cdots u_{i_l}\otimes v_{j_1}\cdots v_{j_r}$ in $U(L)\otimes U(L')$. How to go back from $U(L)\otimes U(L')$ to $U(L\oplus L')$ should be even more clear: just erase the $\otimes$ symbol everywhere. (We have been slightly abusive, viewing $L$ and $L'$ as subsets of $L\oplus L'$.)
Note this is very near to the fact that direct sums distribute through tensor products (why?).
