Reference for redundance of inversion condition for Lie groups The definition of a Lie group is that its multiplication and also the map that sends $g$ to $g^{-1}$ are differentiable maps. It is known that the inversion condition is redundant, using the Implicit Function Theorem.
Q1) I would like to ask if there are any books / notes describing it in the simplest possible way. (Reference request) If anyone can put their proof here it will be good too.
I have read this, and unfortunately I do not really understand it, though admittedly it looks short and neat. Is there a simpler way to prove that inversion is redundant, or is that the simplest proof already?
This is a question in Brocker and tom Dieck, which unfortunately I believe cannot be solved using the material covered in the book alone.
Thanks!
Note: I have read Redundance of the Smoothness of the Inversion Map in the Definition of a Lie Group., to no avail as well.
Q2) Also, what version of Implicit Function Theorem is being used in the proof? After some research, I am pretty sure it is not this version in Wikipedia (https://en.wikipedia.org/wiki/Implicit_function_theorem), but not sure which is the most appropriate version to use.
 A: Let
$$F:G\times G\to G\times G\quad F(g,h)=(g,gh).$$
Then, $F$ is a smooth map since multiplication is assumed to be smooth. 

Lemma. The differential of $F$ at a point $(g,h)\in G\times G$ is given by
  $$(dF)_{(g,h)}:T_gG\times T_hG\to T_gG\times T_{gh}G,\quad (X,Y)\mapsto (X,(dR_h)_g(X)+(dL_g)_h(Y)),\tag{1}$$
  where $R_h:G\to G$ is right multiplication by $h$ and $L_g:G\to G$ left multiplication by $g$.

Proof: This is an easy exercise.
The map $L_g:G\to G$ has a smooth inverse $L_{g^{-1}}$, so it is a diffeomorphism. Thus, $(dL_g)_h$ is an isomorphism and hence $(1)$ is surjective. Since the domain and range have the same dimension, $(1)$ is an isomorphism. This shows that $F$ is a local diffeomorphism. But $F$ is also bijective, so we have shown:

Lemma. The map $F$ is a diffeomorphism.

In particular, its inverse
$$F^{-1}:G\times G\to G\times G,\quad F^{-1}(g,h)=(g,g^{-1}h)$$
is smooth, and hence the following composition is smooth:
$$g\mapsto (g,e)\overset{F^{-1}}{\mapsto} (g,g^{-1})\mapsto g^{-1}.$$
