---

Step * 1 of Lemma det-times

.....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)
BY
{ ((MemTypeCD THENW Auto) THEN Reduce 0 THEN Auto) }

1
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. B : Matrix(n;n;r)
5. i : ℕn
6. k : |r|
7. M : Matrix(n;n;r)
⊢ |(matrix-mul-row(r;k;i;M)*B)| = (k * |(M*B)|) ∈ |r|

2
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. B : Matrix(n;n;r)
5. ∀i:ℕn. ∀k:|r|. ∀M:Matrix(n;n;r).  (|(matrix-mul-row(r;k;i;M)*B)| = (k * |(M*B)|) ∈ |r|)
6. i : ℕn
7. row : ℕn ⟶ |r|
8. M : Matrix(n;n;r)
⊢ |(matrix(if x=i then (row y) +r M[x,y] else M[x,y])*B)|
= (|(matrix(if x=i then row y else M[x,y])*B)| +r |(M*B)|)
∈ |r|

3
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. B : Matrix(n;n;r)
5. ∀i:ℕn. ∀k:|r|. ∀M:Matrix(n;n;r).  (|(matrix-mul-row(r;k;i;M)*B)| = (k * |(M*B)|) ∈ |r|)
6. ∀i:ℕn. ∀row:ℕn ⟶ |r|. ∀M:Matrix(n;n;r).
     (|(matrix(if x=i then (row y) +r M[x,y] else M[x,y])*B)|
     = (|(matrix(if x=i then row y else M[x,y])*B)| +r |(M*B)|)
     ∈ |r|)
7. i : ℕn
8. j : ℕn
9. ¬(i = j ∈ ℤ)
10. M : Matrix(n;n;r)
⊢ |(matrix-swap-rows(M;i;j)*B)| = (-r |(M*B)|) ∈ |r|

4
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. B : Matrix(n;n;r)
5. ∀i:ℕn. ∀k:|r|. ∀M:Matrix(n;n;r).  (|(matrix-mul-row(r;k;i;M)*B)| = (k * |(M*B)|) ∈ |r|)
6. ∀i:ℕn. ∀row:ℕn ⟶ |r|. ∀M:Matrix(n;n;r).
     (|(matrix(if x=i then (row y) +r M[x,y] else M[x,y])*B)|
     = (|(matrix(if x=i then row y else M[x,y])*B)| +r |(M*B)|)
     ∈ |r|)
7. ∀i,j:ℕn.  ((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n;n;r). (|(matrix-swap-rows(M;i;j)*B)| = (-r |(M*B)|) ∈ |r|)))
8. i : ℕn
9. j : ℕn
10. ¬(i = j ∈ ℤ)
11. M : Matrix(n;n;r)
12. matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)
⊢ |(M*B)| = 0 ∈ |r|

---

Latex:

---

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


By

---

Latex:
((MemTypeCD  THENW  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index