I'm studying modal logic and in Chapter 3 of this book, one of the proposed exercises (3.4) is to show that distribution of necessity operator over implication is valid, that is, \begin{equation} \square(\varphi \rightarrow \psi) \; \rightarrow \; (\square \varphi \rightarrow \square \psi) \;\; \; \; \;\text{axiom } (\mathbf{K}) \end{equation} I have an idea of how to show this but I can't finish it. I leave my incomplete study below and appreciate any feedback.
To prove that the formula above is valid let $\mathfrak{R}=(K,R_\mathfrak{R},m_\mathfrak{R})$ be any Kripke frame where $K$ is a nonempty set, $R_\mathfrak{R}$ is a binary relation and on $K$ called the accessibility relation and $m_\mathfrak{R}$ is a function assigning a subset of $K$ to each atomic proposition defined inductively as, \begin{align*} & m_\mathfrak{R}(\varphi \rightarrow \psi) \,=\, (K- m_\mathfrak{R}(\varphi)) \cup m_\mathfrak{R}(\psi) \\ & m_\mathfrak{R}(0) \,=\, \emptyset \\ & m_\mathfrak{R}(\square \varphi) \,=\, K-( R_\mathfrak{R} \circ (K- m_\mathfrak{R}(\varphi))) \end{align*}
In order to prove the axiom $(\mathbf{K})$ we must show that $$m_\mathfrak{R} (\square(\varphi \rightarrow \psi)) \subseteq m_\mathfrak{R}(\square \varphi \rightarrow \square \psi)$$
\begin{align*} & m_\mathfrak{R} (\square(\varphi \rightarrow \psi)) &&\text{defn. of } m_\mathfrak{R}\\ =& K-( R_\mathfrak{R} \circ (K- m_\mathfrak{R}(\varphi \rightarrow \psi))) &&\text{defn. of } m_\mathfrak{R} \\ =& K-( R_\mathfrak{R} \circ (K- ( (K-m_\mathfrak{R}(\varphi)) \cup m_\mathfrak{R}(\psi)))) &&\text{dist. of $-$ over $\cup$}\\ =& K-( R_\mathfrak{R} \circ ((K- (K-m_\mathfrak{R}(\varphi))) \cup (K-m_\mathfrak{R}(\psi)))) &&\text{}\\ =& K-( R_\mathfrak{R} \circ (m_\mathfrak{R}(\varphi) \cup (K-m_\mathfrak{R}(\psi)))) &&\text{dist. of $\circ$ over $\cup$}\\ =& K- \bigg( (R_\mathfrak{R} \circ m_\mathfrak{R}(\varphi)) \cup ( R_\mathfrak{R} \circ (K-m_\mathfrak{R}(\psi)))\bigg) &&\text{dist. of $-$ over $\cup$}\\ =& \bigg( K- (R_\mathfrak{R} \circ m_\mathfrak{R}(\varphi)) \bigg) \cup \bigg( K- ( R_\mathfrak{R} \circ (K-m_\mathfrak{R}(\psi)))\bigg) &&\text{defn. of } m_\mathfrak{R}\\ %=& \bigg( K- (R_\mathfrak{R} \circ m_\mathfrak{R}(\varphi)) \bigg) \cup \bigg( K- ( R_\mathfrak{R} \circ (K-m_\mathfrak{R}(\psi)))\bigg) \\ =& \bigg( K- m_\mathfrak{R}(\diamond \varphi) \bigg) \cup m_\mathfrak{R}(\square \psi) &&\text{since } m_\mathfrak{R}(\neg \varphi)\,=\, K-m_\mathfrak{R}(\varphi)\\ =& m_\mathfrak{R}(\neg \diamond \varphi) \cup m_\mathfrak{R}(\square \psi) \\ \subseteq & \color{red}{...?}\\ =& m_\mathfrak{R}(\square \varphi \rightarrow \square \psi) \end{align*}
This is a sketch of how I would prove it.
Suppose that at an arbitrary world $w$ $v(\Box (P \to Q))=1$ and $v(\Box P)=1$.
Suppose further that $wRu$ for an arbitrary world $u$. Then, by def of $\Box$, it follows that $v(P \to Q)=1$ and $v(P)=1$ at $u$. So, $v(Q)=1$ at $u$.
So, if at a world $w$, $v(\Box (P \to Q))=1$ and $v(\Box P)=1)$, then for any world $wRu$, it holds thay $v(Q)=1$ at $u$.
Thus, $\Box (P \to Q) \to (\Box P \to \Box Q)$ is valid.