Proof of Triangle Inequality for Finite Sums of Vectors

We argue by applying the principle of induction to the set of natural numbers $n$ for which the assertion holds for every family on $[n]$, writing $S$ for the successor map of Natural Numbers. We use $[1]=\{1\}$ and $[S(n)]=[n]\cup\{S(n)\}$ from claims 2 and 3 of Basic Properties of Initial Segments of the Natural Numbers, the base clause and recursion for vector sums from claim 1 of Properties of Finite Sums of Vectors, the corresponding clauses for scalar sums from claim 1 of Properties of Finite Sums, and the triangle inequality for the norm.

Base case. For $n=1$ we have $\sum_{k=1}^{1}v_{k}=v_{1}$ and $\sum_{k=1}^{1}\lVert v_{k}\rVert=\lVert v_{1}\rVert$, so both sides are equal and the inequality holds by reflexivity of the order.

Induction step. Assume the assertion for $n$ and let $v$ be defined on $[S(n)]$. By the recursion for vector sums and the triangle inequality for the norm,

The inductive hypothesis, applied to the restriction of $v$ to $[n]$ and combined with the restriction part of claim 1 of Properties of Finite Sums of Vectors and of claim 1 of Properties of Finite Sums, gives $\lVert\sum_{k=1}^{n}v_{k}\rVert\le\sum_{k=1}^{n}\lVert v_{k}\rVert$. Adding $\lVert v_{S(n)}\rVert$ to both sides, which preserves the order by the first order axiom of Ordered Field, and then using the recursion for scalar sums,

Transitivity of the order now gives the asserted inequality for $S(n)$, completing the induction.