---

Step * 2 of Lemma invertible-matrix-iff-left


1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. (adj(A)*A) = |A|*I ∈ Matrix(n;n;r)
5. ∃B:Matrix(n;n;r). ((B*A) = I ∈ Matrix(n;n;r))
⊢ |A| | 1 in r
BY
{ (D -1
   THEN (Assert |(B*A)| = |I| ∈ |r| BY
               Auto)
   THEN (RWO "det-times det-id" (-1) THENA Auto)
   THEN D 0 With ⌜|B|⌝ 
   THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  A  :  Matrix(n;n;r)
4.  (adj(A)*A)  =  |A|*I
5.  \mexists{}B:Matrix(n;n;r).  ((B*A)  =  I)
\mvdash{}  |A|  |  1  in  r


By

---

Latex:
(D  -1
  THEN  (Assert  |(B*A)|  =  |I|  BY
                          Auto)
  THEN  (RWO  "det-times  det-id"  (-1)  THENA  Auto)
  THEN  D  0  With  \mkleeneopen{}|B|\mkleeneclose{} 
  THEN  Auto)

---

Home Index