# Formal Proof that $f^{-1} \circ f = id_x \ , \forall f$

Given $f$ as an invertible function with domain $X$ and codomain $Y$, then we can say

$$f^{-1}(f(x)) = x$$

Or since they are both logically equivalent

$$f(f^{-1}(x)) = x$$

This can also be written more formally as :

$$f^{-1} \circ f = id_x \ \Leftrightarrow f \circ f^{-1} = id_x$$

It is a relatively simple and common, property of functions, yet I haven't seen a formal proof of it. So how do you prove this statement $\ \forall f\$, where $f$ is an arbitrary invertible function?

If the proof requires higher mathematics (e.g Category Theory, Morphisms etc.), please do not hesitate to include them.

• How are you defining the inverse of an invertible function? – davidlowryduda Apr 21 '16 at 0:06
• I think they're just trying to prove that $f \circ g=id_X$ implies $g \circ f=id_Y$ for any function $f$ from $X$ to $Y$ and any function $g$ from $Y$ to $X$. – Noble Mushtak Apr 21 '16 at 0:07
• On your second line you have an expression on the left side of an implication and a proposition on the right. – Dan Piponi Apr 21 '16 at 0:08
• I don't completely understand this question. If you're asking whether having a right inverse implies having a left inverse (or the other way around), then this is not true. If you're asking whether the right inverse and the left inverse of a function have to be equal if they both exist, this follows from $l = l \circ id = l \circ f \circ r = id \circ r = r$ by associativity (where $r$ and $l$ denote the inverses of $f$). If you're asking whether $f \circ f^{-1} = id$ iff $f(f^{-1}(x)) = x$ for all $x$, this holds because two functions are equal iff their values are equal at each point. – Abel Apr 21 '16 at 0:10
• It feels a bit weird to say they are logically equivalent, since they are both just true if we assume that $f$ is invertible (and both are required for invertibility), as in Tryss's answer. Actually, you can't even say $f(f^{-1}(y))=y$ for all $y$ without assuming the existence of $f^{-1}$, which in turn implies that also $f^{-1}(f(x))=x$ for all $x$, by definition. The most you could say is my second point: if you have functions $g$ and $h$ such that $f(g(y))=y$ for all $y$ and $h(f(x))=x$ for all $x$, then $g=h$ and we call this function $f^{-1}$. – Abel Apr 21 '16 at 0:20

A function $f:X\to Y$ is said to be invertible if there exists a function $g:Y\to X$ such that
$$\forall y \in Y, f(g(y)) = y \text{ and } \forall x\in X, g(f(x)) = x$$
If $f$ has this property, we call $g$ the inverse of $f$ and note it $f^{-1}:= g$