---

Step * 1 1 1 of Lemma det-fun+-at-identity

.....subterm..... T:t
2:n
1. n : ℕ
2. J : ℕn + 1
3. r : Rng
4. d : det-fun(r;n + 1)
5. ∀j:ℕ+n + 1. (matrix-swap-rows(matrix+(r;j;I);0;j) = matrix+(r;j - 1;I) ∈ Matrix(n + 1;n + 1;r))
6. j : ℤ
7. 0 < n + 1
⊢ matrix+(r;0;I) = I ∈ Matrix(n + 1;n + 1;r)
BY
{ (RepUR ``matrix+ identity-matrix`` 0 THEN EqCDA THEN RepeatFor 3 (AutoSplit)) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  n  :  \mBbbN{}
2.  J  :  \mBbbN{}n  +  1
3.  r  :  Rng
4.  d  :  det-fun(r;n  +  1)
5.  \mforall{}j:\mBbbN{}\msupplus{}n  +  1.  (matrix-swap-rows(matrix+(r;j;I);0;j)  =  matrix+(r;j  -  1;I))
6.  j  :  \mBbbZ{}
7.  0  <  n  +  1
\mvdash{}  matrix+(r;0;I)  =  I


By

---

Latex:
(RepUR  ``matrix+  identity-matrix``  0  THEN  EqCDA  THEN  RepeatFor  3  (AutoSplit))

---

Home Index