Proof of Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Counting, Comparison, Monotonicity in the Index Set and the Triangle Inequality

By Commutative Rings §ring, the addition of $R$ is associative and commutative, and $0$ is a neutral element, since $x+0=x$ and $0+x=x+0$; so Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals applies to it. Two rules of $R$ are used. For $c\in R$, $c\cdot0=0$: by Commutative Rings §ring, $c\cdot0=c\cdot(0+0)=c\cdot0+c\cdot0$, and adding $-(c\cdot0)$ to both sides gives $0=c\cdot0$. For $x,y\in R$, $-0=0$ and $-(x+y)=(-x)+(-y)$: indeed $0+0=0$ and $(x+y)+\big((-x)+(-y)\big)=\big(x+(-x)\big)+\big(y+(-y)\big)=0$, and the negative is unique by Negatives, Differences, Reciprocals and Quotients §negative.

Distributive. The map $x\mapsto c\,x$ on $R$ sends $0$ to $0$ and satisfies $c(x+y)=c\,x+c\,y$ by Commutative Rings §ring. Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §homomorphism, with both operations the addition of $R$, gives $c\sum_{x\in A}f(x)=\sum_{x\in A}c\,f(x)$.

Difference. By the rules above, the map $x\mapsto-x$ on $R$ sends $0$ to $0$ and sums to sums, so $\sum_{x\in A}\big(-g(x)\big)=-\sum_{x\in A}g(x)$ by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §homomorphism. As $f(x)-g(x)=f(x)+(-g(x))$, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §termwise gives

$$\sum_{x\in A}\big(f(x)-g(x)\big)=\sum_{x\in A}f(x)+\sum_{x\in A}\big(-g(x)\big)=\sum_{x\in A}f(x)-\sum_{x\in A}g(x).$$

Product of sums. Let $t=\sum_{y\in B}h(y)$. By the distributive clause and commutativity of multiplication, $\Big(\sum_{x\in A}f(x)\Big)t=t\sum_{x\in A}f(x)=\sum_{x\in A}t\,f(x)=\sum_{x\in A}f(x)\,t$, and for each $x\in A$, again by the distributive clause, $f(x)\,t=\sum_{y\in B}f(x)\,h(y)$. Hence, by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §product applied to the map $(x,y)\mapsto f(x)\,h(y)$ on $A\times B$,

$$\Big(\sum_{x\in A}f(x)\Big)\Big(\sum_{y\in B}h(y)\Big)=\sum_{x\in A}\Big(\sum_{y\in B}f(x)\,h(y)\Big)=\sum_{(x,y)\in A\times B}f(x)\,h(y).$$

For the remaining clauses, the ordered field $F$ is by definition a field, and hence a commutative ring by Fields §field, so the above applies in $F$. If $A\neq\emptyset$, let $n=\#A$, which lies in $\mathbb{N}$ by The Iterated Operation over a Finite Set Does Not Depend on the Enumeration §nonempty, and fix a bijection $\varphi$ from $[n]$ onto $A$; by Sums and Products over a Finite Set and over an Interval §operation, $\sum_{x\in A}u(x)=\sum_{k=1}^{n}u(\varphi(k))$ for every $u:A\to F$. If $A=\emptyset$, every sum over $A$ is $0$ by Sums and Products over a Finite Set and over an Interval §empty, and $\#A=0$ by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §empty.

Constant. If $A=\emptyset$, both sides are $0$, since $0\cdot c=0$ by Rules of Arithmetic and Order in an Ordered Field §zero. Otherwise $\sum_{x\in A}c=\sum_{k=1}^{n}c=n\,c$ by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §constant. For $c=1$, $\#A\cdot1=\#A$ by Commutative Rings §ring.

Comparison. If $A=\emptyset$, both sides are $0$. Otherwise apply the first part of Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §comparison to $k\mapsto f(\varphi(k))$ and $k\mapsto g(\varphi(k))$, which satisfy $f(\varphi(k))\le g(\varphi(k))$ for every $k\in[n]$.

Monotone. Let $T\subseteq A$; it is 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 §subset. The comparison clause for $T$, the zero map and $f|_{T}$, together with the constant clause, which gives $\sum_{x\in T}0=\#T\cdot0=0$ by the rule $c\cdot0=0$ proved above, yields $0\le\sum_{x\in T}f(x)$. This applies to $T=S$ and to $T=A\setminus S$. Since $A$ is the union of the disjoint sets $S$ and $A\setminus S$, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §disjoint-union and Rules of Arithmetic and Order in an Ordered Field §order-sum give

$$0\le\sum_{x\in S}f(x)=\sum_{x\in S}f(x)+0\le\sum_{x\in S}f(x)+\sum_{x\in A\setminus S}f(x)=\sum_{x\in A}f(x).$$

Triangle. If $A=\emptyset$, the left side is $|0|=0$ by Rules of Arithmetic and Order in an Ordered Field §absolute-value and the right side is $0$. Otherwise Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §triangle, applied to $k\mapsto f(\varphi(k))$, gives

$$\Big|\sum_{x\in A}f(x)\Big|=\Big|\sum_{k=1}^{n}f(\varphi(k))\Big|\le\sum_{k=1}^{n}|f(\varphi(k))|=\sum_{x\in A}|f(x)|.$$