Proof of Properties of Finite Sums of Vectors

Write $\sigma:[n]\to V$ for the map used in the definition of the finite sum of the family $v$, so that $\sum_{k=1}^{j}v_{k}=\sigma(j)$ for every $j\in[n]$. Throughout we use the axioms of a vector space over $K$ (in particular the associativity and commutativity of vector addition, the neutrality of the zero vector $0_{V}$, and the identity $\lambda(x+y)=\lambda x+\lambda y$), and the following facts about initial segments from claims 1 to 4 of Basic Properties of Initial Segments of the Natural Numbers: $1\in[n]$ and $n\in[n]$; $[1]=\{1\}$; $[S(n)]=[n]\cup\{S(n)\}$ with $S(n)\notin[n]$; and $[j]\subseteq[n]$ whenever $j\le n$. Claims 2 to 7 are proved by applying the principle of induction to the set of natural numbers $n$ for which the assertion in question holds for all admissible data on $[n]$.

Claim 1. Restriction. Let $j\in[n]$, let $v'$ be the restriction of $v$ to $[j]$, which is defined because $[j]\subseteq[n]$, and let $\sigma':[j]\to V$ be the map associated with $v'$ by Existence and Uniqueness of Iterates of a Binary Operation, so that $\sum_{k=1}^{i}v'_{k}=\sigma'(i)$ for every $i\in[j]$. Let $\rho$ be the restriction of $\sigma$ to $[j]$. Since $1\in[j]$ we have $\rho(1)=\sigma(1)=v_{1}=v'_{1}$. If $m\in\mathbb{N}$ satisfies $S(m)\in[j]$, then $S(m)\in[n]$, and $m\in[j]$ because $m<S(m)\le j$ by claims 5 and 1 of Properties of the Order on the Natural Numbers; hence $\rho(S(m))=\sigma(S(m))=\sigma(m)+v_{S(m)}=\rho(m)+v'_{S(m)}$. By the uniqueness part of Existence and Uniqueness of Iterates of a Binary Operation we get $\rho=\sigma'$, so $\sum_{k=1}^{i}v'_{k}=\sigma(i)=\sum_{k=1}^{i}v_{k}$ for every $i\in[j]$.

Recursion. Directly from the definition, $\sum_{k=1}^{1}v_{k}=\sigma(1)=v_{1}$, and for $m$ with $S(m)\in[n]$,

We refer to these two identities as the base clause and the recursion; the corresponding identities for finite sums of scalars are claim 1 of Properties of Finite Sums. By the restriction part of claim 1 here, and by the restriction part of claim 1 of Properties of Finite Sums for scalars, a sum $\sum_{k=1}^{n}$ formed from data given on $[S(n)]$ agrees with the corresponding sum formed from their restriction to $[n]$, so the inductive hypotheses below apply to it.

Claim 2. For $n=1$ we have $[1]=\{1\}$ and both sides equal $u_{1}+v_{1}$ by the base clause. Assume the identity for $n$ and let $u,v$ be defined on $[S(n)]$. By the recursion, the inductive hypothesis applied to the restrictions of $u$ and $v$ to $[n]$, and the commutativity and associativity of vector addition,

which rearranges to

Claim 3. For $n=1$ both sides equal $\lambda v_{1}$ by the base clause. Assume the identity for $n$. By the recursion, the inductive hypothesis and the vector space identity $\lambda(x+y)=\lambda x+\lambda y$,

Claim 4. Sums in $W$ satisfy the base clause and the recursion as well, by claim 1 applied to $W$ in place of $V$. For $n=1$ both sides equal $T(v_{1})$. Assume the identity for $n$. By the recursion in $V$, the additivity of the linear map $T$, the inductive hypothesis, and the recursion in $W$,

Claim 5. First identity. For $n=1$ both sides equal $\langle w,v_{1}\rangle$ by the two base clauses. Assume it for $n$. By the recursion for vector sums, additivity in the second argument (condition 2 of Complex Inner Product Space), the inductive hypothesis, and the recursion for scalar sums,

Second identity. The same induction applies, with additivity in the first argument (claim 1 of Elementary Properties of a Complex Inner Product) in place of additivity in the second argument.

Claim 6. Apply claim 5 to the family $k\mapsto c_{k}v_{k}$ on $[n]$. For the first identity, homogeneity in the second argument (condition 3 of Complex Inner Product Space) gives $\langle w,c_{k}v_{k}\rangle=c_{k}\langle w,v_{k}\rangle$ for every $k\in[n]$, so the two families $k\mapsto\langle w,c_{k}v_{k}\rangle$ and $k\mapsto c_{k}\langle w,v_{k}\rangle$ coincide and therefore have the same finite sum; hence

For the second identity, conjugate homogeneity in the first argument (claim 2 of Elementary Properties of a Complex Inner Product) gives $\langle c_{k}v_{k},w\rangle=\overline{c_{k}}\,\langle v_{k},w\rangle$ for every $k\in[n]$, and the same argument yields

Claim 7. For $n=1$ we have $[1]=\{1\}$, so $i=1$ and $\sum_{k=1}^{1}v_{k}=v_{1}=v_{i}$ by the base clause. Assume the assertion for $n$, let $v$ be defined on $[S(n)]$, and let $i\in[S(n)]=[n]\cup\{S(n)\}$ satisfy $v_{k}=0_{V}$ for every $k\in[S(n)]$ with $k\ne i$.

If $i\in[n]$, then $S(n)\ne i$ because $S(n)\notin[n]$, so $v_{S(n)}=0_{V}$. The restriction of $v$ to $[n]$ satisfies the same hypothesis with the same distinguished index $i$, so the inductive hypothesis gives $\sum_{k=1}^{n}v_{k}=v_{i}$, and the recursion together with the neutrality of $0_{V}$ gives $\sum_{k=1}^{S(n)}v_{k}=v_{i}+0_{V}=v_{i}$.

If $i=S(n)$, then $v_{k}=0_{V}$ for every $k\in[n]$. Applying the inductive hypothesis to the restriction of $v$ to $[n]$ with distinguished index $1$ gives $\sum_{k=1}^{n}v_{k}=v_{1}=0_{V}$, so the recursion gives $\sum_{k=1}^{S(n)}v_{k}=0_{V}+v_{S(n)}=v_{S(n)}=v_{i}$.

The final assertion is the case where all summands are $0_{V}$: taking $i=1$ gives $\sum_{k=1}^{n}v_{k}=v_{1}=0_{V}$.