Summation over Finite Subset is Well-Defined
Jump to navigation
Jump to search
This article needs proofreading. Please check it for mathematical errors. If you believe there are none, please remove {{Proofread}} from the code.To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Proofread}} from the code. |
Theorem
Let $\struct{G, +}$ be a commutative monoid.
Let $F \subseteq G$ be a finite subset of $G$.
Then the summation $\ds \sum_{g \mathop \in F} g$ is well-defined.
Proof
To show that summation over $F$ is well-defined it needs to be shown:
- $(1) \quad \exists$ a finite enumeration of $F$
- $(2) \quad \forall$ finite enumerations $e$ and $d$ of $F : \ds \sum_{i \mathop = 1}^n e_i = \sum_{i \mathop = 1}^n d_i$
Proof of $(1)$
By definition of finite set:
- $\exists n \in \N : \exists$ a bijection $e: \closedint 1 n \to F$
Hence $e$ is a finite enumeration of $F$ by definition.
So the summation $\ds \sum_{i \mathop = 1}^n e_i$ exists.
$\Box$
Proof of $(2)$
Let $d: \closedint 1 n \to F$ be any other finite enumeration of $F$.
Consider the composite mapping $e^{-1} \circ d : \closedint 1 n \to \closedint 1 n$ which exists and is a bijection because $e$ and $d$ are bijections.
Let $\operatorname{id}_G: G \to G$ denote the identity mapping on $G$.
We have:
\(\ds \sum_{i \mathop = 1}^n e_i\) | \(=\) | \(\ds \sum_{i \mathop = 1}^n \map e i\) | Definition of Mapping | |||||||||||
\(\ds \) | \(=\) | \(\ds \sum_{i \mathop = 1}^n \map e {\map {e^{-1} \circ d} i}\) | Indexed Iterated Operation does not Change under Permutation | |||||||||||
\(\ds \) | \(=\) | \(\ds \sum_{i \mathop = 1}^n \map {e \circ \paren{e^{-1} \circ d} } i\) | Definition of Composite Mapping | |||||||||||
\(\ds \) | \(=\) | \(\ds \sum_{i \mathop = 1}^n \map {\paren {e \circ e^{-1} } \circ d} i\) | Composition of Mappings is Associative | |||||||||||
\(\ds \) | \(=\) | \(\ds \sum_{i \mathop = 1}^n \map {\operatorname{id}_G \circ d} i\) | Composite of Bijection with Inverse is Identity Mapping | |||||||||||
\(\ds \) | \(=\) | \(\ds \sum_{i \mathop = 1}^n \map d i\) | Identity Mapping is Left Identity | |||||||||||
\(\ds \) | \(=\) | \(\ds \sum_{i \mathop = 1}^n d_i\) | Definition of Finite Enumeration |
$\Box$
The result follows.
$\blacksquare$