---

Step * 2 1 1 of Lemma det-times

.....assertion..... 
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. B : Matrix(n;n;r)
5. λA.|(A*B)| ∈ det-fun(r;n)
6. (λA.|(A*B)|) = (λM.(((λA.|(A*B)|) I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|)
7. |(A*B)| = (|(I*B)| * (determinant(n;r) A)) ∈ |r|
⊢ (|(I*B)| * (determinant(n;r) A)) = (|A| * |B|) ∈ |r|
BY
{ ((Assert (|(I*B)| * (determinant(n;r) A)) = (|B| * |A|) ∈ |r| BY
          (EqCDA THEN Auto))
   THEN NthHypEqTrans (-1)
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  A  :  Matrix(n;n;r)
4.  B  :  Matrix(n;n;r)
5.  \mlambda{}A.|(A*B)|  \mmember{}  det-fun(r;n)
6.  (\mlambda{}A.|(A*B)|)  =  (\mlambda{}M.(((\mlambda{}A.|(A*B)|)  I)  *  (determinant(n;r)  M)))
7.  |(A*B)|  =  (|(I*B)|  *  (determinant(n;r)  A))
\mvdash{}  (|(I*B)|  *  (determinant(n;r)  A))  =  (|A|  *  |B|)


By

---

Latex:
((Assert  (|(I*B)|  *  (determinant(n;r)  A))  =  (|B|  *  |A|)  BY
                (EqCDA  THEN  Auto))
  THEN  NthHypEqTrans  (-1)
  THEN  Auto)

---

Home Index