Reference for redundance of inversion condition for Lie groups

Question

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.

Answer 1

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}.$$