Adjoint is a smooth Lie-group representation

For $g,h,x\in G$, associativity and $(gh{)}^{-1}=h^{-1}{g}^{-1}$ give $C_{gh}(x)=(gh)x(gh{)}^{-1}=g(hx{h}^{-1})g^{-1}=(C_g\circ C_h)(x)$, while $C_e={\mathrm{id}}_G$.

It remains to verify smoothness, not merely pointwise differentiability. Define $\mathrm{\Phi }:G\times G\to G$ by $\mathrm{\Phi }(g,x)=gx{g}^{-1}$; [F2] makes $\mathrm{\Phi }$ smooth. Fix a finite basis of $\mathfrak{g}$ and a chart at $e$ whose coordinate differential carries it to the standard basis. Around an arbitrary $g_0$, take any chart in the first variable and use the fixed identity chart in the second and target variables. Since $\mathrm{\Phi }(g,e)=e$, the matrix entries of ${\mathrm{Ad}}_g=d_x{\mathrm{\Phi }}_{(g,e)}$ in that basis are the first partial derivatives with respect to the second-variable coordinates, evaluated at the identity coordinate. These entries are smooth functions of the first-variable coordinates because the coordinate representative of $\mathrm{\Phi }$ is smooth. By the standard target structure in [F1], $g\mapsto {\mathrm{Ad}}_g$ is smooth near $g_0$, and $g_0$ was arbitrary.

Differentiate step 1.1 at $e$. Since $C_h(e)=e$, the chain rule [F3] gives ${\mathrm{Ad}}_{gh}=d(C_g{)}_e\circ d(C_h{)}_e={\mathrm{Ad}}_g\circ {\mathrm{Ad}}_h$ and ${\mathrm{Ad}}_e={\mathrm{id}}_{\mathfrak{g}}$. Hence $\mathrm{Ad}$ is a group homomorphism.

Step 2.1 supplies the group-homomorphism law and step 1.2 supplies smoothness, so [F4] identifies $\mathrm{Ad}$ as the claimed smooth representation.

A Lie group is nonempty and boundaryless. If $\dim G=0$, then $\mathfrak{g}=0$ and the target is the one-point group, so the map is constant and smooth; dimension one uses the same coordinate argument. No metric, nondegeneracy, interval, or endpoint occurs. The displayed consequences of the homomorphism assertion in the Statement are established in step 2.1. Fixing one finite basis and finitely many charts in a local smoothness test makes no choice from a family, so the proof is choice-free.