---

Step * 1 1 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. c : |r|
6. (c * |A|) = 1 ∈ |r|
⊢ (c*adj(A)*A) = I ∈ Matrix(n;n;r)
BY
{ ((RWW "matrix-scalar-mul-times 4" 0 THENA Auto)
   THEN (InstLemma `matrix-scalar-mul-mul` [⌜n⌝;⌜n⌝]⋅ THENA Auto)
   THEN (InstLemma `matrix-scalar-mul-1` [⌜n⌝;⌜n⌝]⋅ THENA Auto)) }

1
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. (adj(A)*A) = |A|*I ∈ Matrix(n;n;r)
5. c : |r|
6. (c * |A|) = 1 ∈ |r|
7. ∀[r:Rng]. ∀[k1,k2:|r|]. ∀[M:Matrix(n;n;r)].  (k1*k2*M = k1 * k2*M ∈ Matrix(n;n;r))
8. ∀[r:Rng]. ∀[M:Matrix(n;n;r)].  (1*M = M ∈ Matrix(n;n;r))
⊢ c*|A|*I = I ∈ Matrix(n;n;r)

---

Latex:

---

Latex:

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


By

---

Latex:
((RWW  "matrix-scalar-mul-times  4"  0  THENA  Auto)
  THEN  (InstLemma  `matrix-scalar-mul-mul`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `matrix-scalar-mul-1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index