I am trying to understand Theorem 2.9 from Ch. VII of Serge Lang's Algebra. The statement is the following:
Let $A$ be an integral domain which is integrally closed in its field of fractions $K$. Let $f(x)\in A[x]$ be monic and irreducible. Let $\mathfrak{p}$ be a maximal ideal of $A$ and let $\overline{f}(x)\in (A/\mathfrak{p})[x]$ be the reduction of $f$ modulo $\mathfrak{p}$. Assume that $\overline{f}(x)$ has no multiple roots in an algebraic closure of $A/\mathfrak{p}$. Let $L$ be a splitting field of $f$ over $K$ and let $B$ be the integral closure of $A$ in $L$. Let $\mathfrak{P}\subset B$ be a prime ideal lying above $\mathfrak{p}$.
Let $G_\mathfrak{P}$ be the subgroup of the Galois group of $L$ over $K$ of all $\sigma$ with $\sigma(\mathfrak{P})=\mathfrak{P}$. For each such $\sigma$ we get $\overline{\sigma}\in \mathrm{Aut}_{A/\mathfrak{p}}(B/\mathfrak{P})$ by letting $\overline{\sigma}(\overline{x})=\overline{\sigma(x)}$, where $\overline{x}=x+\mathfrak{P}\in B/\mathfrak{P}$.
The conclusion of the theorem is that the map $\sigma\mapsto \overline{\sigma}$ is an isomorphism of $G_\mathfrak{P}$ with $\mathrm{Aut}_{A/\mathfrak{p}}(B/\mathfrak{P})$, where the latter is Galois group of $\overline{f}$ (according to the theorem).
The statement in italics is my main confusion. How do we know that $\mathrm{Aut}_{A/\mathfrak{p}}(B/\mathfrak{P})$ is the Galois group of $\overline{f}$ i.e. that $B/\mathfrak{P}$ is the splitting field of $\overline{f}$?
What I'm interested in is to apply the theorem with $A=\mathbb{Z}$ and $\mathfrak{p}=(p)$ for some prime $p$ to conclude that the Galois group of $f$ contains a subgroup isomorphic to the Galois group of $\overline{f}$.
I think the following argument works, though it is probably not the most direct. It relies on what the theorem proves. Note that all the roots of $\overline{f}$ over $A/\mathfrak{p}$ are in $B/\mathfrak{P}$, since all the roots of $f$ are in $B$. Thus the field $B/\mathfrak{P}$ contains the Galois closure of $\overline{f}$ over $A/\mathfrak{p}$. If it properly contains it, in particular there is an automorphism of $B/\mathfrak{P}$ over $A/\mathfrak{p}$ that fixes all the roots of $\overline{f}$. Note however that all the automorphisms of $B/\mathfrak{P}$ over $A/\mathfrak{p}$ comes from elements in $G_{\mathfrak{P}}$. Any non-trivial automorphism of this sort must send some root $\alpha$ of $f$ to some distinct root $\beta$ of $f$. Thus mod $\mathfrak{P}$, $\overline{\alpha}$ is sent to $\overline{\beta}$. Both are roots of $\overline{f}$ so by the assumption that the automorphism fixes those roots, $\overline{\alpha}=\overline{\beta}$. This is a contradiction. [If I understand correctly the proof in Lang's book, it does not rely on the fact that the latter field is the Galois group of $\overline{f}$, so this should be ok]