---

Step * 2 1 of Lemma det-times


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|)
⊢ |(A*B)| = (|A| * |B|) ∈ |r|
BY
{ ((ApFunToHypEquands `Z' ⌜Z A⌝ ⌜|r|⌝ (-1)⋅ THENA Auto) THEN Reduce -1 THEN NthHypEqTrans (-1)) }

1
.....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|

---

Latex:

---

Latex:

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)))
\mvdash{}  |(A*B)|  =  (|A|  *  |B|)


By

---

Latex:
((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  A\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)  THEN  Reduce  -1  THEN  NthHypEqTrans  (-1))

---

Home Index