Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus

Let $K$ be a field. Sums over a nonempty finite index set are those of Sum over a Finite Index Set. Let $\mathbb{C}$ be the field of complex numbers; for $z\in\mathbb{C}$ let $\overline{z}$ be its complex conjugate and $|z|$ its modulus. Let $A$ be a nonempty finite set.

1. (Finite unions)¶ If $B(a)$ is a finite set for every $a\in A$, then $\bigcup_{a\in A}B(a)$ is finite.

2. (Disjoint unions)¶ If $F$ and $G$ are nonempty finite sets with $F\cap G=\emptyset$ and $f:F\cup G\to K$ is a map, then

3. (Vanishing terms)¶ Let $F$ be a nonempty finite set and $f:F\to K$ a map. If $f(x)=0$ for every $x\in F$, then $\sum_{x\in F}f(x)=0$. If $G\subseteq F$ is nonempty and $f(x)=0$ for every $x\in F\setminus G$, then $\sum_{x\in F}f(x)=\sum_{x\in G}f(x)$.

4. (Dependent pairs)¶ Let $B(a)$ be a nonempty finite set for every $a\in A$, and let $T$ be the set of ordered pairs $(a,b)$ with $a\in A$ and $b\in B(a)$. Then $T$ is nonempty and finite, and for every map $f:T\to K$

5. (Conjugation)¶ For every nonempty finite set $F$ and every map $f:F\to\mathbb{C}$,

6. (Modulus)¶ For every nonempty finite set $F$ and every map $f:F\to\mathbb{C}$, the real number $\bigl|\sum_{x\in F}f(x)\bigr|$ is at most the sum $\sum_{x\in F}|f(x)|$ of the real numbers $|f(x)|$.