Why is this function a (global) diffeomorphism? Let $f:\mathbb R\to \mathbb R$ a function of class $C^1$ with $|f'(t)|\le k< 1$ for every $t\in \mathbb R$. I would like to prove $\varphi:\mathbb R^2\to \mathbb R^2$ defined as $\varphi(x,y)=(x+f(y),y+f(x))$ is a diffeomorphism from $\mathbb R^2$ to $\mathbb R^2$.
My attempt
Calculating the determinant of the Jacobian:
$\det\mathfrak J(\varphi(x,y))$=
$\det\begin{bmatrix}
1 & f'(y)\\
f'(x) & 1
\end{bmatrix}=1-f'(x)f'(y)$
Therefore,
$|\det\mathfrak J(\varphi(x,y))|=|1-f'(x)f'(y)|\ge1-|f'(x)f'(y)|=1-|f'(x)||f'(y)|>0\ (\text{I'm using the fact $|f'(t)|<1$ for every $t\in \mathbb R$})$
Thus, $\varphi$ is of class $C^1$ (because $f\in C^1$) and the determinant of the Jacobian is non-zero for every point in $\mathbb R^2$. Using the inverse function theorem, we have for every point in $\mathbb R^2$ has a neighborhood such that the restriction to this one is a diffeomorphism (can we say $\varphi$ is a local diffeomorphism?)
Am I right so far? If yes, how can I finish the proof? (I have to prove $\varphi$ is a global diffeomorphism)
 A: As said in the comments and in the other answer we need injectivity and surjectivity.
For injectivity: we have from the Mean Value Theorem that $|f(x)-f(y)|\leq|f'(c)||x-y|\leq k|x-y|$
Now take $(x_1,y_1),(x_2,y_2)\in\mathbb{R}^2$
Taking the norm of sum $|.|_s$
$|\varphi(x_1,y_1)-\varphi(x_2,y_2)|_s=|(x_1+f(y_1),y_1+f(x_1))-(x_2+f(y_2),y_2+f(x_2))|=|x_1-x_2+f(y_1)-f(y_2)|+|y_1-y_2+f(x_1)-f(x_2)|\geq |x_1-x_2|-|f(y_1)-f(y_2)|+|y_1-y_2|-|f(x_1)-f(x_2)|\geq|x_1-x_2|-k|x_1-x_2|+|y_1-y_2|-k|y_1-y_2|=(1-k)|x_1-x_2|+(1-k)|y_1-y_2|$
Now making $\varphi(x_1,y_1)=\varphi(x_2,y_2)$, and with $1-k>0$, we get
$0\geq(1-k)|x_1-x_2|+(1-k)|y_1-y_2|\Rightarrow x_1=x_2,y_1=y_2$
Up to now we have a bijection $\varphi:\mathbb{R}^2\to\varphi(\mathbb{R}^2)$
From $\det[J(φ(x,y))]\ne0$, by the Open Map Theorem, we have that $\varphi(\mathbb{R}^2)$ is open.
But also $\varphi(\mathbb{R}^2)$ is closed. As, if $z\in Cl(\varphi(\mathbb{R}^2))$, there is $z_k\in\varphi(\mathbb{R}^2)$ with $\lim_{k\to\infty}z_k=z$ And there is $x_k\in\mathbb{R}^2$, with $f(x_k)=z_k$. With $|f(x)-f(y)|\leq k|x-y|$, these sequences converge, and finally we get that $z\in\varphi(\mathbb{R}^2)$.
But $\varphi(\mathbb{R}^2)$ being open and closed in $\mathbb{R}^2$, we can split $\mathbb{R}^2=\varphi(\mathbb{R}^2)\cup\mathbb{R}^2-\varphi(\mathbb{R}^2)$, as $\mathbb{R}^2$ is connected, we have the desired $\varphi(\mathbb{R}^2)=\mathbb{R}^2$
A: So far you have shown that it is a local diffeomorphism. So you have to show injectivity and surjectivity. For injectivity you can look at the line between to points which have the same image and then find a contradiction. And for surjectivity you can look at a sufficiently large circle and ask if it contains a disk.
Surjectivity: 

 What do we get from $\vert f'(t) \vert \le k <1 $ for surjectivity? We
 know that $f(t) <K x$ for $k< K<1$ and sufficiently large $t$.
 
 So assume $t_0$ and $K$ have this given property. What can we say
 about the image of the circle in $\Bbb R^2$ with radius $t_0$? The
 point $(x,y)$ is mapped inside a circle of radius $K$ around $(x,y)$.
 What we get is a path surrounding the disc of radius $(1-K)t_o$. But
 since the image of a disc is contractible and thus can not have holes,
 we know that the disc of radius $(1-K)t_o$ is in the image of the disc
 with radius $t_0$. This gives us surjectivity.

Injectivity: 

 For injectivity assume $f(x,y)=f(x',y')$. Then consider the line
 $t(x,y) +(1-t)(x',y')$  between $(x,y)$ and $(x',y')$. Applying $f$ to
 it gives in both components a function in $t$ whose derivative has to
 vanish at some point by mean value theorem. The derivate looks like
 this: $$(x-x') +f'(ty+(1-t)y')(y-y')$$ and the same with $x$ and $y$
 exchanged. Since $\vert f'(t) <1$ at most one of the equation can have
 a zero, depending on $\vert x-x' \vert < \vert y-y' \vert$ or $\vert y-y' \vert \le \vert x-x' \vert$, which is a contradiction.

