---

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


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 < j
8. j < n + 1
9. (d matrix+(r;j - 1;I)) = if isEven(j - 1) then d I else -r (d I) fi  ∈ |r|
10. (d matrix-swap-rows(matrix+(r;j;I);0;j)) = (-r (d matrix+(r;j;I))) ∈ |r|
⊢ (d matrix+(r;j;I)) = if isEven(j) then d I else -r (d I) fi  ∈ |r|
BY
{ ((RWO "5" (-1) THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜-r Z⌝ ⌜|r|⌝ (-1)⋅ THENA Auto)
   THEN (RW RngNormC (-1) THENA Auto)
   THEN NthHypEqTrans (-1)
   THEN (RWO "-3" 0 THENA Auto)) }

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))
6. j : ℤ
7. 0 < j
8. j < n + 1
9. (d matrix+(r;j - 1;I)) = if isEven(j - 1) then d I else -r (d I) fi  ∈ |r|
10. (d matrix+(r;j - 1;I)) = (-r (d matrix+(r;j;I))) ∈ |r|
11. (-r (d matrix+(r;j - 1;I))) = (d matrix+(r;j;I)) ∈ |r|
⊢ (-r if isEven(j - 1) then d I else -r (d I) fi ) = if isEven(j) then d I else -r (d I) fi  ∈ |r|

---

Latex:

---

Latex:

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  <  j
8.  j  <  n  +  1
9.  (d  matrix+(r;j  -  1;I))  =  if  isEven(j  -  1)  then  d  I  else  -r  (d  I)  fi 
10.  (d  matrix-swap-rows(matrix+(r;j;I);0;j))  =  (-r  (d  matrix+(r;j;I)))
\mvdash{}  (d  matrix+(r;j;I))  =  if  isEven(j)  then  d  I  else  -r  (d  I)  fi 


By

---

Latex:
((RWO  "5"  (-1)  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}-r  Z\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (RW  RngNormC  (-1)  THENA  Auto)
  THEN  NthHypEqTrans  (-1)
  THEN  (RWO  "-3"  0  THENA  Auto))

---

Home Index