\(n \times n\)リアル（実）マトリックス（行列）に対して、もしも、各\(n\)列または行ベクトルに対して、マトリックス（行列）にベクトルおよびベクトルのトランスポーズ（転置）を掛けたものがベクトルにベクトルのトランスポーズ（転置）を掛けたものである場合、そしてその場合に限って、マトリックス（行列）は、対角コンポーネントたち\(1\)および非対角コンポーネントたちアンチシンメトリック（反対称）を持つことの記述/証明
話題
About: マトリックス（行列）たちスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、%リング（環）名%マトリックス（行列）たちスペース（空間）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意の\(n \times n\)リアル（実）マトリックス（行列）に対して、もしも、各\(n\)列または行ベクトルに対して、当該マトリックス（行列）に当該ベクトルおよび当該ベクトルのトランスポーズ（転置）を掛けたものが当該ベクトルに当該ベクトルのトランスポーズ（転置）を掛けたものである場合、そしてその場合に限って、当該マトリックス（行列）は、対角コンポーネントたち\(1\)および非対角コンポーネントたちアンチシンメトリック（反対称）を持つという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(\{M\}\): \(= \text{ 当該 } \mathbb{R} \text{ マトリックス（行列）たちスペース（空間） }\)
\(n\): \(\in \mathbb{N} \setminus \{0\}\)
\(M\): \(\in \{M\} \cap \{\text{ 全ての } n \times n \text{ マトリックス（行列）たち }\}\)
//
ステートメント（言明）たち:
(
\(\forall v \in \{M\} \cap \{\text{ 全ての } n \times 1 \text{ マトリックス（行列）たち }\} (v^t M v = v^t v)\)
\(\iff\)
\(\forall j \in \{1, ..., n\} (M^j_j = 1) \land \forall j, l \in \{1, ..., n\} \text{ で、以下を満たすもの、つまり、 } j \neq l (M^j_l = - M^l_j)\)
)
\(\land\)
(
\(\forall v \in \{M\} \cap \{\text{ 全ての } 1 \times n \text{ マトリックス（行列）たち }\} (v M v^t = v v^t)\)
\(\iff\)
\(\forall j \in \{1, ..., n\} (M^j_j = 1) \land \forall j, l \in \{1, ..., n\} \text{ で、以下を満たすもの、つまり、 } j \neq l (M^j_l = - M^l_j)\)
)
//
2: 注
"\(M = I\)"は含意されない、例えば、\(M = \begin{pmatrix} 1 & 1 \\ - 1 & 1 \end{pmatrix}\)としよう、すると、\(v^t M v = \begin{pmatrix} v^1 & v^2 \end{pmatrix} \begin{pmatrix} 1 & 1 \\ - 1 & 1 \end{pmatrix} \begin{pmatrix} v^1 \\ v^2 \end{pmatrix} = \begin{pmatrix} v^1 & v^2 \end{pmatrix} \begin{pmatrix} v^1 + v^2 \\ - v^1 + v^2 \end{pmatrix} = v^1 (v^1 + v^2) + v^2 (- v^1 + v^2) = {v^1}^2 + {v^2}^2 = \begin{pmatrix} v^1 & v^2 \end{pmatrix} \begin{pmatrix} v^1 \\ v^2 \end{pmatrix} = v^t v\)。
任意の\(n \times n\)コンプレックス（複素）マトリックス（行列）に対して、もしも、各\(n\)列または行ベクトルに対して、当該マトリックス（行列）に当該ベクトルおよび当該ベクトルのエルミートコンジュゲート（共役）を掛けたものが当該ベクトルに当該ベクトルのエルミートコンジュゲート（共役）を掛けたものである場合、そしてその場合に限って、当該マトリックス（行列）はアイデンティティ（単位行列）であるという命題と比較のこと。
3: Proof
Whole Strategy: Step 1: suppose that \(v^t M v = v^t v\); Step 2: see that \(M\) is with the diagonals \(1\) and the non-diagonals antisymmetric; Step 3: suppose that \(M\) is with the diagonals \(1\) and the non-diagonals antisymmetric; Step 4: see that \(v^* M v = v^* v\); Step 5: suppose that \(v M v^* = v v^*\); Step 6: see that \(M\) is with the diagonals \(1\) and the non-diagonals antisymmetric; Step 7: suppose that \(M\) is with the diagonals \(1\) and the non-diagonals antisymmetric; Step 8: see that \(v M v^* = v v^*\).
Step 1:
Let us suppose that \(\forall v \in \{M\} \cap \{\text{ the } n \times 1 \text{ matrices } \} (v^* M v = v^* v)\).
Step 2:
Let \(j \in \{1, ..., n\}\) be any.
Let \(v\) be such that \(v^j = 1\) and for each \(m \neq j\), \(v^m = 0\).
Then, \(v^* M v = v^*_m (M v)^m = v^*_m M^m_p v^p = v^*_j M^j_j v^j = 1 M^j_j 1 = M^j_j\).
On the other hand, \(v^* v = v^*_m v^m = v^*_j v^j = 1 1 = 1\).
So, \(M^j_j = 1\).
Let \(j, l \in \{1, ..., n\}\) be any such that \(j \neq l\)
Let \(v\) be such that \(v^j = 1\) and \(v^l = 1\) and for each \(m \neq j, l\), \(v^m = 0\).
Then, \(v^* M v = v^*_m (M v)^m = v^*_m M^m_p v^p = v^*_m (M^m_j v^j + M^m_l v^l) = v^*_j (M^j_j v^j + M^j_l v^l) + v^*_l (M^l_j v^j + M^l_l v^l) = 1 (M^j_j 1 + M^j_l 1) + 1 (M^l_j 1 + M^l_l 1) = M^j_j + M^j_l + M^l_j + M^l_l = 1 + M^j_l + M^l_j + 1\).
On the other hand, \(v^* v = v^*_m v^m = v^*_j v^j + v^*_l v^l = 1 1 + 1 1 = 1 + 1\).
So, \(M^j_l + M^l_j = 0\).
Step 3:
Let us suppose that \(M\) is with the diagonals \(1\) and the non-diagonals antisymmetric.
Step 4:
Let \(v \in \{M\} \cap \{\text{ the } n \times 1 \text{ matrices } \}\) be any.
\(v^t M v = {v^t}_m M^m_p v^p = \sum_{m \in \{1, ..., n\}} v^m M^m_p v^p = \sum_{m \in \{1, ..., n\}} v^m (M^m_m v^m + \sum_{p \in \{1, ..., n\} \setminus \{m\}} M^m_p v^p) = \sum_{m \in \{1, ..., n\}} v^m (1 v^m + \sum_{p \in \{1, ..., n\} \setminus \{m\}} M^m_p v^p) = \sum_{m \in \{1, ..., n\}} v^m (v^m + \sum_{p \in \{1, ..., n\} \setminus \{m\}} M^m_p v^p) = \sum_{m \in \{1, ..., n\}} v^m v^m + \sum_{m \in \{1, ..., n\}} v^m \sum_{p \in \{1, ..., n\} \setminus \{m\}} M^m_p v^p = \sum_{m \in \{1, ..., n\}} v^m v^m + \sum_{m \in \{1, ..., n\}} \sum_{p \in \{1, ..., n\} \setminus \{m\}} v^m M^m_p v^p\).
As for \(\sum_{m \in \{1, ..., n\}} \sum_{p \in \{1, ..., n\} \setminus \{m\}} v^m M^m_p v^p\), as \(\sum_{m \in \{1, ..., n\}} \sum_{p \in \{1, ..., n\} \setminus \{m\}} = \sum_{(m, p) \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m \neq p}\), \(= \sum_{(m, p) \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m \neq p} v^m M^m_p v^p = 1 / 2 (\sum_{(m, p) \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m \neq p} v^m M^m_p v^p + \sum_{(m', p') \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m' \neq p'} v^{m'} M^{m'}_{p'} v^{p'}) = 1 / 2 (\sum_{(m, p) \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m \neq p} v^m M^m_p v^p - \sum_{(m', p') \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m' \neq p'} v^{m'} M^{p'}_{m'} v^{p'}) = 1 / 2 (\sum_{(m, p) \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m \neq p} v^m M^m_p v^p - \sum_{(p', m') \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } p' \neq m'} v^{p'} M^{p'}_{m'} v^{m'}) = 0\)
So, \(v^t M v = \sum_{m \in \{1, ..., n\}} v^m v^m = v^t v\).
Step 5:
Let us suppose that \(\forall v \in \{M\} \cap \{\text{ the } 1 \times n \text{ matrices }\} (v M v^t = v v^t)\).
Step 6:
Let \(j \in \{1, ..., n\}\) be any.
Let \(v\) be such that \(v_j = 1\) and for each \(m \neq j\), \(v_m = 0\).
Then, \(v M v^t = v_m (M v^t)^m = v_m M^m_p {v^t}^p = v_j M^j_j {v^t}^j = 1 M^j_j 1 = M^j_j\).
On the other hand, \(v v^t = v_m {v^t}^m = v_j {v^t}^j = 1 1 = 1\).
So, \(M^j_j = 1\).
Let \(j, l \in \{1, ..., n\}\) be any such that \(j \neq l\)
Let \(v\) be such that \(v_j = 1\) and \(v_l = 1\) and for each \(m \neq j, l\), \(v_m = 0\).
Then, \(v M v^t = v_m (M {v^t})^m = v_m M^m_p {v^t}^p = v_m (M^m_j {v^t}^j + M^m_l {v^t}^l) = v_j (M^j_j {v^t}^j + M^j_l {v^t}^l) + v_l (M^l_j {v^t}^j + M^l_l {v^t}^l) = 1 (M^j_j 1 + M^j_l 1) + 1 (M^l_j 1 + M^l_l 1) = M^j_j + M^j_l + M^l_j + M^l_l = 1 + M^j_l + M^l_j + 1\).
On the other hand, \(v v^t = v_m {v^t}^m = v_j {v^t}^j + v_l {v^t}^l = 1 1 + 1 1 = 1 + 1\).
So, \(M^j_l + M^l_j = 0\).
Step 7:
Let us suppose that \(M\) is with the diagonals \(1\) and the non-diagonals antisymmetric.
Step 8:
Let \(v \in \{M\} \cap \{\text{ the } 1 \times n \text{ matrices } \}\) be any.
\(v M v^t = v_m M^m_p {v^t}^p = v_m \sum_{p \in \{1, ..., n\}} M^m_p v_p = \sum_{m \in \{1, ..., n\}} v_m (M^m_m v_m + \sum_{p \in \{1, ..., n\} \setminus \{m\}} M^m_p v_p) = \sum_{m \in \{1, ..., n\}} v_m (1 v_m + \sum_{p \in \{1, ..., n\} \setminus \{m\}} M^m_p v_p) = \sum_{m \in \{1, ..., n\}} v_m v_m + \sum_{m \in \{1, ..., n\}} v_m \sum_{p \in \{1, ..., n\} \setminus \{m\}} M^m_p v_p = \sum_{m \in \{1, ..., n\}} v_m v_m + \sum_{m \in \{1, ..., n\}} \sum_{p \in \{1, ..., n\} \setminus \{m\}} v_m M^m_p v_p\).
As for \(\sum_{m \in \{1, ..., n\}} \sum_{p \in \{1, ..., n\} \setminus \{m\}} v_m M^m_p v_p\), as \(\sum_{m \in \{1, ..., n\}} \sum_{p \in \{1, ..., n\} \setminus \{m\}} = \sum_{(m, p) \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m \neq p}\), \(= \sum_{(m, p) \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m \neq p} v_m M^m_p v_p = 1 / 2 (\sum_{(m, p) \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m \neq p} v_m M^m_p v_p + \sum_{(m', p') \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m' \neq p'} v_{m'} M^{m'}_{p'} v_{p'}) = 1 / 2 (\sum_{(m, p) \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m \neq p} v_m M^m_p v_p - \sum_{(m', p') \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m' \neq p'} v_{m'} M^{p'}_{m'} v_{p'}) = 1 / 2 (\sum_{(m, p) \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } m \neq p} v_m M^m_p v_p - \sum_{(p', m') \in \{1, ..., n\} \times \{1, ..., n\} \text{ such that } p' \neq m'} v_{p'} M^{p'}_{m'} v_{m'}) = 0\).
So, \(v M v^t = \sum_{m \in \{1, ..., n\}} v_m v_m = v v^t\).
