I've been searching around, and I'm only finding pseudo-derivations of this. After a lot of searching combined with reasoning, I've come up with the following;
Is the reasoning correct?
The power function of a test is the probability that $H_0$ is rejected given a true value for the parameter (or under an alternative hypothesis $H_A:\mu=\mu_A$. Assume that we have the statistic $Z=\frac{\bar X-\mu}{{\sigma/\sqrt n}}\sim\mathrm{N}(0,1)$ and the hypothesis:
$$\def\P#1{\text{P}\left(#1\right)}H_0:\mu=\mu_0~~\text{vs}~~\mu>\mu_0$$
If we now assume that the true value of $\mu=\mu_1$ then let $\bar X_1$ be the true distribution of $\bar X$: $$\bar X_1\overset{\tiny\text{true}}{\sim} \text{N}(\mu_1,\sigma/{\sqrt n})$$ And let $\bar X_0$ be the distribution of $\bar X_0$ assuming $H_0$ is true $$\bar X_0\overset{\tiny\text{H}_0}{\sim} \text{N}(\mu_0,\sigma/{\sqrt n})$$
We will reject $H_0$ if $\P{\bar X_0 > \bar x_{0,\alpha}}$ (using upper tails), where $ \bar x_{0,\alpha} $ is the $\alpha$-quantile of $\bar X_0$. We want to obtain the probability that the null hypothesis is rejected if we know the true value of $\mu$. That is what is the probability that a sample from $\bar X_1$ takes a value within the rejection region for $\bar X_0$, or:
$$\P{\bar X_1 > \bar x_{0,\alpha}}$$.
Also we can easily show that the $\bar x_{0,\alpha}$ quantile relates to the $z_\alpha$ quantile like this $$\bar x_{0,\alpha} = \frac{z_{\alpha}\sigma}{\sqrt{n}}+\mu_0\\$$ And we obtain $\def\sonsqn{\sigma/{\sqrt n}}$ \begin{align*} \P{\bar X_1 > \bar x_{0,\alpha}} &= \P{\frac{\bar X_1-\mu_1}{\sonsqn}>\frac{\bar x_{0,\alpha}-\mu_1}{\sonsqn}}\\ \rlap{\text{Inserting for $\bar x_{0,\alpha}$ in the relation above}}\\ &=\P{Z>z_\alpha + \frac{\mu_0-\mu_1}{\sonsqn}}=1-\Phi\left(z_\alpha + \frac{\mu_0-\mu_1}{\sonsqn}\right) \end{align*}
