---

Step * 1 1 of Lemma null-space-unique


1. r : IntegDom{i}
2. n : ℕ
3. M : Matrix(n;n;r)
4. (adj(M)*M) = |M|*I ∈ Matrix(n;n;r)
5. ¬(|M| = 0 ∈ |r|)
6. u : Column(n;r)
7. (M*u) = 0 ∈ Column(n;r)
8. |M|*u = 0 ∈ Column(n;r)
9. x : ℕn
10. x1 : ℕ1
⊢ u[x,x1] = 0 ∈ |r|
BY
{ (ApFunToHypEquands `Z' ⌜Z[x,x1]⌝ ⌜|r|⌝ (-3)⋅ THENA Auto) }

1
1. r : IntegDom{i}
2. n : ℕ
3. M : Matrix(n;n;r)
4. (adj(M)*M) = |M|*I ∈ Matrix(n;n;r)
5. ¬(|M| = 0 ∈ |r|)
6. u : Column(n;r)
7. (M*u) = 0 ∈ Column(n;r)
8. |M|*u = 0 ∈ Column(n;r)
9. x : ℕn
10. x1 : ℕ1
11. |M|*u[x,x1] = 0[x,x1] ∈ |r|
⊢ u[x,x1] = 0 ∈ |r|

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  (adj(M)*M)  =  |M|*I
5.  \mneg{}(|M|  =  0)
6.  u  :  Column(n;r)
7.  (M*u)  =  0
8.  |M|*u  =  0
9.  x  :  \mBbbN{}n
10.  x1  :  \mBbbN{}1
\mvdash{}  u[x,x1]  =  0


By

---

Latex:
(ApFunToHypEquands  `Z'  \mkleeneopen{}Z[x,x1]\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-3)\mcdot{}  THENA  Auto)

---

Home Index