[proofplan]
Every face of the join is uniquely decomposed into its $K$-part and its $L$-part because the vertex sets are disjoint. The dimension formula follows by translating dimension into maximal face cardinality and using additivity of cardinality under disjoint union. For the link identity, we test an arbitrary face of $K * L$ against the defining link condition and observe that the condition separates exactly into the corresponding link conditions in $K$ and in $L$.
[/proofplan]
[step:Decompose faces of the join into their two factor components]
Let $V_K$ and $V_L$ denote the vertex sets of $K$ and $L$, respectively. Since $V_K \cap V_L = \varnothing$, every face $\rho \in K * L$ has a unique decomposition
\begin{align*}
\rho = \alpha \cup \beta
\end{align*}
with $\alpha \in K$ and $\beta \in L$, namely
\begin{align*}
\alpha := \rho \cap V_K
\end{align*}
and
\begin{align*}
\beta := \rho \cap V_L.
\end{align*}
For such a decomposition, $\alpha \cap \beta = \varnothing$, so
\begin{align*}
|\rho| = |\alpha \cup \beta| = |\alpha| + |\beta|.
\end{align*}
[/step]
[step:Compute the dimension by maximizing face cardinalities]
Define
\begin{align*}
m_K := \max_{\alpha \in K} |\alpha|
\end{align*}
and
\begin{align*}
m_L := \max_{\beta \in L} |\beta|.
\end{align*}
These maxima exist because $K$ and $L$ are finite and nonempty. By definition of dimension for a finite simplicial complex,
\begin{align*}
\dim K = m_K - 1
\end{align*}
and
\begin{align*}
\dim L = m_L - 1.
\end{align*}
For every face $\rho \in K * L$, write $\rho = \alpha \cup \beta$ with $\alpha \in K$ and $\beta \in L$. By the preceding step,
\begin{align*}
|\rho| = |\alpha| + |\beta| \leq m_K + m_L.
\end{align*}
Conversely, choose faces $\alpha_0 \in K$ and $\beta_0 \in L$ satisfying $|\alpha_0| = m_K$ and $|\beta_0| = m_L$. Then $\alpha_0 \cup \beta_0 \in K * L$, and
\begin{align*}
|\alpha_0 \cup \beta_0| = m_K + m_L.
\end{align*}
Thus the maximum cardinality of a face of $K * L$ is $m_K + m_L$, and therefore
\begin{align*}
\dim(K * L) = (m_K + m_L) - 1 = (m_K - 1) + (m_L - 1) + 1 = \dim K + \dim L + 1.
\end{align*}
[guided]
The dimension of a finite simplicial complex is controlled by the largest possible number of vertices in a face. We therefore define
\begin{align*}
m_K := \max_{\alpha \in K} |\alpha|
\end{align*}
and
\begin{align*}
m_L := \max_{\beta \in L} |\beta|.
\end{align*}
The finiteness and nonemptiness hypotheses are used here: they guarantee that these maxima exist. By the definition of dimension,
\begin{align*}
\dim K = m_K - 1
\end{align*}
and
\begin{align*}
\dim L = m_L - 1.
\end{align*}
Now take any face $\rho \in K * L$. By definition of the join, there are faces $\alpha \in K$ and $\beta \in L$ such that $\rho = \alpha \cup \beta$. Because the vertex sets of $K$ and $L$ are disjoint, the two parts do not share vertices, so cardinality is additive:
\begin{align*}
|\rho| = |\alpha \cup \beta| = |\alpha| + |\beta|.
\end{align*}
Since $|\alpha| \leq m_K$ and $|\beta| \leq m_L$, every face of $K * L$ satisfies
\begin{align*}
|\rho| \leq m_K + m_L.
\end{align*}
To see that this upper bound is attained, choose faces $\alpha_0 \in K$ and $\beta_0 \in L$ with $|\alpha_0| = m_K$ and $|\beta_0| = m_L$. Their union is a face of the join:
\begin{align*}
\alpha_0 \cup \beta_0 \in K * L.
\end{align*}
Again using disjointness of the vertex sets,
\begin{align*}
|\alpha_0 \cup \beta_0| = |\alpha_0| + |\beta_0| = m_K + m_L.
\end{align*}
Thus the largest face of $K * L$ has cardinality $m_K + m_L$. Therefore
\begin{align*}
\dim(K * L) = (m_K + m_L) - 1.
\end{align*}
Substituting $m_K - 1 = \dim K$ and $m_L - 1 = \dim L$ gives
\begin{align*}
\dim(K * L) = \dim K + \dim L + 1.
\end{align*}
[/guided]
[/step]
[step:Translate the link condition in the join into link conditions in the factors]
Fix faces $\sigma \in K$ and $\tau \in L$. Since $\sigma \cup \tau \in K * L$, the link $\operatorname{lk}_{K * L}(\sigma \cup \tau)$ is defined by
\begin{align*}
\operatorname{lk}_{K * L}(\sigma \cup \tau)
=
\{\rho \in K * L : \rho \cap (\sigma \cup \tau) = \varnothing \text{ and } \rho \cup \sigma \cup \tau \in K * L\}.
\end{align*}
Let $\rho \in K * L$, and write its unique decomposition as
\begin{align*}
\rho = \gamma \cup \delta
\end{align*}
with $\gamma \in K$ and $\delta \in L$. Because all vertices of $\gamma$ and $\sigma$ lie in $V_K$, all vertices of $\delta$ and $\tau$ lie in $V_L$, and $V_K \cap V_L = \varnothing$, we have
\begin{align*}
\rho \cap (\sigma \cup \tau) = \varnothing
\end{align*}
if and only if
\begin{align*}
\gamma \cap \sigma = \varnothing
\end{align*}
and
\begin{align*}
\delta \cap \tau = \varnothing.
\end{align*}
Also,
\begin{align*}
\rho \cup \sigma \cup \tau = (\gamma \cup \sigma) \cup (\delta \cup \tau).
\end{align*}
By the definition of the join, this union belongs to $K * L$ if and only if
\begin{align*}
\gamma \cup \sigma \in K
\end{align*}
and
\begin{align*}
\delta \cup \tau \in L.
\end{align*}
Therefore $\rho \in \operatorname{lk}_{K * L}(\sigma \cup \tau)$ if and only if $\gamma \in \operatorname{lk}_K(\sigma)$ and $\delta \in \operatorname{lk}_L(\tau)$. Equivalently,
\begin{align*}
\rho = \gamma \cup \delta \in \operatorname{lk}_K(\sigma) * \operatorname{lk}_L(\tau).
\end{align*}
Since this equivalence holds for every face $\rho \in K * L$, we conclude
\begin{align*}
\operatorname{lk}_{K * L}(\sigma \cup \tau)=\operatorname{lk}_K(\sigma)*\operatorname{lk}_L(\tau).
\end{align*}
[/step]
