---

Step * of Lemma det-times

∀[r:CRng]. ∀[n:ℕ]. ∀[A,B:Matrix(n;n;r)].  (|(A*B)| = (|A| * |B|) ∈ |r|)
BY
{ (Auto THEN Assert ⌜λA.|(A*B)| ∈ det-fun(r;n)⌝⋅) }

1
.....assertion..... 
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. B : Matrix(n;n;r)
⊢ λA.|(A*B)| ∈ det-fun(r;n)

2
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)
⊢ |(A*B)| = (|A| * |B|) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[A,B:Matrix(n;n;r)].    (|(A*B)|  =  (|A|  *  |B|))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mlambda{}A.|(A*B)|  \mmember{}  det-fun(r;n)\mkleeneclose{}\mcdot{})

---

Home Index