Question about the proof of the diamond isomorphism theorem on modular lattice A lattice $(L, \le)$ is a modular lattice @ wiki if the following modular law holds:
$$\forall x \in L: a \le b \implies a \lor (x \land b) = (a \lor x) \land b.$$
The diamond isomorphism theorem @ wiki on modular lattice says that

For any two elements $a,b$ of a modular lattice, one can consider the intervals $[a \land b, b]$ and $[a, a \lor b]$. They are connected by order-preserving maps
  $$\varphi: [a \land b, b] \to [a, a \lor b],
\psi: [a, a \lor b] \to [a \land b, b]$$
  that are defined by $\varphi(x) = x \lor a$ and $\psi(y) = y \land b$.
  Then, $\varphi$ and $\psi$ are both isomorphisms between $[a \land b, b]$ and $[a, a \lor b].$

I tried to prove this theorem by first showing that $\varphi$ preserves the operations $\land$ and $\lor$ as follows:
$$
\forall x_1, x_2 \in [a \land b, b]: \\
\varphi(x_1 \land x_2) = (x_1 \land x_2) \lor a\\
\varphi(x_1) \land \varphi(x_2) = (x_1 \lor a) \land (x_2 \lor a) = (a \lor x_1) \land (x_2 \lor a) =_{\text{modular law}} a \lor (x_1 \land (x_2 \lor a))
$$
What is the next to show that $\varphi(x_1 \land x_2) = \varphi(x_1) \land \varphi(x_2)$?

Edit 1: Note that $a \lor (x_1 \land (x_2 \lor a)) \ge a \lor (x_1 \land x_2)$. How to show the other direction? (Maybe this relies on the fact that $\varphi$ and $\psi$ are bijections.)
Edit 2: The bijection $\varphi$ is a lattice isomorphism can also be verified by showing that $\varphi$ is order-preserving, which is quite easy. A theorem connecting the order-theoretic definition and the algebraic definition of lattice isomorphism may be helpful to show that $\varphi(x_1 \land x_2) = \varphi(x_1) \land \varphi(x_2)$. Any ideas?
 A: Let (M) denote the modular law in included in your question.
Notice that the path you're following doesn't really use the fact that $x \in [a \wedge b, b]$.
Perhaps the best approach is to prove first that $\varphi$ and $\psi$ are inverse of each other.
For example, for $x \in [a \wedge b, b]$,
\begin{align}
\psi\varphi(x)
&= \psi(x \vee a)\\
&= (x \vee a) \wedge b\\
&= x \vee(a \wedge b)\tag{$\because x \leq b$ and (M)}\\
&= x.\tag{$\because a \wedge b \leq x$}
\end{align}
Dually, $\varphi\psi(y)=y$, whenever $y \in [a,a\vee b]$.
Hence $\varphi$ and $\psi$ are bijective maps.
Now, it is clear that both $\varphi$ and $\psi$ are order-preserving maps.
Hence the intervals $[a \wedge b, b]$ and $[a, a \vee b]$ are order-isomorphic.
But an order-isomorphism between lattices is necessarily an isomorphism, and therefore $\varphi$ and $\psi$ are isomorphisms.
A: I come up with the following argument (please review it):
First, we can verify that $\varphi$ and $\psi$ are bijections and that $\varphi^{-1} = \psi$ and $\psi^{-1} = \varphi$.
Next, it is easy to show that $\psi$ preserves the operation $\land$:
$$\psi(y_1 \land y_2) = y_1 \land y_2 \land b = (y_1 \land b) \land (y_2 \land b) = \psi(y_1) \land \psi(y_2).$$
Then, 
$$
\psi\big(\varphi(x_1) \land \varphi(x_2) \big) = \psi\varphi(x_1) \land \psi\varphi(x_2) = x_1 \land x_2.
$$
Therefore, we have
$$
\varphi(x_1 \land x_2) = \varphi\Big(\psi\big(\varphi(x_1) \land \varphi(x_2) \big)\Big) = \varphi(x_1) \land \varphi(x_2).
$$
