Step
*
of Lemma
det-fun+
∀[n:ℕ]. ∀[J:ℕn + 1]. ∀[r:Rng]. ∀[d:det-fun(r;n + 1)]. (λM.(d matrix+(r;J;M)) ∈ det-fun(r;n))
BY
{ (Intros THEN Unhide THEN D -1 THEN (MemTypeCD THENW Auto) THEN Reduce 0 THEN Auto) }
1
1. n : ℕ
2. J : ℕn + 1
3. r : Rng
4. d : Matrix(n + 1;n + 1;r) ⟶ |r|
5. ∀i:ℕn + 1. ∀k:|r|. ∀M:Matrix(n + 1;n + 1;r). ((d matrix-mul-row(r;k;i;M)) = (k * (d M)) ∈ |r|)
6. ∀i:ℕn + 1. ∀row:ℕn + 1 ⟶ |r|. ∀M:Matrix(n + 1;n + 1;r).
((d matrix(if x=i then (row y) +r M[x,y] else M[x,y]))
= ((d matrix(if x=i then row y else M[x,y])) +r (d M))
∈ |r|)
7. ∀i,j:ℕn + 1. ((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n + 1;n + 1;r). ((d matrix-swap-rows(M;i;j)) = (-r (d M)) ∈ |r|)))
8. ∀i,j:ℕn + 1.
((¬(i = j ∈ ℤ))
⇒ (∀M:Matrix(n + 1;n + 1;r). ((matrix-swap-rows(M;i;j) = M ∈ Matrix(n + 1;n + 1;r)) ⇒ ((d M) = 0 ∈ |r|))))
9. i : ℕn
10. k : |r|
11. M : Matrix(n;n;r)
⊢ (d matrix+(r;J;matrix-mul-row(r;k;i;M))) = (k * (d matrix+(r;J;M))) ∈ |r|
2
1. n : ℕ
2. J : ℕn + 1
3. r : Rng
4. d : Matrix(n + 1;n + 1;r) ⟶ |r|
5. ∀i:ℕn + 1. ∀k:|r|. ∀M:Matrix(n + 1;n + 1;r). ((d matrix-mul-row(r;k;i;M)) = (k * (d M)) ∈ |r|)
6. ∀i:ℕn + 1. ∀row:ℕn + 1 ⟶ |r|. ∀M:Matrix(n + 1;n + 1;r).
((d matrix(if x=i then (row y) +r M[x,y] else M[x,y]))
= ((d matrix(if x=i then row y else M[x,y])) +r (d M))
∈ |r|)
7. ∀i,j:ℕn + 1. ((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n + 1;n + 1;r). ((d matrix-swap-rows(M;i;j)) = (-r (d M)) ∈ |r|)))
8. ∀i,j:ℕn + 1.
((¬(i = j ∈ ℤ))
⇒ (∀M:Matrix(n + 1;n + 1;r). ((matrix-swap-rows(M;i;j) = M ∈ Matrix(n + 1;n + 1;r)) ⇒ ((d M) = 0 ∈ |r|))))
9. ∀i:ℕn. ∀k:|r|. ∀M:Matrix(n;n;r). ((d matrix+(r;J;matrix-mul-row(r;k;i;M))) = (k * (d matrix+(r;J;M))) ∈ |r|)
10. i : ℕn
11. row : ℕn ⟶ |r|
12. M : Matrix(n;n;r)
⊢ (d matrix+(r;J;matrix(if x=i then (row y) +r M[x,y] else M[x,y])))
= ((d matrix+(r;J;matrix(if x=i then row y else M[x,y]))) +r (d matrix+(r;J;M)))
∈ |r|
3
1. n : ℕ
2. J : ℕn + 1
3. r : Rng
4. d : Matrix(n + 1;n + 1;r) ⟶ |r|
5. ∀i:ℕn + 1. ∀k:|r|. ∀M:Matrix(n + 1;n + 1;r). ((d matrix-mul-row(r;k;i;M)) = (k * (d M)) ∈ |r|)
6. ∀i:ℕn + 1. ∀row:ℕn + 1 ⟶ |r|. ∀M:Matrix(n + 1;n + 1;r).
((d matrix(if x=i then (row y) +r M[x,y] else M[x,y]))
= ((d matrix(if x=i then row y else M[x,y])) +r (d M))
∈ |r|)
7. ∀i,j:ℕn + 1. ((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n + 1;n + 1;r). ((d matrix-swap-rows(M;i;j)) = (-r (d M)) ∈ |r|)))
8. ∀i,j:ℕn + 1.
((¬(i = j ∈ ℤ))
⇒ (∀M:Matrix(n + 1;n + 1;r). ((matrix-swap-rows(M;i;j) = M ∈ Matrix(n + 1;n + 1;r)) ⇒ ((d M) = 0 ∈ |r|))))
9. ∀i:ℕn. ∀k:|r|. ∀M:Matrix(n;n;r). ((d matrix+(r;J;matrix-mul-row(r;k;i;M))) = (k * (d matrix+(r;J;M))) ∈ |r|)
10. ∀i:ℕn. ∀row:ℕn ⟶ |r|. ∀M:Matrix(n;n;r).
((d matrix+(r;J;matrix(if x=i then (row y) +r M[x,y] else M[x,y])))
= ((d matrix+(r;J;matrix(if x=i then row y else M[x,y]))) +r (d matrix+(r;J;M)))
∈ |r|)
11. i : ℕn
12. j : ℕn
13. ¬(i = j ∈ ℤ)
14. M : Matrix(n;n;r)
⊢ (d matrix+(r;J;matrix-swap-rows(M;i;j))) = (-r (d matrix+(r;J;M))) ∈ |r|
4
1. n : ℕ
2. J : ℕn + 1
3. r : Rng
4. d : Matrix(n + 1;n + 1;r) ⟶ |r|
5. ∀i:ℕn + 1. ∀k:|r|. ∀M:Matrix(n + 1;n + 1;r). ((d matrix-mul-row(r;k;i;M)) = (k * (d M)) ∈ |r|)
6. ∀i:ℕn + 1. ∀row:ℕn + 1 ⟶ |r|. ∀M:Matrix(n + 1;n + 1;r).
((d matrix(if x=i then (row y) +r M[x,y] else M[x,y]))
= ((d matrix(if x=i then row y else M[x,y])) +r (d M))
∈ |r|)
7. ∀i,j:ℕn + 1. ((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n + 1;n + 1;r). ((d matrix-swap-rows(M;i;j)) = (-r (d M)) ∈ |r|)))
8. ∀i,j:ℕn + 1.
((¬(i = j ∈ ℤ))
⇒ (∀M:Matrix(n + 1;n + 1;r). ((matrix-swap-rows(M;i;j) = M ∈ Matrix(n + 1;n + 1;r)) ⇒ ((d M) = 0 ∈ |r|))))
9. ∀i:ℕn. ∀k:|r|. ∀M:Matrix(n;n;r). ((d matrix+(r;J;matrix-mul-row(r;k;i;M))) = (k * (d matrix+(r;J;M))) ∈ |r|)
10. ∀i:ℕn. ∀row:ℕn ⟶ |r|. ∀M:Matrix(n;n;r).
((d matrix+(r;J;matrix(if x=i then (row y) +r M[x,y] else M[x,y])))
= ((d matrix+(r;J;matrix(if x=i then row y else M[x,y]))) +r (d matrix+(r;J;M)))
∈ |r|)
11. ∀i,j:ℕn.
((¬(i = j ∈ ℤ)) ⇒ (∀M:Matrix(n;n;r). ((d matrix+(r;J;matrix-swap-rows(M;i;j))) = (-r (d matrix+(r;J;M))) ∈ |r|)))
12. i : ℕn
13. j : ℕn
14. ¬(i = j ∈ ℤ)
15. M : Matrix(n;n;r)
16. matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)
⊢ (d matrix+(r;J;M)) = 0 ∈ |r|
Latex:
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[J:\mBbbN{}n + 1]. \mforall{}[r:Rng]. \mforall{}[d:det-fun(r;n + 1)]. (\mlambda{}M.(d matrix+(r;J;M)) \mmember{} det-fun(r;n))
By
Latex:
(Intros THEN Unhide THEN D -1 THEN (MemTypeCD THENW Auto) THEN Reduce 0 THEN Auto)
Home
Index