[proofplan] The claim has two parts: set-theoretic equality $|K'| = |K|$ of underlying spaces, and verification that $K'$ is a simplicial complex. For the equality of polyhedra we show both inclusions. The inclusion $|K'| \subseteq |K|$ is almost immediate: every simplex of $K'$ has vertices that are barycenters of simplices of $K$, and each barycenter lies in its parent simplex, so the convex hull of a chain of barycenters sits inside the largest simplex in the chain. The reverse inclusion is the substance: we induct on dimension to show every point of a simplex $\sigma \in K$ decomposes via the barycenter $\hat{\sigma}$ into a convex combination of points of proper faces, hence eventually into a convex combination of barycenters of a chain. Simpliciality of $K'$ requires checking that the faces of any chain-simplex are chain-simplices and that two chain-simplices intersect in a common face; both follow from the chain structure. [/proofplan]

[step:Establish the inclusion $|K'| \subseteq |K|$ via convexity of simplices] Let $\langle \hat{\sigma}_0, \ldots, \hat{\sigma}_k \rangle \in K'$, corresponding to a strict chain of faces $\sigma_0 \subsetneq \sigma_1 \subsetneq \cdots \subsetneq \sigma_k$ in $K$. A general point has the form \begin{align*} p = \sum_{j=0}^k t_j\, \hat{\sigma}_j, \qquad t_j \geq 0, \qquad \sum_{j=0}^k t_j = 1. \end{align*} By the definition of the barycenter, each $\hat{\sigma}_j$ lies in $\mathring{\sigma_j} \subseteq \sigma_j$; since $\sigma_j \subseteq \sigma_k$ (as $\sigma_j$ is a face of $\sigma_k$), every $\hat{\sigma}_j$ lies in $\sigma_k$. The simplex $\sigma_k$, being the convex hull of its vertices in Euclidean space, is convex, so the convex combination $p$ lies in $\sigma_k \subseteq |K|$. This shows $|K'| \subseteq |K|$. [/step]

[step:Prove the reverse inclusion $|K| \subseteq |K'|$ by induction on simplex dimension]We show: for every simplex $\sigma \in K$, $\sigma \subseteq |K'|$. We argue by induction on $n = \dim \sigma$. **Base case** ($n = 0$): Let $\sigma = \langle a \rangle \in K$ be a $0$-simplex. Then $\hat{\sigma} = a$, and the chain of length $1$ consisting of $\sigma$ alone produces the $0$-simplex $\langle \hat{\sigma} \rangle = \langle a \rangle \in K'$. Hence $a \in |K'|$, so $\sigma = \{a\} \subseteq |K'|$. **Inductive step**: Fix $n \geq 1$ and assume the inclusion $\tau \subseteq |K'|$ holds for every simplex $\tau \in K$ with $\dim \tau < n$. Let $\sigma \in K$ with $\dim \sigma = n$ and let $x \in \sigma$. If $x = \hat{\sigma}$, then $x$ is the sole vertex of $\langle \hat{\sigma} \rangle \in K'$, so $x \in |K'|$. Otherwise $x \neq \hat{\sigma}$. The ray from $\hat{\sigma}$ through $x$ exits $\sigma$ at a unique point $y$ of the boundary $\partial \sigma = \sigma \setminus \mathring{\sigma}$ on the far side. Concretely, since $\hat{\sigma} \in \mathring{\sigma}$ (all barycentric coordinates strictly positive), the affine parameter $\lambda \geq 0$ for which \begin{align*} \hat{\sigma} + \lambda (x - \hat{\sigma}) \in \partial \sigma \end{align*} achieves its minimum at some $\lambda_0 \geq 1$. Setting $y = \hat{\sigma} + \lambda_0 (x - \hat{\sigma})$ gives $y \in \partial \sigma$ and \begin{align*} x = \left(1 - \frac{1}{\lambda_0}\right) \hat{\sigma} + \frac{1}{\lambda_0}\, y, \qquad 0 < \frac{1}{\lambda_0} \leq 1, \end{align*} so $x$ is a convex combination of $\hat{\sigma}$ and $y$. The boundary $\partial \sigma$ is the union of the proper faces $\tau \subsetneq \sigma$, each of dimension at most $n - 1$. Hence $y \in \tau$ for some proper face $\tau \in K$ with $\dim \tau < n$. By the inductive hypothesis, $y \in |K'|$, so $y$ lies in some simplex $\langle \hat{\tau}_0, \ldots, \hat{\tau}_{k-1} \rangle \in K'$ corresponding to a chain $\tau_0 \subsetneq \cdots \subsetneq \tau_{k-1}$ of faces with $\tau_{k-1} \subseteq \tau \subsetneq \sigma$. Appending $\sigma$ to this chain yields a strict chain $\tau_0 \subsetneq \cdots \subsetneq \tau_{k-1} \subsetneq \sigma$, producing the simplex $\langle \hat{\tau}_0, \ldots, \hat{\tau}_{k-1}, \hat{\sigma} \rangle \in K'$. The convex hull of its vertices contains $y$ (as a convex combination of $\hat{\tau}_0, \ldots, \hat{\tau}_{k-1}$) and $\hat{\sigma}$, hence contains every convex combination of $y$ and $\hat{\sigma}$, in particular $x$. Therefore $x \in |K'|$. Since $x \in \sigma$ was arbitrary, $\sigma \subseteq |K'|$. This completes the induction. Taking the union over all $\sigma \in K$ gives $|K| = \bigcup_{\sigma \in K} \sigma \subseteq |K'|$. Combined with Step 1, $|K'| = |K|$.[/step]

[guided]We must show $|K| \subseteq |K'|$. The natural approach is to prove simplex by simplex: for every $\sigma \in K$, show $\sigma \subseteq |K'|$. The obstruction is that a simplex $\sigma$ of $K$ is typically *not* a simplex of $K'$; its interior is instead cut into smaller pieces by the barycenters of $\sigma$ and its faces. So we cannot use $\sigma$ directly; we must build up $\sigma$ from smaller $K'$-simplices. The geometric intuition: the barycenter $\hat{\sigma}$ lies in the interior of $\sigma$, and one can express any point $x \in \sigma$ as a convex combination of $\hat{\sigma}$ and some point $y$ on the boundary $\partial \sigma$. The boundary is a union of proper faces, which have strictly smaller dimension, so by induction $y \in |K'|$. Then the $K'$-simplex containing $y$, together with $\hat{\sigma}$, gives a larger $K'$-simplex containing $x$. **Base case**: For $\sigma = \langle a \rangle$, the barycenter is the vertex $a$ itself, and $\langle a \rangle \in K'$ directly. **Inductive step**: Fix $n \geq 1$ and suppose the claim holds for every simplex of dimension $< n$. Let $\sigma \in K$ be an $n$-simplex and $x \in \sigma$. The barycenter $\hat{\sigma} \in \mathring{\sigma}$ sits in the interior: expanding in barycentric coordinates, $\hat{\sigma} = \frac{1}{n+1}(a_0 + \cdots + a_n)$, so all coordinates equal $\frac{1}{n+1} > 0$. **Case 1**: $x = \hat{\sigma}$. Then $\langle \hat{\sigma} \rangle \in K'$ (the length-one chain $\sigma$ gives this $0$-simplex), and $x \in |K'|$. **Case 2**: $x \neq \hat{\sigma}$. Consider the ray from $\hat{\sigma}$ through $x$: parametrised by $\lambda \geq 0$, the point $\hat{\sigma} + \lambda (x - \hat{\sigma})$ equals $\hat{\sigma}$ at $\lambda = 0$ and $x$ at $\lambda = 1$. Since $\hat{\sigma} \in \mathring{\sigma}$, for small $\lambda > 0$ we are still in $\mathring{\sigma}$; as $\lambda$ increases, eventually the ray exits $\sigma$. Let $\lambda_0$ be the smallest $\lambda \geq 1$ with the point on $\partial \sigma$ (this exists because $\sigma$ is compact and the ray must exit). Set \begin{align*} y = \hat{\sigma} + \lambda_0 (x - \hat{\sigma}) \in \partial \sigma. \end{align*} Then $x$ sits on the segment $[\hat{\sigma}, y]$: solving for $x$ gives \begin{align*} x = \left(1 - \tfrac{1}{\lambda_0}\right) \hat{\sigma} + \tfrac{1}{\lambda_0}\, y, \end{align*} a convex combination (the coefficients are non-negative and sum to $1$, using $\lambda_0 \geq 1$). Now $\partial \sigma = \sigma \setminus \mathring{\sigma}$ is covered by the proper faces of $\sigma$, each of dimension $\leq n - 1 < n$. Pick a proper face $\tau$ of $\sigma$ with $y \in \tau$. Then $\tau \in K$ (faces of simplices are simplices by the complex axiom), and by the inductive hypothesis $\tau \subseteq |K'|$; so $y$ lies in some $K'$-simplex $\langle \hat{\tau}_0, \ldots, \hat{\tau}_{k-1} \rangle$ indexed by a chain $\tau_0 \subsetneq \cdots \subsetneq \tau_{k-1} \subseteq \tau$. Since $\tau_{k-1} \subseteq \tau \subsetneq \sigma$, appending $\sigma$ extends the chain strictly: \begin{align*} \tau_0 \subsetneq \cdots \subsetneq \tau_{k-1} \subsetneq \sigma. \end{align*} The corresponding $K'$-simplex $\langle \hat{\tau}_0, \ldots, \hat{\tau}_{k-1}, \hat{\sigma} \rangle$ has a convex hull that contains both $y$ and $\hat{\sigma}$, and therefore the entire segment between them, which contains $x$. Thus $x \in |K'|$ in either case. The induction closes, yielding $\sigma \subseteq |K'|$ for every $\sigma \in K$, hence $|K| \subseteq |K'|$.[/guided]

[step:Verify the face-closure axiom of a simplicial complex for $K'$] For $K'$ to be a simplicial complex, every face of every simplex of $K'$ must itself be in $K'$. Let $\langle \hat{\sigma}_0, \ldots, \hat{\sigma}_k \rangle \in K'$, corresponding to the chain $\sigma_0 \subsetneq \cdots \subsetneq \sigma_k$. A face of this simplex is determined by a subset $\{j_0 < j_1 < \cdots < j_m\} \subseteq \{0, 1, \ldots, k\}$, yielding the simplex $\langle \hat{\sigma}_{j_0}, \ldots, \hat{\sigma}_{j_m} \rangle$. The corresponding sequence $\sigma_{j_0} \subsetneq \sigma_{j_1} \subsetneq \cdots \subsetneq \sigma_{j_m}$ is a strict chain of faces (subchains of strict chains are strict), so $\langle \hat{\sigma}_{j_0}, \ldots, \hat{\sigma}_{j_m} \rangle \in K'$ by the defining formula for $K'$. [/step]

[step:Verify the intersection axiom by analysing common chain refinements] For $K'$ to be a simplicial complex, the intersection of any two simplices of $K'$ must be a face of each, i.e., empty or a common face. Let $\alpha = \langle \hat{\sigma}_0, \ldots, \hat{\sigma}_k \rangle, \beta = \langle \hat{\tau}_0, \ldots, \hat{\tau}_\ell \rangle \in K'$ correspond to chains $\sigma_0 \subsetneq \cdots \subsetneq \sigma_k$ and $\tau_0 \subsetneq \cdots \subsetneq \tau_\ell$ in $K$. Let $p \in \alpha \cap \beta$. We show $p$ lies in a common face of $\alpha$ and $\beta$. Any point of $|K|$ sits in the interior of a unique simplex $\rho \in K'$ by the [Unique Interior Simplex](/theorems/1914) theorem applied to the complex $K'$ (which was set-theoretically realised in Step 2; the face-closure axiom in Step 3 permits treating the set $K'$ as a simplicial complex for the purposes of the interior-simplex lemma once intersections are handled — but we cannot assume this yet). We therefore argue directly. Consider the set $\mathcal{C} = \{\sigma_0, \ldots, \sigma_k\} \cap \{\tau_0, \ldots, \tau_\ell\}$ of shared simplices. The claim is that $p$ is a convex combination of the barycenters $\{\hat{\rho} : \rho \in \mathcal{C}\}$, and moreover $\mathcal{C}$ is a chain (being the intersection of two chains with respect to the face-inclusion order, and the face-inclusion order on a finite set of simplices of $K$ is a total order on any chain, so the intersection of two chains is again a chain). To prove this claim, observe: each barycenter $\hat{\sigma}_j$ lies in $\mathring{\sigma}_j$, and by the [Unique Interior Simplex](/theorems/1914) theorem in $K$, distinct open simplices $\mathring{\sigma}$ are disjoint. Express $p \in \alpha$ as $p = \sum_j s_j \hat{\sigma}_j$ with $s_j \geq 0$, $\sum s_j = 1$, and similarly $p \in \beta$ as $p = \sum_i t_i \hat{\tau}_i$. Decompose both sums according to the simplex of $K$ in whose interior each barycenter sits: $\hat{\sigma}_j \in \mathring{\sigma}_j$ and $\hat{\tau}_i \in \mathring{\tau}_i$. A point of $|K|$ has a unique expression as a combination of barycenters up to grouping into a *single* open simplex; but the barycenters in a chain lie in pairwise distinct open simplices. Hence the sum $\sum s_j \hat{\sigma}_j$ has a unique representation as a convex combination landing in a single simplex of $K$ — namely $\sigma_k$. Both expressions for $p$ must correspond point-wise: for each simplex $\rho \in K$, the contribution of $\rho$'s barycenter from the first sum must equal its contribution from the second. If $\rho$ does not appear in the $\tau$-chain, its coefficient in $\beta$'s expression is $0$, forcing $s_j = 0$ for the index $j$ with $\sigma_j = \rho$, if any. Symmetrically for $\beta$. Therefore the nonzero barycenters in both expressions come from shared simplices in $\mathcal{C}$. The simplex $\langle \hat{\rho} : \rho \in \mathcal{C}\rangle$, indexed by the chain $\mathcal{C}$, is a common face of $\alpha$ and $\beta$ (it is a subchain of each), and $p$ lies in it. Hence $\alpha \cap \beta$ is contained in the common face $\langle \hat{\rho} : \rho \in \mathcal{C} \rangle$ of $\alpha$ and $\beta$; the reverse inclusion is immediate since every common face is in both simplices. Thus $\alpha \cap \beta$ is a common face of $\alpha$ and $\beta$, confirming the intersection axiom. Combining Steps 1-4, $|K'| = |K|$ and $K'$ satisfies both axioms of a simplicial complex. [/step]