Definitions: Let $H^A = \inf \{n \geq 0 : X_n \in A \}$ be the first hitting-time of the set $A$. Let $k_i^A = \mathbb{E}_i(H^A)$ be the mean hitting time of $A$ from $i$.
Theorem: The vector of mean hitting times $k^A = (k_i^A, i \in I)$ is the minimal non-negative solution to $$k_i^A = \begin{cases} 0 & \text{if } i \in A \\ 1 + \sum_j p_{ij}k_j^A & \text{if } i \notin A \end{cases}$$
I know how to prove it's a solution, but I would like to check that my proof of minimality is correct. Specifically, we're told to first show by induction that if $(y_i)$ is any non-negative solution, then $$y_i \geq \mathbb{E}_i\left[\min(H^A, m)\right] \tag{$\ast$} \label{inductiveclaim}$$ for all $m \geq 0$.
Here's my proof:
When $m=0$, the RHS of \eqref{inductiveclaim} is $0$, so the statement is true for all $i$ (since each $y_i$ is non-negative).
For the inductive step, suppose that for all $i$, $y_i \geq \mathbb{E}_i\left[\min(H^A, m-1)\right]$, where $m \geq 1$. If $i \in A$ then $H^A=0$, so again the RHS of \eqref{inductiveclaim} is $0$ and the statement is true. If $i \notin A$, then \begin{align} \mathbb{E}_i\left[\min(H^A, m)\right] &= \sum_j p_{ij}\mathbb{E}_i\left[\min(H^A, m) \mid X_1=j \right] \\ &= \sum_j p_{ij}\left(1 + \mathbb{E}_j\left[\min(H^A, m-1) \right]\right) \\ &= 1 + \sum_j p_{ij}\mathbb{E}_j\left[\min(H^A, m-1) \right] \\ &\leq 1 + \sum_j p_{ij} y_j \\ &= y_i \end{align} which proves the inductive step. Hence \eqref{inductiveclaim} is true for all $i$ and $m$.
Then, taking the limit as $m \to \infty$, $y_i \geq \mathbb{E}_i\left[H^A\right] = k_i^A$ . $\square$
Is this correct, and if so, how can we rigorously justify the step from the first line to the second line in the induction proof?