---

Step * of Lemma null-space-unique

∀[r:IntegDom{i}]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].
  ∀[u:Column(n;r)]. (((M*u) = 0 ∈ Column(n;r)) ⇒ (u = 0 ∈ Column(n;r))) supposing ¬(|M| = 0 ∈ |r|)
BY
{ (InstLemma `adjugate-property2` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Auto
   THEN ((ApFunToHypEquands `Z' ⌜(adj(M)*Z)⌝ ⌜Column(n;r)⌝ (-1)⋅ THENA Auto)
         THEN (Assert I ∈ Matrix(n;n;r) BY
                     Auto)
         THEN (InstLemma `matrix-times-0-right` [⌜n⌝;⌜n⌝;⌜1⌝]⋅ THENA Auto))
   THEN (RWW "matrix-times-assoc< 4 matrix-scalar-mul-times matrix-times-id-left -1" (-3)⋅ THENA Auto)
   THEN RepeatFor 2 (Thin (-1))) }

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)
⊢ u = 0 ∈ Column(n;r)

---

Latex:

---

Latex:
\mforall{}[r:IntegDom\{i\}].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].
    \mforall{}[u:Column(n;r)].  (((M*u)  =  0)  {}\mRightarrow{}  (u  =  0))  supposing  \mneg{}(|M|  =  0)


By

---

Latex:
(InstLemma  `adjugate-property2`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  ((ApFunToHypEquands  `Z'  \mkleeneopen{}(adj(M)*Z)\mkleeneclose{}  \mkleeneopen{}Column(n;r)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
              THEN  (Assert  I  \mmember{}  Matrix(n;n;r)  BY
                                      Auto)
              THEN  (InstLemma  `matrix-times-0-right`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (RWW  "matrix-times-assoc<  4  matrix-scalar-mul-times  matrix-times-id-left  -1"  (-3)\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (Thin  (-1)))

---

Home Index