[Math] Proof – Inverse of linear function is linear

functionslinear algebraproof-verificationproof-writingsoft-question

This is my first proof related to linear functions.
It refers to the linear-algebra-$\textit{linear}$ (not the calculus-$\textit{linear}$).
Please comment.

Theorem

The inverse of a linear bijection is linear.

Proof

Let $X,Y$ be vector spaces over a common field.
Let $f : X \rightarrow Y$ be a linear bijection.
We denote by $f^{-1}$ the inverse of $f$.
It remains to prove that $f^{-1}$ is linear,
i.e. both $\textit{additive}$ and $\textit{homogeneous}$.

Additivity

Let $y_1, y_2 \in Y$.
We prove that $$f^{-1}(y_1 + y_2) = f^{-1}(y_1) + f^{-1}(y_2).$$
\begin{equation*}
\begin{split}
f^{-1}(y_1) + f^{-1}(y_2)
&= f^{-1}\Big( f\big( f^{-1}(y_1) + f^{-1}(y_2) \big) \Big) && \quad \text{by bijectivity} \\
&= f^{-1}\Big( f\big( f^{-1}(y_1) \big) +
f\big( f^{-1}(y_2) \big) \Big) && \quad \text{by linearity of } f \\
&= f^{-1}\Big( y_1 + f\big( f^{-1}(y_2) \big) \Big) && \quad \text{by bijectivity} \\
&= f^{-1}(y_1 + y_2) && \quad \text{by bijectivity}\phantom{\Big(\Big)} \\
\end{split}
\end{equation*}

Homogeneity

Let $y \in Y$ and let $s$ be a scalar.
We prove that $$f^{-1}(sy) = sf^{-1}(y).$$
\begin{equation*}
\begin{split}
sf^{-1}(y)
&= f^{-1}\Big( f\big( sf^{-1}(y) \big) \Big) && \quad \text{by bijectivity} \\
&= f^{-1}\Big( sf\big( f^{-1}(y) \big) \Big) && \quad \text{by linearity of } f \\
&= f^{-1}(sy) && \quad \text{by bijectivity}\phantom{\Big(\Big)} \\
\end{split}
\end{equation*}

QED

Best Answer

General principle: You can demonstrate two vectors in X are equal by showing that f maps them to the same vector in Y (since f is injective). For example: Apply $f$ to $f^{-1}(y_1)+f^{-1}(y_2)$ and argue that the result is $y_1 + y_2$. Do a similar calculation involving $f^{-1}(y_1+y_2)$. You should then be able to see why the inverse of an additive injection is additive. Homogeneity can be approached the same way. You may observe that surjectivity of $f$ is not really involved in what is going on here.