Let $A$ be a commutative monoid ordered by $\leq$, that is: $$x\leq y \Rightarrow x + z \leq y +z$$ such that suprema $\bigvee$ of families index by a set $I$ exists and such that:
$$\bigvee_{i\in I} (x_i + y) = \bigvee_{i\in I} x_i + y $$ (this seems useful / necessary according to Wikipedia)
Let: $$\sum_{i\in I} x_i := \bigvee_{\tilde{I} \in K_I} \sum_{i\in \tilde{I}} x_i$$ where $K_I = \{\tilde{I}\subseteq I : \tilde{I}\text{ is finite} \}$.
How can I show the following "infinite associativity / commutativity property":
If $(I_j)_{j\in J}$ is a partition of $I$ then:
$$\sum_{i\in I} x_i = \sum_{j\in J} \sum_{i\in I_j} x_i$$
This seems to involve switching suprema with finite sums but I can't figure out how it works exactly.
Also (not the actual question): does anyone know how this property is actually called?
Here is an outline of a proof.
Step 1: Prove by induction on the number of elements in $\tilde {J}$ that if $\tilde{J}$ is finite, then $$\sum_{j\in \tilde{J}} \left(\bigvee_{u \in U_j} y_u \right) = \bigvee_{(u_j)_{j \in \tilde J} \in (\prod_{j \in \tilde{J}} U_j) } \left(\sum_{j \in J} y_{u_j}\right)$$ Step 2: Using the result from step 1 we have $$\sum_{j\in J} \sum_{i\in I_j} x_i=\bigvee_{\tilde{J} \in K_J} \sum_{j\in \tilde{J}} \left(\bigvee_{\tilde{I_j} \in K_{I_j}} \sum_{i\in \tilde{I_j}} x_i\right)=\bigvee_{\tilde{J} \in K_J} \left(\bigvee_{(\tilde{I_j})_{j\in \tilde J} \in \prod_{j \in \tilde J} K_{I_j}} \sum_{j\in \tilde{J}} \sum_{i\in \tilde{I_j}} x_i\right) = \bigvee_{\tilde{J} \in K_J} \left(\bigvee_{(\tilde{I_j})_{j\in \tilde J} \in \prod_{j \in \tilde J} K_{I_j}} \sum_{i\in \cup_{j\in \tilde J}\tilde{I_j}} x_i\right)$$ Note that in the last step we used commutativity (,associativity, induction) and that $\tilde {I}_{j_1} \cap \tilde {I}_{j_2} = \emptyset$ if $j_1 \neq j_2$.
Step 3: Notice that since $(I_j)_{j\in J}$ is a partition every finite subset $\tilde {I}$ of $I$ is obtained uniquely as $\cup_{j \in \tilde{J}} \tilde{I}_j$ where $\tilde J$ is a finite subset of $J$ and each $\tilde I_j$ is a finite subset of $I_j$.
Step 4: Combine the observations from steps 2 and 3 and use basic properties of joins to prove the desired result.