Question about a Theorem on integral Galois extensions from Lang

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]