[proofplan] We prove that the map on homology induced by a simplicial approximation $a: K' \to K$ to the identity is an isomorphism. The argument is by induction on the number of simplices of $K$, with Mayer-Vietoris as the inductive engine. The base case handles the single-simplex complex $\overline{\sigma}$: its barycentric subdivision is the cone on $\partial \sigma$ with apex $\hat{\sigma}$, both $\overline{\sigma}$ and its subdivision are contractible, and one checks on generators that $a_*$ is the identity isomorphism between their $H_0 = \mathbb{Z}$'s. For the inductive step we pick a maximal simplex $\sigma$, decompose $K = L \cup S$ with $S = \overline{\sigma}$ and $L = K \setminus \{\sigma\}$, so that $L \cap S = \partial \sigma$, and subdivide compatibly to obtain $K' = L' \cup S'$. Mayer-Vietoris gives a commutative ladder of long exact sequences with $a_*$ vertical maps on $H_n(S'), H_n(L'), H_n(\partial\sigma')$ (isomorphisms by induction) and $a_*$ on $H_n(K')$ in the middle; the [Five Lemma](/theorems/1938) then forces the middle map to be an isomorphism. [/proofplan]

[step:Induct on the number of simplices of $K$] Let $N(K)$ denote the number of simplices of $K$ (equivalently, the number of elements of $K$ regarded as a set of simplices). We prove the theorem by strong induction on $N(K)$. The base case $N(K) = 1$ corresponds to $K = \{\varnothing\}$ or — more usefully — the degenerate edge case of a single vertex, $K = \{\{v\}\}$. In this case $K' = K$ (the barycentric subdivision of a single vertex is itself), the map $a$ is the identity, and $a_* = \operatorname{id}$ on $H_n(K)$ trivially. The interesting base case is $N(K) = $ "single maximal simplex with all faces", which we treat in Step 2. [/step]

[step:Prove the base case when $K$ is the closure of a single simplex]Let $\sigma$ be an $n$-simplex and let $K = \overline{\sigma}$ be the simplicial complex consisting of $\sigma$ together with all its faces. Then $K'$ is the barycentric subdivision of $K$. We show that $a: K' \to K$ induces an isomorphism $a_*: H_m(K') \to H_m(K)$ for every $m \ge 0$. Both $K$ and $K'$ are contractible. Indeed, $|K| = |\sigma|$ is a convex subset of Euclidean space, hence contractible via a straight-line homotopy to any interior point. For $K'$: every simplex of $K'$ contains $\hat{\sigma}$ in its closure (the flag corresponding to any simplex of $K'$ can be extended at the top by $\sigma$ itself), so $K'$ is the [simplicial cone](/theorems/???) over the barycentric subdivision $(\partial \sigma)'$ of the boundary, with apex $\hat{\sigma}$. Simplicial cones have trivial reduced homology, so $\widetilde{H}_m(K') = 0$ for all $m \ge 0$. Consequently \begin{align*} H_m(K) \cong \begin{cases} \mathbb{Z} & m = 0, \\ 0 & m \ge 1, \end{cases} \qquad H_m(K') \cong \begin{cases} \mathbb{Z} & m = 0, \\ 0 & m \ge 1. \end{cases} \end{align*} For $m \ge 1$ the map $a_*: 0 \to 0$ is trivially an isomorphism. For $m = 0$, a generator of $H_0(K')$ is represented by any vertex of $K'$, and $a_*$ sends it to a vertex of $K$, which generates $H_0(K)$. Since $|K|$ is path-connected, all vertices represent the same class in $H_0(K)$, and the map $\mathbb{Z} \to \mathbb{Z}$ of $a_*$ on $H_0$ sends the generator $[v']$ (for any vertex $v' \in V_{K'}$) to $[a(v')]$, which equals the generator of $H_0(K)$. Thus $a_*$ is the identity on $H_0 = \mathbb{Z}$, hence an isomorphism.[/step]

[guided]The single-simplex case is the essential base case because it isolates the geometric fact that **barycentric subdivision does not change the homotopy type of a single simplex**, which is what eventually propagates to arbitrary complexes via Mayer-Vietoris. Why is $|K'|$ contractible? The simplex $|K| = |\sigma|$ is a convex set, and any convex set is contractible via straight-line contraction to any chosen point. Under $|K'| = |K|$ the same contraction works, but we can also use the simplicial-cone structure explicitly: every flag of simplices of $\sigma$ can be extended at the top by $\sigma$ itself, because $\sigma$ is the unique top-dimensional simplex of $K$. This means every simplex of $K'$ is a face of some simplex of $K'$ that contains $\hat{\sigma}$, and the straight-line homotopy to $\hat{\sigma}$ is simplicial on this cone structure. Since both $|K|$ and $|K'|$ are contractible (equivalently, have the homotopy type of a point), both have $H_m = 0$ for $m \ge 1$ and $H_0 = \mathbb{Z}$. For $m \ge 1$ there is nothing to check. For $m = 0$ we only need to check that $a_*$ sends the class of a vertex to the class of a vertex. This is tautological: $a$ is a simplicial map, so it sends vertices to vertices, and $a_\sharp$ preserves the cycles. The class of any vertex generates $H_0$ of a path-connected complex, so the map is the identity $\mathbb{Z} \to \mathbb{Z}$.[/guided]

[step:Set up the inductive step by decomposing $K$ along a maximal simplex] Suppose now $N(K) > 1$ and that the theorem holds for every simplicial complex with strictly fewer simplices. Fix a simplex $\sigma \in K$ of maximal dimension among all simplices of $K$ (so no simplex of $K$ strictly contains $\sigma$). Define \begin{align*} S &:= \overline{\sigma} = \{\tau : \tau \text{ is a face of } \sigma\}, \\ L &:= K \setminus \{\sigma\}, \\ T &:= L \cap S = \partial\sigma = \{\tau : \tau \text{ is a proper face of } \sigma\}. \end{align*} We check these are simplicial complexes and that $K = L \cup S$. The face-closure axiom for $K$ ensures that every face of $\sigma$ is in $K$, so $S \subseteq K$ and $S$ is a simplicial complex. The removal of the single top simplex $\sigma$ leaves the face-closure condition intact on $L = K \setminus \{\sigma\}$, because no other simplex of $K$ has $\sigma$ as a face (maximality of $\sigma$ in $K$). Hence $L$ is a simplicial complex. Clearly $L \cup S = K$ and $L \cap S = \partial \sigma = T$, a simplicial complex. Moreover $N(S) = \dim \sigma + 1 \cdots$ — more precisely, $N(S) = 2^{\dim \sigma + 1}$ counting all non-empty faces plus $\varnothing$ if included; in any case, $S \ne K$ forces $N(S) < N(K)$, and similarly $N(L) = N(K) - 1 < N(K)$, $N(T) < N(S) \le N(K)$. So the inductive hypothesis applies to $S$, $L$, and $T$. Passing to barycentric subdivisions and writing $S', L', T'$ for the subdivisions of $S, L, T$: the construction of $K'$ is natural in the sense that the subdivision of a subcomplex is the subcomplex of simplices of $K'$ corresponding to flags entirely in the subcomplex. Explicitly, \begin{align*} S' = (\overline{\sigma})' \subseteq K', \qquad L' = (K \setminus \{\sigma\})' \subseteq K', \qquad T' = (\partial\sigma)' = S' \cap L', \end{align*} and $K' = S' \cup L'$. The simplicial approximation $a: K' \to K$ restricts to simplicial approximations (to the respective identities) $a: S' \to S$, $a: L' \to L$, $a: T' \to T$: for any vertex $\hat{\tau}$ of $T' \subseteq L' \subseteq K'$, the value $a(\hat{\tau})$ is a vertex of $\tau \in T \subseteq L \subseteq K$, so $a(\hat{\tau}) \in T$, and the restricted vertex map is again of the form described in [Simplicial Approximations to the Identity](/theorems/1935). Hence by that theorem, the restrictions are simplicial approximations to the identity. [/step]

[step:Assemble the Mayer-Vietoris ladder and identify the vertical maps as $a_*$] The [Mayer-Vietoris long exact sequence](/theorems/???) for the decompositions $K = L \cup S$ (with $L \cap S = T$) and $K' = L' \cup S'$ (with $L' \cap S' = T'$) gives two long exact sequences \begin{align*} \cdots \to H_n(T) \to H_n(L) \oplus H_n(S) \to H_n(K) \to H_{n-1}(T) \to \cdots \end{align*} and \begin{align*} \cdots \to H_n(T') \to H_n(L') \oplus H_n(S') \to H_n(K') \to H_{n-1}(T') \to \cdots. \end{align*} The simplicial approximation $a$ and its restrictions induce a commutative diagram between these two sequences in which the vertical maps are the induced maps on homology: \begin{align*} \begin{array}{ccccccccc} H_n(T') & \to & H_n(L') \oplus H_n(S') & \to & H_n(K') & \to & H_{n-1}(T') & \to & H_{n-1}(L') \oplus H_{n-1}(S') \\ \downarrow a_* & & \downarrow a_* \oplus a_* & & \downarrow a_* & & \downarrow a_* & & \downarrow a_* \oplus a_* \\ H_n(T) & \to & H_n(L) \oplus H_n(S) & \to & H_n(K) & \to & H_{n-1}(T) & \to & H_{n-1}(L) \oplus H_{n-1}(S). \end{array} \end{align*} Commutativity of each square follows from the naturality of the Mayer-Vietoris sequence: the connecting homomorphism is natural in maps of pairs $(X; L, S) \to (X'; L', S')$ that respect the cover, and $a: K' \to K$ does so by construction (Step 3). By the inductive hypothesis, $a_*: H_m(T') \to H_m(T)$, $a_*: H_m(L') \to H_m(L)$, and $a_*: H_m(S') \to H_m(S)$ are isomorphisms for all $m$. In particular the direct-sum maps $a_* \oplus a_*$ are isomorphisms. Hence in the ladder above, four of the five vertical maps around the central $a_*: H_n(K') \to H_n(K)$ are isomorphisms — namely the two to the left and the two to the right. [/step]

[step:Apply the Five Lemma to conclude]Applying the [Five Lemma](/theorems/1938) to any five consecutive terms of the Mayer-Vietoris ladder centred at $H_n(K')$ and $H_n(K)$ — with the four flanking vertical maps being isomorphisms — we conclude that the central vertical map \begin{align*} a_*: H_n(K') \to H_n(K) \end{align*} is an isomorphism for every $n \ge 0$. This completes the inductive step. By induction on $N(K)$, the map $a_*: H_n(K') \to H_n(K)$ is an isomorphism for every simplicial complex $K$ and every $n \ge 0$, which is the claim of the theorem.[/step]

[guided]The engine of the inductive step is the Five Lemma. We have a ladder of two Mayer-Vietoris long exact sequences: \begin{align*} H_n(T') \to H_n(L') \oplus H_n(S') \to H_n(K') \to H_{n-1}(T') \to H_{n-1}(L') \oplus H_{n-1}(S') \end{align*} above, and the corresponding $T, L, S, K$ version below. The vertical maps are all forms of $a_*$. The inductive hypothesis gives isomorphisms at every vertical arrow **except** the one over $H_n(K')$ itself — this is the one we want to establish. By the Five Lemma, if the four flanking vertical maps are isomorphisms and the two rows are exact, then the middle vertical map is also an isomorphism. We verify the Five Lemma hypotheses. Exactness of each row is the content of the Mayer-Vietoris theorem. The four flanking vertical maps are isomorphisms by the inductive hypothesis (for the "corner" pieces $T, L, S$), combined with the elementary fact that $\phi \oplus \psi$ is an isomorphism iff both $\phi$ and $\psi$ are. Commutativity of the ladder is naturality of Mayer-Vietoris in simplicial maps respecting the cover, which is a general property verified by tracking how the connecting homomorphism is defined (pick a cycle, split it into chains supported on $L$ and $S$, take the boundary of the $L$-part, descend to $T$). Why does this reduction work? The spatial content of "barycentric subdivision preserves homology" is local: it is a simplex-by-simplex phenomenon. Mayer-Vietoris is precisely the tool that converts local statements (on $L, S, T$) into global statements (on $K = L \cup S$). The base case locks down the single-simplex case, and the induction propagates it up through the combinatorial structure of $K$.[/guided]