---

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

∀[n:ℕ]. ∀[J:ℕn + 1]. ∀[r:Rng]. ∀[d:det-fun(r;n + 1)].
  ((d matrix+(r;J;I)) = if isEven(J) then d I else -r (d I) fi  ∈ |r|)
BY
{ (Auto
   THEN (Assert ∀j:ℕ+n + 1. (matrix-swap-rows(matrix+(r;j;I);0;j) = matrix+(r;j - 1;I) ∈ Matrix(n + 1;n + 1;r)) BY
               (Auto
                THEN RepUR ``matrix-swap-rows matrix+ identity-matrix`` 0
                THEN EqCDA
                THEN CaseNat 0 `x'
                THEN Reduce 0
                THEN RepeatFor 3 (AutoSplit)))
   ) }

1
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))
⊢ (d matrix+(r;J;I)) = if isEven(J) then d I else -r (d I) fi  ∈ |r|

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[J:\mBbbN{}n  +  1].  \mforall{}[r:Rng].  \mforall{}[d:det-fun(r;n  +  1)].
    ((d  matrix+(r;J;I))  =  if  isEven(J)  then  d  I  else  -r  (d  I)  fi  )


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}j:\mBbbN{}\msupplus{}n  +  1.  (matrix-swap-rows(matrix+(r;j;I);0;j)  =  matrix+(r;j  -  1;I))  BY
                          (Auto
                            THEN  RepUR  ``matrix-swap-rows  matrix+  identity-matrix``  0
                            THEN  EqCDA
                            THEN  CaseNat  0  `x'
                            THEN  Reduce  0
                            THEN  RepeatFor  3  (AutoSplit)))
  )

---

Home Index