Proof of Nonnegativity and Monotonicity of a Sum over a Finite Index Set

Each result cited is universally quantified over the data in its own statement, and is applied here to the data named.

Claim 1 (An enumeration of $G$). Since $G$ is nonempty and finite, Finite Set gives a natural number $p$ such that $G$ has $p$ elements, and that definition then supplies a bijection $\varphi:[p]\to G$, where $[p]$ is the initial segment determined by $p$. By Sum over a Finite Index Set, for every map $u:G\to\mathbb{R}$,

Claim 2 (Clause 1). Suppose $h(x)\le h'(x)$ for every $x\in G$. Then $h(\varphi(k))\le h'(\varphi(k))$ for every $k\in[p]$, because $\varphi(k)\in G$. By claim 1 of Comparison and Absolute Value Bounds for Finite Sums of Real Numbers,

and claim 1 identifies the two sides with $\sum_{x\in G}h(x)$ and $\sum_{x\in G}h'(x)$.

Claim 3 (Clause 2). Suppose $0\le h(x)$ for every $x\in G$. Each summand satisfies $0\le h(\varphi(k))$, because $\varphi(k)\in G$. Hence $0\le\sum_{k=1}^{p}h(\varphi(k))$ by claim 5 of Properties of Finite Sums, and claim 1 identifies that sum with $\sum_{x\in G}h(x)$.

Claim 4 (Clause 3). Suppose $0\le h(x)$ for every $x\in G$, and let $E\subseteq G$ be nonempty.

Suppose first $E=G$. Then the two sums are the same real number, and $t\le t$ for every real $t$ because the order of $\mathbb{R}$ is a total order, hence reflexive.

Suppose now $E\ne G$, and put $E'=G\setminus E$, which is nonempty because $E\subseteq G$ and $E\ne G$. Both $E$ and $E'$ are finite by claim 3 of Basic Properties of Finite Sets, applied to the finite set $G$ and to each of them. They are disjoint and their union is $G$, so claim 3 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set, applied to $G$, to $E$, to $E'$ and to $h$, gives

The restriction of $h$ to $E'$ is nonnegative at every point of $E'$, so clause 2, proved in claim 3 and applied to the nonempty finite set $E'$ and to that restriction, gives $0\le\sum_{x\in E'}h(x)$. Since

claim 3 of Elementary Arithmetic in an Ordered Field yields $\sum_{x\in E}h(x)\le\sum_{x\in G}h(x)$.