How to prove the correctness of the binary tree inversion algorithm?
It might be surprising to you, but &quot;the mirror reflection of the right subtree around the center of the root tree is a combination of moving the subtree from root.right to root.left and inverting the subtree around the center of the subtree itself&quot; could be, in fact, part of the definition of &quot;a mirror reflection of the right subtree around the center of the root tree&quot;!
Note that the following definition of &quot;the inversion of a binary tree&quot;, as given in the question, does not define what is the &quot;mirror reflection of the original tree's right subtree&quot;. Although that mirroring is pretty intuitive for a human to understand accurately, given the accompanying illustrations, it is, in fact, not defined/specified clear enough to enable you to prove the correctness of the algorithm formally.

Define the inversion of a binary tree as the tree whose left subtree is a mirror reflection of the original tree's right subtree around the center and right subtree a mirror reflection of the original tree's left subtree.

So, here is the real question.
How do we define mirror reflection formally?
Here is a recursive definition. (This can be seen as taking the given algorithm as the definition basically.)
Given a binary tree $T$ or an empty graph, its mirror reflection $T'$ is another graph such that

$T'$ is empty if $T$ is empty.
$T'$ is a single node that is the same as $T$'s single node if $T$ is a single node.
Otherwise, $T'$ is also a binary tree such that

the root of $T'$ is the same as the root of $T$ and
the left subtree of $T'$ is a mirror reflection of the right subtree of $T$ and
the right subtree of $T'$ is a mirror reflection of the left subtree of $T$.



When $T'$ is a mirror reflection of $T$,  we also say $T'$ is a mirror reflection of $T$ along/around the center of $T$, or any imaginary line that goes from root to a leaf.

Here is a non-recursive definition, that is equivalent to the above.
Given a binary tree $T$ or an empty graph, its mirror reflection is any graph that is isomorphic to the graph $T'$ defined below.

If $T$ is empty, so is $T'$.
Otherwise, let $V$ be the nodes of $T$. Let $V'$ be a copy of $V$; that is, for each $v\in V$, there is unique node in $V'$ that corresponds to $v$. Call that unique node $v'$.

For any two nodes $p, c\in V$ such that $c$ is the left child of $p$, we let $c'$ be the right child of $p'$.
For any two nodes $p, c\in V$ such that $c$ is the right child of $p$, we let $c'$ be the left child of $p'$.




The OP also proposes the following geometric/graphical definition of &quot;inversion of a tree&quot;.

Let $(a,b)$ be the coordinate of the node at depth $a$ that is the $b$-th node from the imaginary center line. If $b$ is negative then the node is to the left of the line. Then the inversion can be defined as the resulting tree if we map $(a,b)$ to $(a,-b)$ and keep the edges accordingly.

The definition above, although graphically clear to a human, might not be very friendly for rigorous reasoning. For example, &quot;the b-th node from the imaginary center line&quot; requires further non-trivial clarification. 

With either of my definitions above, it will be rather easy to prove the correctness of the algorithm.
You might have noticed by now that inversion of a binary tree means exactly the same as its mirror reflection!