The pointwise norm on a tangent space is smooth off the zero vector

Set-up and the zero-dimensional case. [F2, F3, F4, given] By [F2] the space $T_{p}M$ is an $n$-dimensional real vector space. If $n=0$, then $T_{p}M=\{0_p\}$ by [F3], so $T_{p}M\setminus \{0_p\}=\mathrm{\varnothing }$ and the smoothness assertion is vacuous; assume henceforth $n\ge 1$. By [F3] the finite-dimensional space $T_{p}M$ has a finite basis, and we fix one ordered basis $e_1,\dots ,e_n$; fixing a single basis is one existential instantiation and invokes no choice principle. By [F4] every $w\in T_{p}M$ has exactly one coordinate list $(v^1(w),\dots ,v^n(w))\in {\mathbb{R}}^n$ with $w={\sum }_{i=1}^n{v}^i(w)e_i$. The coefficient map $v:T_{p}M\to {\mathbb{R}}^n$, $v(w)=(v^1(w),\dots ,v^n(w))$, is linear and bijective: linear because the coordinate list of $\alpha w+\beta w^{\mathrm{\prime }}$ is $\alpha v(w)+\beta v(w^{\mathrm{\prime }})$ by uniqueness in [F4], injective because $v(w)=0$ forces $w={\sum }_{i}0e_i=0_p$, and surjective because an arbitrary $\lambda \in {\mathbb{R}}^n$ is the coordinate list of ${\sum }_i{\lambda }_i{e}_i$ again by uniqueness in [F4].

The square root is smooth on $(0,\mathrm{\infty })$. [F5, F6, F7, F8, F9, F10, given] Let $x_0>0$ and put $t_0:=\sqrt{x_0}>0$, so that $t_0^2=x_0$ by [F10]. The function $f(t):=t^2$ on the open set $U:=(0,\mathrm{\infty })\subseteq \mathbb{R}$ is the product of the identity map with itself; the identity map is $C^k$ for every $k$ by the definition in [F5] (all its iterated partial derivatives are the constants $0$ and $1$), so [F6] makes $f$ $C^k$ for every $k$, that is, smooth. Its derivative at $t_0$ is $f^{\mathrm{\prime }}(t_0)=2t_0\mathrm{\ne }0$ by [F7], so the derivative is invertible and [F8] supplies open neighbourhoods $V$ of $t_0$ and $W$ of $x_0$ with $f{\mathrm{\mid }}_V:V\to W$ bijective and $C^1$ inverse $g:W\to V$; since $f$ is $C^k$ for every $k$, [F9] makes this same local inverse $C^k$ for every $k$, that is, smooth. For $y\in W$ we have $g(y)\in V\subseteq (0,\mathrm{\infty })$ and $f(g(y))=y$, that is, $g(y)\ge 0$ and $g(y{)}^2=y$; by the uniqueness clause of [F10] applied to the nonnegative number $y$, $g(y)=\sqrt{y}$. Hence the square root function agrees on the open neighbourhood $W$ of the arbitrary point $x_0>0$ with the smooth map $g$, so it is smooth at every point of $(0,\mathrm{\infty })$.

The norm squared is a quadratic form in the coordinates. [F1, F4, step 1.1] Let $w={\sum }_{i=1}^n{v}^i(w)e_i$ and $w^{\mathrm{\prime }}={\sum }_{j=1}^n{v}^{\mathrm{\prime }j}(w^{\mathrm{\prime }})e_j$ be two vectors of $T_{p}M$. Bilinearity of $g_p$ [F1] and the coordinate expansion [F4] give $g_p(w,w^{\mathrm{\prime }})={\sum }_{i,j=1}^n{v}^i(w)v^{\mathrm{\prime }j}(w^{\mathrm{\prime }})c_{ij},c_{ij}:=g_p(e_i,e_j)\in \mathbb{R},$ a finite sum of products of coordinates with the constants $c_{ij}$. In particular $Q(w):=g_p(w,w)=q(v(w)),q(\lambda ):={\sum }_{i,j=1}^n{c}_{ij}{\lambda }_i{\lambda }_j,$ for $w\in T_{p}M$ and $\lambda \in {\mathbb{R}}^n$. Positive definiteness [F1] gives $Q(w)>0$ for $w\mathrm{\ne }{0}_p$ and $Q(0_p)=0$; since the coefficient isomorphism $v$ of step 1.1 is linear and bijective with $v(0_p)=0$, this reads $q(\lambda )>0\text{ for }\lambda \mathrm{\ne }0,q(0)=0.$

The quadratic polynomial is smooth. [F5, F6, step 2.1] Each coordinate function $\lambda \mapsto {\lambda }_i$ on ${\mathbb{R}}^n$ is $C^k$ for every $k$ by the definition in [F5]: its iterated coordinate partial derivatives are the constants $0$ and $1$. The functions $\lambda \mapsto {\lambda }_i{\lambda }_j$ are products of $C^k$ maps and the functions $\lambda \mapsto c_{ij}{\lambda }_i{\lambda }_j$ are their scalar multiples, so each is $C^k$ for every $k$ by [F6]; the finite sum $q$ defining the quadratic form is again $C^k$ for every $k$ by [F6], that is, $q$ is smooth. Together with step 2.1 this yields the positivity statement $q(\lambda )>0$ exactly for $\lambda \mathrm{\ne }0$.

The pointwise norm is smooth off zero in the coordinates of the basis. [F1, F6, F11, step 1.1, step 1.2, step 2.1, step 3.1] For $w\mathrm{\ne }{0}_p$ the pointwise norm is $N_p(w)=\mathrm{\mid }w{\mathrm{\mid }}_g=\sqrt{g_p(w,w)}=\sqrt{q(v(w))}$ by [F1], [F11] and step 2.1, and $q(v(w))>0$ by step 3.1. By step 1.2 the square root is smooth on $(0,\mathrm{\infty })$, and step 3.1 makes $q$ smooth on the open set ${\mathbb{R}}^n$; the smooth map $q$ carries ${\mathbb{R}}^n\setminus \{0\}$ into $(0,\mathrm{\infty })$ by step 3.1, so the composite $\sigma (\lambda ):=\sqrt{q(\lambda )}$ is $C^k$ for every $k$ on the open set ${\mathbb{R}}^n\setminus \{0\}$ by the composition clause of [F6]; that is, $\sigma$ is smooth. By step 1.1 the coefficient map $v$ is a linear bijection, so $N_p=\sigma \circ v$ on $T_{p}M\setminus \{0_p\}$; this exhibits the coordinate representative $\sigma ={\sigma }_e$ of the pointwise norm in the ordered basis $e_1,\dots ,e_n$ as a smooth function on ${\mathbb{R}}^n\setminus \{0\}$.

Basis independence and boundary audit. [F4, F5, F6, F10, step 1.1, step 4.1] Let $e_1^{\mathrm{\prime }},\dots ,e_n^{\mathrm{\prime }}$ be a second ordered basis with coefficient isomorphism $v^{\mathrm{\prime }}$ and representative ${\sigma }_{e^{\mathrm{\prime }}}$. The change of coordinates $v^{\mathrm{\prime }}\circ v^{-1}:{\mathbb{R}}^n\to {\mathbb{R}}^n$ is a linear bijection, hence $C^k$ for every $k$ with $C^k$ inverse $v\circ v^{\mathrm{\prime }-1}$: a linear map has component functions that are finite sums of scalar multiples of coordinate functions, and both it and its inverse are covered by the algebra and composition clauses of [F6]; the coordinate lists are related by $v^{\mathrm{\prime }}(w)=(v^{\mathrm{\prime }}\circ v^{-1})(v(w))$, so ${\sigma }_{e^{\mathrm{\prime }}}={\sigma }_e\circ (v\circ v^{\mathrm{\prime }-1})$ is smooth exactly when ${\sigma }_e$ is, again by [F6]. This proves the claimed independence of the basis. The audit: the zero-dimensional case was disposed of in step 1.1, so the excluded vector $0_p$ is the only point at which smoothness is not asserted, and there $N_p(0_p)=\sqrt{q(0)}=0$ by step 2.1 and the square root is not used, since step 1.2 asserts smoothness of the square root only on $(0,\mathrm{\infty })$, whose endpoint $0$ is exactly what is being excluded; in dimension one the form is $q(\lambda )=c_{11}{\lambda }^2$ with $c_{11}>0$ and $N_p$ is $\sqrt{c_{11}}\mathrm{\mid }\lambda \mathrm{\mid }$ in the coordinate, smooth off the origin and subsumed by the general composite; no degenerate case arises because positive definiteness [F1] makes $q$ strictly positive off zero, so $q$ never takes the value $0$ on the domain of $\sigma$; no choice principle is used beyond the single existential instantiation of the basis in step 1.1, and the two Euclidean closures of [F6] and the uniqueness clause of [F10] are theorems of ZF; the lemma states a smoothness assertion and no equivalence, so neither forward nor reverse direction of a biconditional is claimed. $\mathrm{\square }$