ファイナイト（有限）セット（集合）たちのファイナイト（有限）インデックス付けされたセット（集合）、インデックス付けされたセット（集合）のディスジョインテッド（互いに素化された）ユニオン（和集合）、コミュータティブ（可換）リング（環）に対して、ディスジョインテッド（互いに素化された）ユニオン（和集合）によるプロダクト（積）は、インデックス付けされたセット（集合）の要素たちによるプロダクト（積）たちの後にインデックスによるプロダクト（積）を取ったものであることの記述/証明
話題
About: リング（環）
この記事の目次
開始コンテキスト
- 読者は、セット（集合）たちのインデックス付けされたセット（集合）のディスジョインテッド（互いに素化された）ユニオン（和集合）の定義を知っている。
- 読者は、リング（環）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意の、ファイナイト（有限）セット（集合）たちのファイナイト（有限）インデックス付けされたセット（集合）、当該インデックス付けされたセット（集合）のディスジョインテッド（互いに素化された）ユニオン（和集合）、任意のコミュータティブ（可換）リング（環）に対して、当該ディスジョインテッド（互いに素化された）ユニオン（和集合）によるプロダクト（積）は、当該インデックス付けされたセット（集合）の要素たちによるプロダクト（積）たちの後に当該インデックスによるプロダクト（積）を取ったものであるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\in \{\text{ 全てのファイナイト（有限）インデックスセット（集合）たち }\}\)
\(\{L_j \in \{\text{ 全てのファイナイト（有限）インデックスセット（集合）たち }\}\}_{j \in J}\): \(\in \{\text{ 全てのインデックス付けされたセット（集合）たち }\}\)
\(R\): \(\in \{\text{ 全てのコミュータティブ（可換）リング（環）たち }\}\)
\(\{r_{j, l_j} \in R\}_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j}\):
//
ステートメント（言明）たち:
\(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j} = \prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\)
//
2: 注
\(R\)はコミュータティブ（可換）である必要がある、なぜなら、そうでなかったら、\(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j}\)または\(\prod_{j \in J} \prod_{l_j \in L_j}\)はウェルデファイント（妥当に定義された）ではないことになる、なぜなら、\(\cup_{j \in J} \{j\} \times L_j\)、\(J\)や\(L_j\)は特に順序付けられていなかった。
\(J\)および各\(L_j\)はファイナイト（有限）である必要がある、なぜなら、そうでなかったら、\(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j}\)や\(\prod_{j \in J} \prod_{l_j \in L_j}\)はウェルデファイント（妥当に定義された）でないことになる、なぜなら、インフィニット（無限）数のファクター（因子）たちのプロダクト（積）は定義されていない。
3: Proof
Whole Strategy: Step 1: see that each of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) and \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) has only \(1\) term with \(r_{j, l_j}\) s as the factors; Step 2: see that each factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) appears as a factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) only once; Step 3: see that each factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) appears as a factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) only once; Step 4: conclude the proposition.
Step 1:
\(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) has only \(1\) term with \(r_{j, l_j}\) s as the factors.
\(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) has only \(1\) term with \(r_{j, l_j}\) s as the factors.
As \(R\) is commutative, the orders of the factors do not matter.
Note that we are going to distinguish the factors by the indexes, \((j, l_j)\) s: when \(r_{j, l_j} = r_{j', l'_{j'}}\), they cannot be distinguished by the values but we distinguish them by the indexes.
So, \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j} = \prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) if and only if each factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) appears as a factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) only once and each factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) appears as a factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) only once.
Step 2:
Let \(r_{j, l_j}\) be any factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\).
\((j, l_j) \in \cup_{j \in J} \{j\} \times L_j\).
\((j, l_j) \in \{j\} \times L_j\) for a \(j \in J\), so, \(l_j \in L_j\).
So, \(r_{j, l_j}\) appears as a factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) only once.
Step 3:
Let \(r_{j, l_j}\) be any factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\).
\(r_{j, l_j}\) is a factor of \(\prod_{l_j \in L_j} r_{j, l_j}\).
So, \(r_{j, l_j}\) appears as a factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) only once.
Step 4:
So, \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j} = \prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\).
