[proofplan] We prove both inequalities separately. For $\dim B \leq \dim A$: any chain of primes in $\operatorname{Spec}(B)$ contracts to a chain in $\operatorname{Spec}(A)$ of the same length, with strictness guaranteed by [Incomparability](/theorems/2880). For $\dim A \leq \dim B$: any chain of primes in $\operatorname{Spec}(A)$ lifts to a chain in $\operatorname{Spec}(B)$ of the same length, using [Lying Over](/theorems/2944) for the bottom prime and [Going Up](/theorems/2945) to extend the chain inductively. [/proofplan] [step:Contract a chain of primes in $B$ to a strict chain in $A$ via Incomparability, giving $\dim B \leq \dim A$] Let $\mathfrak{q}_0 \subsetneq \mathfrak{q}_1 \subsetneq \cdots \subsetneq \mathfrak{q}_n$ be a chain of prime ideals in $\operatorname{Spec}(B)$. Define $\mathfrak{p}_i = \mathfrak{q}_i \cap A$ for each $0 \leq i \leq n$. Each $\mathfrak{p}_i$ is a prime ideal of $A$ (as the contraction of a prime ideal under the inclusion $A \hookrightarrow B$). We verify that the contracted chain is strictly ascending. Suppose for contradiction that $\mathfrak{p}_i = \mathfrak{p}_{i+1}$ for some $0 \leq i \leq n - 1$. Then $\mathfrak{q}_i \cap A = \mathfrak{q}_{i+1} \cap A$ and $\mathfrak{q}_i \subsetneq \mathfrak{q}_{i+1}$. Since $A \subset B$ is an integral extension, [Incomparability](/theorems/2880) states that if $\mathfrak{q}, \mathfrak{q}' \in \operatorname{Spec}(B)$ satisfy $\mathfrak{q} \cap A = \mathfrak{q}' \cap A$ and $\mathfrak{q} \subset \mathfrak{q}'$, then $\mathfrak{q} = \mathfrak{q}'$. Applying this to $\mathfrak{q} = \mathfrak{q}_i$ and $\mathfrak{q}' = \mathfrak{q}_{i+1}$ gives $\mathfrak{q}_i = \mathfrak{q}_{i+1}$, contradicting the strict inclusion $\mathfrak{q}_i \subsetneq \mathfrak{q}_{i+1}$. Therefore $\mathfrak{p}_0 \subsetneq \mathfrak{p}_1 \subsetneq \cdots \subsetneq \mathfrak{p}_n$ is a chain of length $n$ in $\operatorname{Spec}(A)$. Since every chain in $\operatorname{Spec}(B)$ yields a chain of equal length in $\operatorname{Spec}(A)$, taking the supremum over all chains gives $\dim B \leq \dim A$. [guided] We want to show that a chain of length $n$ in $\operatorname{Spec}(B)$ cannot "collapse" when contracted to $A$. Let $\mathfrak{q}_0 \subsetneq \mathfrak{q}_1 \subsetneq \cdots \subsetneq \mathfrak{q}_n$ be such a chain, and set $\mathfrak{p}_i = \mathfrak{q}_i \cap A$. Each $\mathfrak{p}_i$ is prime because the contraction of a prime ideal under a ring homomorphism is always prime: if $ab \in \mathfrak{p}_i = \mathfrak{q}_i \cap A$, then $ab \in \mathfrak{q}_i$, so $a \in \mathfrak{q}_i$ or $b \in \mathfrak{q}_i$ (since $\mathfrak{q}_i$ is prime), giving $a \in \mathfrak{p}_i$ or $b \in \mathfrak{p}_i$. The key question is: can the contracted chain have a repeated prime, i.e., can $\mathfrak{p}_i = \mathfrak{p}_{i+1}$ for some $i$? If this occurred, we would have two distinct primes $\mathfrak{q}_i \subsetneq \mathfrak{q}_{i+1}$ of $B$ lying over the same prime of $A$. But [Incomparability](/theorems/2880) forbids exactly this: in an integral extension $A \subset B$, there cannot exist primes $\mathfrak{q} \subsetneq \mathfrak{q}'$ in $B$ with $\mathfrak{q} \cap A = \mathfrak{q}' \cap A$. (The hypotheses of Incomparability require $A \subset B$ integral, which holds by assumption.) So the contracted chain $\mathfrak{p}_0 \subsetneq \mathfrak{p}_1 \subsetneq \cdots \subsetneq \mathfrak{p}_n$ is strictly ascending, hence has length $n$. Since every chain of length $n$ in $\operatorname{Spec}(B)$ produces a chain of length $n$ in $\operatorname{Spec}(A)$, we conclude $\dim B \leq \dim A$. [/guided] [/step] [step:Lift a chain of primes in $A$ to a chain in $B$ via Lying Over and Going Up, giving $\dim A \leq \dim B$] Let $\mathfrak{p}_0 \subsetneq \mathfrak{p}_1 \subsetneq \cdots \subsetneq \mathfrak{p}_n$ be a chain of prime ideals in $\operatorname{Spec}(A)$. We construct a chain $\mathfrak{q}_0 \subsetneq \mathfrak{q}_1 \subsetneq \cdots \subsetneq \mathfrak{q}_n$ in $\operatorname{Spec}(B)$ with $\mathfrak{q}_i \cap A = \mathfrak{p}_i$ for each $i$, by induction on $i$. **Base case ($i = 0$).** Since $A \subset B$ is an integral extension and $\mathfrak{p}_0 \in \operatorname{Spec}(A)$, [Lying Over](/theorems/2944) provides $\mathfrak{q}_0 \in \operatorname{Spec}(B)$ with $\mathfrak{q}_0 \cap A = \mathfrak{p}_0$. **Inductive step.** Suppose we have constructed $\mathfrak{q}_0 \subsetneq \cdots \subsetneq \mathfrak{q}_k$ with $\mathfrak{q}_j \cap A = \mathfrak{p}_j$ for $0 \leq j \leq k$, where $k < n$. We have the inclusions $\mathfrak{p}_k \subsetneq \mathfrak{p}_{k+1}$ in $A$ and $\mathfrak{q}_k \in \operatorname{Spec}(B)$ with $\mathfrak{q}_k \cap A = \mathfrak{p}_k$. Since $A \subset B$ is integral, [Going Up](/theorems/2945) (applied with the pair $\mathfrak{p}_k \subset \mathfrak{p}_{k+1}$ and the prime $\mathfrak{q}_k$ lying over $\mathfrak{p}_k$) provides $\mathfrak{q}_{k+1} \in \operatorname{Spec}(B)$ with $\mathfrak{q}_k \subset \mathfrak{q}_{k+1}$ and $\mathfrak{q}_{k+1} \cap A = \mathfrak{p}_{k+1}$. The inclusion $\mathfrak{q}_k \subset \mathfrak{q}_{k+1}$ is strict: if $\mathfrak{q}_k = \mathfrak{q}_{k+1}$, then $\mathfrak{p}_k = \mathfrak{q}_k \cap A = \mathfrak{q}_{k+1} \cap A = \mathfrak{p}_{k+1}$, contradicting $\mathfrak{p}_k \subsetneq \mathfrak{p}_{k+1}$. By induction, we obtain a chain $\mathfrak{q}_0 \subsetneq \mathfrak{q}_1 \subsetneq \cdots \subsetneq \mathfrak{q}_n$ of length $n$ in $\operatorname{Spec}(B)$. Since every chain of length $n$ in $\operatorname{Spec}(A)$ lifts to a chain of length $n$ in $\operatorname{Spec}(B)$, taking the supremum gives $\dim A \leq \dim B$. [guided] The challenge here is the reverse inequality: given a chain in $A$, we need to "lift" it to $B$. This requires two separate tools from the theory of integral extensions. First, we need a prime of $B$ lying over the bottom prime $\mathfrak{p}_0$. [Lying Over](/theorems/2944) guarantees this: for any integral extension $A \subset B$ and any $\mathfrak{p} \in \operatorname{Spec}(A)$, there exists $\mathfrak{q} \in \operatorname{Spec}(B)$ with $\mathfrak{q} \cap A = \mathfrak{p}$. The only hypothesis is integrality of the extension, which we have. Next, we need to extend the chain upward one step at a time. Suppose we already have $\mathfrak{q}_k$ with $\mathfrak{q}_k \cap A = \mathfrak{p}_k$, and we want $\mathfrak{q}_{k+1} \supset \mathfrak{q}_k$ with $\mathfrak{q}_{k+1} \cap A = \mathfrak{p}_{k+1}$. This is exactly the statement of [Going Up](/theorems/2945): given an integral extension $A \subset B$, primes $\mathfrak{p}_k \subset \mathfrak{p}_{k+1}$ in $A$, and $\mathfrak{q}_k \in \operatorname{Spec}(B)$ lying over $\mathfrak{p}_k$, there exists $\mathfrak{q}_{k+1} \in \operatorname{Spec}(B)$ containing $\mathfrak{q}_k$ and lying over $\mathfrak{p}_{k+1}$. Why is the resulting inclusion $\mathfrak{q}_k \subset \mathfrak{q}_{k+1}$ strict? If $\mathfrak{q}_k = \mathfrak{q}_{k+1}$, then contracting to $A$ gives $\mathfrak{p}_k = \mathfrak{p}_{k+1}$, contradicting the hypothesis that the original chain is strictly ascending. Applying this inductive construction from $i = 0$ to $i = n$ produces the desired chain of length $n$ in $\operatorname{Spec}(B)$, giving $\dim A \leq \dim B$. [/guided] [/step] [step:Combine both inequalities to conclude $\dim A = \dim B$] From the first step, $\dim B \leq \dim A$. From the second step, $\dim A \leq \dim B$. Together, $\dim A = \dim B$. [/step]