Finite dimensional irreducible representations of a semisimple Lie Algebra separate points of the universal enveloping algebra.

The following is an explicit argument building on the knowledge of the finite-dimensional irreducible representation of ${\mathfrak g}$. At its heart is the non-degeneracy of the Shapovalov-form and the description of its determinant, but I tried to keep the exposition elementary.

Setup: Let ${\mathfrak g}={\mathfrak n}^-\oplus{\mathfrak h}\oplus{\mathfrak n}^+$ be a triangular decomposition of ${\mathfrak g}$ with respect to a Cartan subalgebra ${\mathfrak h}$ of ${\mathfrak g}$ and a choice of positive roots $\Phi^+\subset{\mathfrak h}^{\ast}$. Further, let ${\mathfrak b}:={\mathfrak h}\oplus{\mathfrak n}^+$ be the associated Borel subalgebra. Finally, recall the PBW decomposition ${\mathscr U}{\mathfrak g}\cong{\mathscr U}{\mathfrak n}^-\otimes{\mathscr U}{\mathfrak h}\otimes{\mathscr U}{\mathfrak n}^+$.

It is known (and not hard to show) that every finite-dimensional irreducible representation of ${\mathfrak g}$ is uniquely of the form $L(\lambda)=M(\lambda)/N(\lambda)$, where $\lambda\in{\mathfrak h}^{\ast}$ is dominant integral, i.e. $\lambda(h_\alpha)\in{\mathbb Z}_{\geq 0}$ for all $\alpha\in\Phi^+$, and $M(\lambda) := {\mathscr U}{\mathfrak g}\otimes_{{\mathscr U}{\mathfrak b}} {\mathbb C}_\lambda$ for the $1$-dimensional ${\mathscr U}{\mathfrak b}$-module ${\mathbb C}_\lambda$ given by ${\mathfrak n}^+{\mathbb C}_\lambda = \{0\}$ and ${\mathfrak h}$ acting on ${\mathbb C}_\lambda$ via $\lambda$.

It is important to get the idea of how $M(\lambda)$ and $L(\lambda)$ come about geometrically: The weight space diagram of $M(\lambda)$ is a downwards directed cone rooted in $\lambda$, while the one of $L(\lambda)$ is its largest symmetric subset with respect to the Weyl group action. See here, for example, where the dotted lines indicate the weight cone of $M(\lambda)$, and the solid area is where the weights of $L(\lambda)$ live.

Let's consider the point separation for elements of ${\mathscr U}{\mathfrak n}^-$ first. For those, their action on $M(\lambda)$ is very simple: As a ${\mathscr U}{\mathfrak n}^-$-module, $M(\lambda)\cong {\mathscr U}{\mathfrak n}^-$ with $1\otimes 1\mapsto 1$ because ${\mathscr U}{\mathfrak g}\cong{\mathscr U}{\mathfrak n}^-\otimes{\mathscr U}{\mathfrak h}\otimes{\mathscr U}{\mathfrak n}^+$ by PBW. So no non-zero element of ${\mathscr U}{\mathfrak n}^-$ acts trivially on $M(\lambda)$, because it doesn't kill the highest weight vector $1\otimes 1$. The idea is now to make $\lambda\gg 0$ large enough, for any fixed element of ${\mathscr U}{\mathfrak n}^-\setminus\{0\}$, so that this argument can be carried over to $L(\lambda)$, showing that the element under consideration doesn't annihilate the highest weight vector. Intuitively, this should be possible, because the larger $\lambda$ gets, the further 'away from' $\lambda$ does the submodule $N(\lambda)$ start that is annihilated from $M(\lambda)$ when passing to $L(\lambda)$.

Starting to be precise, you have the following:

Proposition: For any simple root $\alpha\in\Delta$, there is a unique embedding $M(s_\alpha\cdot\lambda)\subset M(\lambda)$, and $$L(\lambda)=M(\lambda)/\sum_{\alpha\in\Delta} M(s_\alpha\cdot\lambda).$$

NB: Pursuing this further, you get the BGG resolution of $L(\lambda)$ in terms of $M(w\cdot \lambda)$, with $w\in W$ in the $l(w)$-th syzygy.

Corollary: If $\mu\preceq\lambda$ (i.e. $\lambda-\mu\in{\mathbb Z}_+\Phi^+$, so $\mu$ is in the cone below $\lambda$) but $\lambda - \mu = \sum_{\alpha\in\Delta} c_\alpha \alpha$ with $c_\alpha < \lambda(h_\alpha)$ for all $\alpha\in\Delta$, then the projection $M(\lambda)_\mu\twoheadrightarrow L(\lambda)_\mu$ is an isomorphism.

In other words, it is only in the union of the 'shifted' cones rooted at $s_\alpha\cdot\lambda$ that $L(\lambda)$ starts looking different from $M(\lambda)$. This should be somewhat intuitive.

From that we get separation of points as follows:

Corollary: Let $\theta = \sum_{\alpha\in\Delta} c_\alpha \alpha$ with $c_\alpha\in{\mathbb Z}^+$, and suppose $y\in{\mathscr U}{\mathfrak n}^-_{-\theta}$; that is, $x$ is a sum of products $y_{\alpha_{i_1}}\cdots y_{\alpha_{i_k}}$ such that $\theta = \sum_i \alpha_{i_j}$. Then for any $\lambda\in{\mathfrak h}^{\ast}$ with $\lambda(h_\alpha)\in{\mathbb Z}^{> c_\alpha}$ for all $\alpha\in\Delta$, $y.v_\lambda\neq 0$ for the highest weight vector $v_\lambda$ of $L(\lambda)$. In particular, $xy$ doesn't act trivially on $L(\lambda)$.

Proof: If $\tilde{v}_\lambda$ denotes the highest weight vector of $M(\lambda)$, then by the previous proposition we have $y.\tilde{v}_\lambda\in M(\lambda)\setminus N(\lambda)$. In particular, $x$ acts nontrivially on the image $v_\lambda$ of $\tilde{v}_\lambda$ in $L(\lambda)$.

Corollary: Let $\theta$, $y\in{\mathscr U}{\mathfrak n}^-_{-\theta}$ and $\lambda$ be as before. Then there exists some $x\in{\mathscr U}{\mathfrak n}^+_{\theta}$ such that $(xy)_0(\lambda)\neq 0$, where $(xy)_0\in {\mathscr U}{\mathfrak h}\cong {\mathscr P}({\mathfrak h}^{\ast})$ is the projection of $xy\in{\mathscr U}{\mathfrak g}_{0}$ onto ${\mathscr U}{\mathfrak h}\subset {\mathscr U}{\mathfrak g}_{0}$ with respect to the PBW decomposition.

Here, we used that ${\mathscr U}{\mathfrak h}\cong {\mathfrak S}({\mathfrak h})\cong {\mathscr P}({\mathfrak h}^{\ast})$ can be viewed as the algebra of polynomial functions on ${\mathfrak h}^{\ast}$.

Proof: Since $y.v_\lambda\neq 0$ in $L(\lambda)$ and $L(\lambda)$ is simple, we have $L(\lambda)={\mathscr U}{\mathfrak g}.y.v_\lambda={\mathscr U}{\mathfrak n}^-{\mathscr U}{\mathfrak b}.y.v_\lambda$. In particular, there exists $x\in {\mathscr U}{\mathfrak n}^+$ such that $(xy).v_\lambda\neq 0$ in $L(\lambda)_\lambda$. For such $x$, we must have $(xy)_0\neq 0$ since the $({\mathscr U}{\mathfrak g}){\mathfrak n}^+$-component of $xy$ acts trivially on the highest weight vector $v_\lambda$. Finally, note that $z\in{\mathscr U}{\mathfrak h}$ acts on $v_\lambda$ by $z(\lambda)$.

In the previous corollary, the roles of $x$ and $y$ can be reversed:

Corollary: For $\theta$, $\lambda$ as before and $x\in {\mathscr U}{\mathfrak n}^+_{\theta}$, there exists an $y\in {\mathscr U}{\mathfrak n}^-_{-\theta}$ such that $(xy)_0(\lambda)\neq 0$.

Proof: Apply the corollary to $\tau(y)\in {\mathscr U}{\mathfrak n}^-_{-\theta}$, where $\tau:{\mathscr U}{\mathfrak g}^{\text{opp}}\to{\mathscr U}{\mathfrak g}$ is the auto-involution of ${\mathscr U}{\mathfrak g}$ swapping ${\mathfrak n}^+$ and ${\mathfrak n}^-$.

Theorem (Separation of Points): For any $z\in {\mathscr U}{\mathfrak g}\setminus\{0\}$ there exists a finite-dimensional $L(\lambda)$ such that $z.L(\lambda)\neq 0$.

Proof: Assume $z=\sum_\theta y_\theta h_\theta x_\theta$ where $x_\theta\in{\mathscr U}{\mathfrak n}^+_\theta$ and $y_\theta\in{\mathscr U}{\mathfrak n}^-$, $h_\theta\in{\mathscr U}{\mathfrak h}$; in other words, you group PBW terms by the weight on the ${\mathfrak n}$-side. Now, consider $\theta$ maximal w.r.t. the ordering $\lambda\preceq\mu:\Leftrightarrow \mu-\lambda\in{\mathbb Z}^+\Phi^+$ such that $y_\theta h_\theta x_\theta$ nonzero. Then, we know from our previous work that there's some $\lambda\gg 0$ such that for any $\lambda^{\prime}$ such $\lambda\preceq\lambda^{\prime}$ there exists some $y^{\prime}_\theta\in{\mathscr U}{\mathfrak n}^-_{-\theta}$ (depending on $\lambda^{\prime}$) such that $(x_\theta y^{\prime}_\theta)_0(\lambda^{\prime})\neq 0$. Picking $\lambda^{\prime}$ large enough, we may assume that also $h_\theta(\lambda^{\prime})\neq 0$; this is because the polynomial $h_\theta\in {\mathscr P}{\mathfrak h}\cong{\mathscr P}({\mathfrak h}^{\ast})$ cannot vanish on the shifted half-lattice $\lambda + {\mathbb Z}^+\Phi^+$. Putting everything together, in $L(\lambda^{\prime})$ we then have $(y_\theta h_\theta x_\theta).(y^{\prime}_\theta v_{\lambda^{\prime}}) = h_\theta(\lambda^{\prime}) (x_\theta y^{\prime}_\theta)_0(\lambda^{\prime}) y_\theta v_{\lambda^{\prime}}\neq 0$, where for the last step we potentially have to enlarge $\lambda^{\prime}$ again. What about the other summands in $z$? They all annihilate $y^{\prime}_\theta v_{\lambda^{\prime}}$ because of the maximality of $\theta$.

Theorem (Harish-Chandra 1949) for an arbitrary finite-dimensional Lie algebra over a field of characteristic, finite-dimensional representations separate points of the universal enveloping algebra.

This is a deep result, proved in Chap 2 of Dixmier's book "enveloping algebras". It has Ado's theorem as corollary.

In the semisimple case in characteristic zero, finite-dimensional representations split as direct sum of irreducible representations (Weyl), and hence the desired result follows: finite-dimensional irreducible representations separate points.

I don't know if Harish-Chandra's theorem is much easier in the semisimple case (for which Ado's theorem is trivial).

I'm not sure of the picture in finite characteristic, but this is probably tackled by work of Jacobson or so.