Existence of valuation rings in a finite extension of the field of fractions of a weakly Artinian domain without Axiom of Choice

Can we prove the following theorem without Axiom of Choice? This is a generalization of this problem.

Theorem Let $A$ be a weakly Artinian domain. Let $K$ be the field of fractions of $A$. Let $L$ be a finite extension field of $K$. Let $B$ be a subring of $L$ containing $A$. Let $P$ be a prime ideal of $B$. Then there exists a valuation ring of $L$ dominating $B_P$.

As for why I think this question is interesting, please see(particularly Pete Clark's answer): Why worry about the axiom of choice?

-

Lemma 1 Let $A$ be an integrally closed weakly Artinian domain. Let $S$ be a multiplicative subset of $A$. Let $A_S$ be the localization with respect to $S$. Then $A_S$ is an integrally closed weakly Artinian domain.

Proof: Let $K$ be the field of fractions of $A$. Suppose that $x \in K$ is integral over $A_S$. $x^n + a_{n-1}x^{n-1} + ... + a_1x + a_0 = 0$, where $a_i \in A_S$. Hence there exists $s \in S$ such that $sx$ is integral over $A$. Since $A$ is integrally closed, $sx \in A$. Hence $x \in A_S$. Hence $A_S$ is integrally closed.

Let $f$ be a non-zero element of $A_S$. $f = a/s$, where $a \in A, s \in S$. Then $fA_S = aA_S$. By this, $aA$ is a product of prime ideals of $A$. Let $P$ be a non-zero prime ideal $P$ of $A$. Since $P$ is maximal, $A_S/P^nA_S$ is isomorphic to $A/P^n$ or $0$. Hence $leng_{A_S} A_S/aA_S$ is finite. QED

Lemma 2 Let $A$ be an integrally closed weakly Artinian domain. Let $P$ be a non-zero prime ideal of $A$. Then $A_P$ is a discrete valuation ring.

Proof: By Lemma 1 and this, every non-zero ideal of $A_P$ has a unique factorization as a product of prime ideals. Hence $PA_P \neq P^2A_p$. Let $x \in PA_P - P^2A_P$. Since $PA_P$ is the only non-zero prime ideal of $A_P$, $xA = PA_P$. Since every non-zero ideal of $A_P$ can be written $P^nA_P$, $A_P$ is a principal ideal domain. Hence $A_P$ is a discrete valuation ring. QED

Proof of the title theorem We can assume that $P \neq 0$. Let $C$ be the integral closure of $B$ in $L$. By this, $C$ is a weakly Artinian $A$-algebra in the sense of Definition 2 of my answer to this. By Lemma 2 of my answer to this, $C$ is a weakly Artinian ring. Let $S = B - P$. Let $C_P$ and $B_P$ be the localizations of $C$ and $B$ with respect to $S$ respectively. By this, $leng_A C/PC$ is finite. Hence by Lemma 7 of my answer to this, $C/PC$ is finitely generated as an $A$-module.Hence $C/PC$ is finitely generated as a $B$-module. Hence $C_P/PC_P$ is finitely generated as a $B_P$-module. Since $PC_P \neq C_P$, by the lemma of the answer by QiL to this, there exists a maximal ideal of $C_P/PC_P$ whose preimage is $PB_P$. Hence there exists a maximal ideal $Q$ of $C_P$ such tha $PB_P = Q \cap B_P$. Let $Q' = Q \cap C$. Then $Q'$ is a prime ideal of $C$ lying over $P$. By Lemma 2, $C_Q'$ is a discrete valuation ring and it dominates $B_P$. QED

-