\(n \times n\)クォータニオン（4元数）マトリックス（行列）に対して、もしも、各\(n\)列または行要素に対して、マトリックス（行列）に要素および要素のクォータニオン（4元数）コンジュゲート（共役）トランスポーズ（転置）を掛けたものが要素に要素のクォータニオン（4元数）コンジュゲート（共役）トランスポーズ（転置）を掛けたものである場合、そしてその場合に限って、マトリックス（行列）はアイデンティティ（単位行列）であることの記述/証明
話題
About: マトリックス（行列）たちスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、%リング（環）名%マトリックス（行列）たちスペース（空間）の定義を知っている。
- 読者は、クォータニオン（4元数）たちディビジョン（除算持ち）アソシアティブ（結合的）アルジェブラ（多元環）の定義を知っている。
- 読者は、任意のクォータニオン（4元数）に対して、もしも、当該クォータニオン（4元数）に\(i\)を左から右から掛けたものたちの合計、当該クォータニオン（4元数）に\(j\)を左から右から掛けたものたちの合計、当該クォータニオン（4元数）に\(k\)を左から右から掛けたものたちの合計が\(0\)である場合、そしてその場合に限って、当該クォータニオン（4元数）は\(0\)であるという命題を認めている。
ターゲットコンテキスト
- 読者は、任意の\(n \times n\)クォータニオン（4元数）マトリックス（行列）に対して、もしも、各\(n\)列または行要素に対して、当該マトリックス（行列）に当該要素および当該要素のクォータニオン（4元数）コンジュゲート（共役）トランスポーズ（転置）を掛けたものが当該要素に当該要素のクォータニオン（4元数）コンジュゲート（共役）トランスポーズ（転置）を掛けたものである場合、そしてその場合に限って、当該マトリックス（行列）はアイデンティティ（単位行列）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(\{M\}\): \(= \text{ 当該 } \mathbb{H} \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^* M v = v^* v)\)
\(\iff\)
\(M = I\)
)
\(\land\)
(
\(\forall v \in \{M\} \cap \{\text{ 全ての } 1 \times n \text{ マトリックス（行列）たち }\} (v M v^* = v v^*)\)
\(\iff\)
\(M = I\)
)
//
2: Proof
Whole Strategy: Step 1: suppose that \(v^* M v = v^* v\); Step 2: see that \(M = I\); Step 3: suppose that \(M = I\); Step 4: see that \(v^* M v = v^* v\); Step 5: suppose that \(v M v^* = v v^*\); Step 6: see that \(M = I\); Step 7: suppose that \(M = I\); 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\).
Let \(v\) be such that \(v^j = 1\) and \(v^l = i\) 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 i) + (- i) (M^l_j 1 + M^l_l i) = M^j_j + M^j_l i - i M^l_j + (- i) 1 (i) = 1 + M^j_l i - i M^l_j + (- i) i = 1 + M^j_l i - i M^l_j + 1\).
On the other hand, \(v^* v = v^*_m v^m = v^*_j v^j + v^*_l v^l = 1 1 + (- i) i = 1 + 1\).
So, \(M^j_l i - i M^l_j = 0\).
From \(M^j_l + M^l_j = 0\) and \(M^j_l i - i M^l_j = 0\), \(M^j_l i - i (- M^j_l) = 0\), but the left hand side is \(M^j_l i + i M^j_l\), so, \(M^j_l i + i M^j_l = 0\).
Let \(v\) be such that \(v^j = 1\) and \(v^l = j\) 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 j) + (- j) (M^l_j 1 + M^l_l j) = M^j_j + M^j_l j - j M^l_j + (- j) 1 j = 1 + M^j_l j - j M^l_j + (- j) j = 1 + M^j_l j - j M^l_j + 1\).
On the other hand, \(v^* v = v^*_m v^m = v^*_j v^j + v^*_l v^l = 1 1 + (- j) j = 1 + 1\).
So, \(M^j_l j - j M^l_j = 0\).
From \(M^j_l + M^l_j = 0\) and \(M^j_l j - j M^l_j = 0\), \(M^j_l j - j (- M^j_l) = 0\), but the left hand side is \(M^j_l j + j M^j_l\), so, \(M^j_l j + j M^j_l = 0\).
Let \(v\) be such that \(v^j = 1\) and \(v^l = k\) 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 k) + (- k) (M^l_j 1 + M^l_l k) = M^j_j + M^j_l k - k M^l_j + (- k) 1 k = 1 + M^j_l k - k M^l_j + (- k) k = 1 + M^j_l k - k M^l_j + 1\).
On the other hand, \(v^* v = v^*_m v^m = v^*_j v^j + v^*_l v^l = 1 1 + (- k) k = 1 + 1\).
So, \(M^j_l k - k M^l_j = 0\).
From \(M^j_l + M^l_j = 0\) and \(M^j_l k - k M^l_j = 0\), \(M^j_l k - k (- M^j_l) = 0\), but the left hand side is \(M^j_l k + k M^j_l\), so, \(M^j_l k + k M^j_l = 0\).
\(M^j_l = 0\), by the proposition that for any quaternion, if and only if the sum of the quaternion multiplied by \(i\) from left and right, the sum of the quaternion multiplied by \(j\) from left and right, and the sum of the quaternion multiplied by \(k\) from left and right are \(0\), the quaternion is \(0\).
So, \(M = I\).
Step 3:
Let us suppose that \(M = I\).
Step 4:
Let \(v \in \{M\} \cap \{\text{ the } n \times 1 \text{ matrices } \}\) be any.
\(v^* M v = v^* I v = v^*_m I^m_p v^p = v^*_m I^m_m v^m = v^*_m 1 v^m = v^* v\).
Step 5:
Let us suppose that \(\forall v \in \{M\} \cap \{\text{ the } 1 \times n \text{ matrices }\} (v M v^* = v v^*)\).
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^* = 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\).
Let \(v\) be such that \(v_j = 1\) and \(v_l = i\) 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 (- i)) + i (M^l_j 1 + M^l_l (- i)) = M^j_j - M^j_l i + i M^l_j + i M^l_l (- i) = M^j_j - M^j_l i + i M^l_j + i 1 (- i) = 1 - M^j_l i + i M^l_j + i (- i) = 1 - M^j_l i + i M^l_j + 1\).
On the other hand, \(v v^* = v_m {v^*}^m = v_j {v^*}^j + v_l {v^*}^l = 1 1 + i (- i) = 1 + 1\).
So, \(M^j_l i - i M^l_j = 0\).
From \(M^j_l + M^l_j = 0\) and \(M^j_l i - i M^l_j = 0\), \(M^j_l i - i (- M^j_l) = 0\), but the left hand side is \(M^j_l i + i M^j_l\), so, \(M^j_l i + i M^j_l = 0\).
Let \(v\) be such that \(v_j = 1\) and \(v_l = j\) 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 (- j)) + j (M^l_j 1 + M^l_l (- j)) = M^j_j - M^j_l j + j M^l_j + j M^l_l (- j) = M^j_j - M^j_l j + j M^l_j + j 1 (- j) = 1 - M^j_l j + j M^l_j + j (- j) = 1 - M^j_l j + j M^l_j + 1\).
On the other hand, \(v v^* = v_m {v^*}^m = v_j {v^*}^j + v_l {v^*}^l = 1 1 + j (- j) = 1 + 1\).
So, \(M^j_l j - j M^l_j = 0\).
From \(M^j_l + M^l_j = 0\) and \(M^j_l j - j M^l_j = 0\), \(M^j_l j - j (- M^j_l) = 0\), but the left hand side is \(M^j_l j + j M^j_l\), so, \(M^j_l j + j M^j_l = 0\).
Let \(v\) be such that \(v_j = 1\) and \(v_l = k\) 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 (- k)) + k (M^l_j 1 + M^l_l (- k)) = M^j_j - M^j_l k + k M^l_j + k M^l_l (- k) = M^j_j - M^j_l k + k M^l_j + k 1 (- k) = 1 - M^j_l k + k M^l_j + k (- k) = 1 - M^j_l k + k M^l_j + 1\).
On the other hand, \(v v^* = v_m {v^*}^m = v_j {v^*}^j + v_l {v^*}^l = 1 1 + k (- k) = 1 + 1\).
So, \(M^j_l k - k M^l_j = 0\).
From \(M^j_l + M^l_j = 0\) and \(M^j_l k - k M^l_j = 0\), \(M^j_l k - k (- M^j_l) = 0\), but the left hand side is \(M^j_l k + k M^j_l\), so, \(M^j_l k + k M^j_l = 0\).
\(M^j_l = 0\), by the proposition that for any quaternion, if and only if the sum of the quaternion multiplied by \(i\) from left and right, the sum of the quaternion multiplied by \(j\) from left and right, and the sum of the quaternion multiplied by \(k\) from left and right are \(0\), the quaternion is \(0\).
So, \(M = I\).
Step 7:
Let us suppose that \(M = I\).
Step 8:
Let \(v \in \{M\} \cap \{\text{ the } 1 \times n \text{ matrices } \}\) be any.
\(v M v^* = v I v^* = v_m I^m_p {v^*}^p = v_m I^m_m {v^*}^m = v_m 1 {v^*}^m = v v^*\).
