Proof of Finite Sums: Vanishing Terms, Finite Additivity of Measures, and Finite Sums of Series in [0,∞]

Proof of (i). First let $B$ be a finite set; we show $\sum_{x\in B}0=0$. Let $\kappa:M\to M$ be the map with constant value $0$. Then $\kappa(0)=0$, and $\kappa(x+y)=0=0+0=\kappa(x)+\kappa(y)$ for all $x,y\in M$, as $0$ is neutral. By Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vi), applied with $\kappa$ and the map $B\to M$ with constant value $0$, and as $\sum_{x\in B}0$ is an element of $M$ (Sums and Products over a Finite Set and over an Interval (v)), $0=\kappa\bigl(\sum_{x\in B}0\bigr)=\sum_{x\in B}\kappa(0)=\sum_{x\in B}0$.

Now let $A$, $E$ and $f$ be as stated. The sets $E$ and $A\setminus E$ are finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iv), they are disjoint, and their union is $A$. By Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (ii) and Sums and Products over a Finite Set and over an Interval (iii),

$$\sum_{a\in A}f(a)=\sum_{a\in E}f(a)+\sum_{a\in A\setminus E}f(a).$$

The restriction of $f$ to $A\setminus E$ is the map with constant value $0$, so the second sum is $\sum_{a\in A\setminus E}0=0$ by the first paragraph, and $\sum_{a\in A}f(a)=\sum_{a\in E}f(a)+0=\sum_{a\in E}f(a)$, as $0$ is neutral.

Proof of (ii) and (iii). If $f(a)=0$ for every $a\in A$, take $E=\emptyset$ in (i): then $\sum_{a\in A}f(a)=\sum_{a\in\emptyset}f(a)=0$ by Sums and Products over a Finite Set and over an Interval (ii). If $a_{0}\in A$ and $f(a)=0$ for every $a\in A$ with $a\neq a_{0}$, take $E=\{a_{0}\}$ in (i), a subset of $A$ with $A\setminus E=\{a\in A:a\neq a_{0}\}$: then $\sum_{a\in A}f(a)=\sum_{a\in\{a_{0}\}}f(a)=f(a_{0})$ by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (i).

Proof of (iv). Let $U=\bigcup_{j\in J}B_{j}$. If $J=\emptyset$, then $U$ has no element, so $U=\emptyset$, which lies in $\mathcal{F}$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (vi); and $\mu(U)=0$ by Measure, Measure Space, and Probability Measure (i), while $\sum_{j\in J}\mu(B_{j})=0$ by Sums and Products over a Finite Set and over an Interval (ii).

Let $J\neq\emptyset$. Then $n=\#J\in\mathbb{N}$ by The Iterated Operation over a Finite Set Does Not Depend on the Enumeration (i), and there is a bijection $\varphi$ from $[n]$ onto $J$ by The Number of Elements of a Finite Set (i). For $k\in[n]$ let $A_{k}=B_{\varphi(k)}\in\mathcal{F}$. For $k,l\in[n]$ with $k\neq l$, $\varphi(k)\neq\varphi(l)$ as $\varphi$ is injective, so $A_{k}\cap A_{l}=\emptyset$: the family $(A_{k})_{k\in[n]}$ is pairwise disjoint. Its union is $U$: a set lying in $A_{k}$ lies in $B_{\varphi(k)}$, and a set lying in $B_{j}$ with $j\in J$ lies in $A_{k}$ for the $k\in[n]$ with $\varphi(k)=j$, which exists as $\varphi$ is surjective. By Basic Properties of a Measure (i), $U\in\mathcal{F}$ and $\mu(U)=\sum_{k=1}^{n}\mu(B_{\varphi(k)})$, and this is $\sum_{j\in J}\mu(B_{j})$ by Sums and Products over a Finite Set and over an Interval (i), applied to the map $j\mapsto\mu(B_{j})$ from $J$ to $[0,\infty]$.

Proof of (v). For $c\in C$ let $\beta(c)=\sum_{m\in\mathbb{N}}b(c,m)$. If $C=\emptyset$, then $\sum_{c\in C}\beta(c)=0$ and $\sum_{c\in C}b(c,m)=0$ for every $m\in\mathbb{N}$, by Sums and Products over a Finite Set and over an Interval (ii), and $\sum_{m\in\mathbb{N}}0=0$ by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iv); so both sides are $0$.

Let $C\neq\emptyset$, let $n=\#C\in\mathbb{N}$, by The Iterated Operation over a Finite Set Does Not Depend on the Enumeration (i), and let $\varphi$ be a bijection from $[n]$ onto $C$, by The Number of Elements of a Finite Set (i). By Maps Defined by Cases (i), with the predicative condition $k\in[n]$ on the pairs $(m,k)\in\mathbb{N}\times\mathbb{N}$, there is a map $w:\mathbb{N}\times\mathbb{N}\to[0,\infty]$ with $w(m,k)=b(\varphi(k),m)$ if $k\in[n]$ and $w(m,k)=0$ if $k\notin[n]$. If $k\in\mathbb{N}$ and $n<k$, then $k\notin[n]$: by Intervals of Natural Numbers (ii) and Intervals of Natural Numbers (i), $k\in[n]$ would give $k\le n$, which fails by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (vii), the order of $\mathbb{N}_{0}$ being a well-order, hence total, by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (v).

Let $m\in\mathbb{N}$. The sequence $k\mapsto w(m,k)$ has $w(m,k)=0$ for every $k\in\mathbb{N}$ with $n<k$, so by Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (vii) its sum is the partial sum $\sum_{k=1}^{n}w(m,k)$. On $[n]$ this sequence agrees with $k\mapsto b(\varphi(k),m)$, so by Sums and Products over a Finite Set and over an Interval (i), applied to the map $c\mapsto b(c,m)$ on $C$,

$$\sum_{k\in\mathbb{N}}w(m,k)=\sum_{k=1}^{n}b(\varphi(k),m)=\sum_{c\in C}b(c,m).$$

Let $k\in\mathbb{N}$. If $k\in[n]$, the sequence $m\mapsto w(m,k)$ is $m\mapsto b(\varphi(k),m)$, so $\sum_{m\in\mathbb{N}}w(m,k)=\beta(\varphi(k))$. If $k\notin[n]$, every term of $m\mapsto w(m,k)$ is $0$, so $\sum_{m\in\mathbb{N}}w(m,k)=0$ by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iv). Hence the sequence $k\mapsto\sum_{m\in\mathbb{N}}w(m,k)$ vanishes at every $k\in\mathbb{N}$ with $n<k$ and agrees with $k\mapsto\beta(\varphi(k))$ on $[n]$, and by Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (vii) and Sums and Products over a Finite Set and over an Interval (i), applied to $\beta$,

$$\sum_{k\in\mathbb{N}}\sum_{m\in\mathbb{N}}w(m,k)=\sum_{k=1}^{n}\beta(\varphi(k))=\sum_{c\in C}\beta(c).$$

By Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (xii), $\sum_{m\in\mathbb{N}}\sum_{k\in\mathbb{N}}w(m,k)=\sum_{k\in\mathbb{N}}\sum_{m\in\mathbb{N}}w(m,k)$; by the two displays this is $\sum_{m\in\mathbb{N}}\sum_{c\in C}b(c,m)=\sum_{c\in C}\sum_{m\in\mathbb{N}}b(c,m)$.