[proofplan]
The forward implication is exactly the finite Birkhoff representation theorem: a finite distributive lattice is recovered as the lattice of order ideals of its join-irreducible elements by sending an element to the join-irreducibles below it. For the converse, assume the displayed map is a lattice isomorphism. The lattice of order ideals of any finite poset is distributive because its meet and join are intersection and union. Since a lattice isomorphism preserves meet and join, the distributive identities transfer back from the order-ideal lattice to $L$.
[/proofplan]
[step:Apply Birkhoff representation in the distributive case]
Assume first that $L$ is distributive. The poset $J_{\mathrm{irr}}(L)$ is finite because it is a subset of the finite set $L$, and its order is the order inherited from $L$. By [citetheorem:8145], applied to the finite distributive lattice $L$, the map
\begin{align*}
\Phi:L\to \mathcal{J}(J_{\mathrm{irr}}(L)), \qquad \Phi(x)=\{j\in J_{\mathrm{irr}}(L):j\le x\}
\end{align*}
is a lattice isomorphism. This proves the forward implication.
[/step]
[step:Identify the lattice operations on order ideals]
Assume conversely that $\Phi:L\to \mathcal{J}(J_{\mathrm{irr}}(L))$ is a lattice isomorphism. Put
\begin{align*}
P=J_{\mathrm{irr}}(L).
\end{align*}
For order ideals $I,K\in \mathcal{J}(P)$, their meet in $\mathcal{J}(P)$ is $I\cap K$, and their join in $\mathcal{J}(P)$ is $I\cup K$.
Indeed, $I\cap K$ is an order ideal because if $p\in I\cap K$ and $q\le p$ in $P$, then $q\in I$ and $q\in K$, hence $q\in I\cap K$. Similarly, $I\cup K$ is an order ideal because if $p\in I\cup K$ and $q\le p$, then $p$ lies in at least one of $I$ or $K$, and the order-ideal property of that ideal gives $q\in I\cup K$. The set $I\cap K$ is the greatest lower bound of $I$ and $K$ under inclusion, and $I\cup K$ is the least upper bound of $I$ and $K$ under inclusion.
[guided]
We need to know the concrete meet and join operations in the target lattice, because distributivity is a statement about how meet and join interact. Let $P=J_{\mathrm{irr}}(L)$, regarded as a finite poset with the order inherited from $L$. The elements of $\mathcal{J}(P)$ are order ideals of $P$, ordered by inclusion.
Take two order ideals $I,K\in \mathcal{J}(P)$. We first verify that $I\cap K$ is again an order ideal. Let $p\in I\cap K$, and let $q\in P$ satisfy $q\le p$. Since $p\in I$ and $I$ is an order ideal, we get $q\in I$. Since $p\in K$ and $K$ is an order ideal, we also get $q\in K$. Thus $q\in I\cap K$, so $I\cap K$ is an order ideal. It is contained in both $I$ and $K$, and any order ideal contained in both $I$ and $K$ is contained in their intersection. Therefore $I\cap K$ is the meet of $I$ and $K$ in $\mathcal{J}(P)$.
Now we verify the join. Let $p\in I\cup K$, and let $q\in P$ satisfy $q\le p$. If $p\in I$, then the order-ideal property of $I$ gives $q\in I\subset I\cup K$. If $p\in K$, then the order-ideal property of $K$ gives $q\in K\subset I\cup K$. Hence $I\cup K$ is an order ideal. It contains both $I$ and $K$, and any order ideal containing both $I$ and $K$ contains their union. Therefore $I\cup K$ is the join of $I$ and $K$ in $\mathcal{J}(P)$.
Thus the order-ideal lattice has the familiar set-theoretic operations:
\begin{align*}
I\wedge K=I\cap K, \qquad I\vee K=I\cup K.
\end{align*}
[/guided]
[/step]
[step:Prove the order-ideal lattice is distributive]
Let $I,K,M\in \mathcal{J}(P)$. Using the operation descriptions from the previous step and the distributive law for intersection over union of sets, we have
\begin{align*}
I\wedge (K\vee M) = I\cap (K\cup M) = (I\cap K)\cup (I\cap M) = (I\wedge K)\vee (I\wedge M).
\end{align*}
Thus $\mathcal{J}(P)$ satisfies the meet-over-join distributive identity. The dual distributive identity also holds because union distributes over intersection:
\begin{align*}
I\vee (K\wedge M) = I\cup (K\cap M) = (I\cup K)\cap (I\cup M) = (I\vee K)\wedge (I\vee M).
\end{align*}
Therefore $\mathcal{J}(P)$ is a distributive lattice.
[/step]
[step:Transfer distributivity back across the lattice isomorphism]
Let $x,y,z\in L$. Since $\Phi$ is a lattice isomorphism, it preserves finite meets and joins:
\begin{align*}
\Phi(x\wedge (y\vee z))=\Phi(x)\wedge_{\mathcal{J}(P)}(\Phi(y)\vee_{\mathcal{J}(P)}\Phi(z)).
\end{align*}
Because $\mathcal{J}(P)$ is distributive, the right-hand side equals
\begin{align*}
(\Phi(x)\wedge_{\mathcal{J}(P)}\Phi(y))\vee_{\mathcal{J}(P)}(\Phi(x)\wedge_{\mathcal{J}(P)}\Phi(z)).
\end{align*}
Using preservation of meets and joins again, this is
\begin{align*}
\Phi((x\wedge y)\vee (x\wedge z)).
\end{align*}
Hence
\begin{align*}
\Phi(x\wedge (y\vee z))=\Phi((x\wedge y)\vee (x\wedge z)).
\end{align*}
Since $\Phi$ is injective, it follows that
\begin{align*}
x\wedge (y\vee z)=(x\wedge y)\vee (x\wedge z).
\end{align*}
Thus $L$ is distributive. This proves the converse implication and completes the proof.
[/step]
