\(n \times n\)リング（環）マトリックス（行列）に対して、もしも、マトリックス（行列）に各列または行を掛けたものが元の列または行である場合、そしてその場合に限って、マトリックス（行列）はアイデンティティ（単位行列）であることの記述/証明
話題
About: リング（環）
この記事の目次
開始コンテキスト
- 読者は、\(n \times n\)リング（環）マトリックス（行列）たちのリング（環）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意の\(n \times n\)リング（環）マトリックス（行列）に対して、もしも、当該マトリックス（行列）に各列または行を掛けたものが元の列または行である場合、そしてその場合に限って、当該マトリックス（行列）はアイデンティティ（単位行列）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(R\): \(\in \{\text{ 全てのリング（環）たち }\}\)
\(M\): \(\in M_n (R)\)
//
ステートメント（言明）たち:
(
\(\forall m \in R^m (M m = m)\)、ここで、\(m\)は列とみなされる
\(\iff\)
\(M = I\)
)
\(\land\)
(
\(\forall m \in R^m (m M = m)\)、ここで、\(m\)は行とみなされる
\(\iff\)
\(M = I\)
)
//
2: Proof
Whole Strategy: Step 1: suppose that \(\forall m \in R^m (M m = m)\); Step 2: see that \(M = I\); Step 3: suppose that \(M = I\); Step 4: see that \(\forall m \in R^m (M m = m)\); Step 5: suppose that \(\forall m \in R^m (m M = m)\); Step 6: see that \(M = I\); Step 7: suppose that \(M = I\); Step 8: see that \(\forall m \in R^m (m M = m)\).
Step 1:
Let us suppose that \(\forall m \in R^m (M m = m)\).
Step 2:
\(M^j_l m^l = m^j\).
Let \(p \in \{1, ..., n\}\) be any.
Let us take \(m\) such that \(m^p = 1\) and \(m^j = 0\) for each \(j \neq p\).
\(M^p_l m^l = m^p = 1\), but the left hand side is \(M^p_p m^p = M^p_p 1 = M^p_p\), so, \(M^p_p = 1\).
For each \(j \neq p\), \(M^j_l m^l = m^j = 0\), but the left hand side is \(M^j_p m^p = M^j_p 1 = M^j_p\), so, \(M^j_p = 0\).
So, each diagonal component of \(M\) is \(1\) and the other components of \(M\) are \(0\).
So, \(M = I\).
Step 3:
Let us suppose that \(M = I\).
Step 4:
For each \(m \in R^m\), \((M m)^j = M^j_l m^l = I^j_l m^l = m^j\).
So, \(M m = m\).
Step 5:
Let us suppose that \(\forall m \in R^m (m M = m)\).
Step 6:
\(m_l M^l_j = m_j\).
Let \(p \in \{1, ..., n\}\) be any.
Let us take \(m\) such that \(m_p = 1\) and \(m_j = 0\) for each \(j \neq p\).
\(m_l M^l_p = m_p = 1\), but the left hand side is \(m_p M^p_p = 1 M^p_p = M^p_p\), so, \(M^p_p = 1\).
For each \(j \neq p\), \(m_l M^l_j = m_j = 0\), but the left hand side is \(m_p M^p_j = 1 M^p_j = M^p_j\), so, \(M^p_j = 0\).
So, each diagonal component of \(M\) is \(1\) and the other components of \(M\) are \(0\).
So, \(M = I\).
Step 7:
Let us suppose that \(M = I\).
Step 8:
For each \(m \in R^m\), \((m M)_j = m_l M^l_j = m_l I^l_j = m_j\).
So, \(m M = m\).
