It might be surprising to you, but "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" could be, in fact, part of the definition of "a mirror reflection of the right subtree around the center of the root tree"!
Note that the following definition of "the inversion of a binary tree", as given in the question, does not define what is the "mirror reflection of the original tree's right subtree". 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 "inversion of a tree".
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, "the b-th node from the imaginary center line" 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!