Summation over Finite Index is Well-Defined

From ProofWiki
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 $\family{g }_{i \mathop \in I}$ be an indexed subset of $G$ where the indexing set $I$ is finite.


Then the summation $\ds \sum_{i \mathop \in I} g_i$ is well-defined.


Proof

To show that summation over $I$ is well-defined it needs to be shown:

$(1) \quad \exists$ a finite enumeration of $I$
$(2) \quad \forall$ finite enumerations $e$ and $d$ of $I : \ds \sum_{k \mathop = 1}^n g_{e_k} = \sum_{k \mathop = 1}^n g_{d_k}$


Proof of $(1)$

By definition of finite set:

$\exists n \in \N : \exists$ a bijection $e: \closedint 1 n \to I$

Hence $e$ is a finite enumeration of $I$ by definition.

So the summation $\ds \sum_{k \mathop = 1}^n g_{e_k}$ exists.

$\Box$


Proof of $(2)$

Let $d: \closedint 1 n \to I$ be any other finite enumeration of $I$.


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}_I: I \to I$ denote the identity mapping on $I$.


We have:

\(\ds \sum_{k \mathop = 1}^n g_{e_k}\) \(=\) \(\ds \sum_{k \mathop = 1}^n \map {g \circ e} k\) Definition of Mapping
\(\ds \) \(=\) \(\ds \sum_{k \mathop = 1}^n \map {g \circ e} {\map {e^{-1} \circ d} k}\) Indexed Iterated Operation does not Change under Permutation
\(\ds \) \(=\) \(\ds \sum_{k \mathop = 1}^n \map {\paren{g \circ e} \circ \paren{e^{-1} \circ d} } k\) Definition of Composite Mapping
\(\ds \) \(=\) \(\ds \sum_{k \mathop = 1}^n \map {\paren{ g \circ \paren{\paren {e \circ e^{-1} } \circ d} } } k\) Composition of Mappings is Associative
\(\ds \) \(=\) \(\ds \sum_{k \mathop = 1}^n \map {g \circ \paren{\operatorname{id}_I \mathop \circ d} } k\) Composite of Bijection with Inverse is Identity Mapping
\(\ds \) \(=\) \(\ds \sum_{k \mathop = 1}^n \map {g \circ d} k\) Identity Mapping is Left Identity
\(\ds \) \(=\) \(\ds \sum_{k \mathop = 1}^n g_{d_k}\) Definition of Finite Enumeration

$\Box$


The result follows.

$\blacksquare$

Retrieved from "https://proofwiki.org/w/index.php?title=Summation_over_Finite_Index_is_Well-Defined&oldid=640411"