---

Step * 1 2 1 1 2 2 1 1 of Lemma det-kI+J

.....assertion..... 
1. r : CRng
2. n : ℤ
3. 0 < n
4. a : |r|
5. ¬(n = 1 ∈ ℤ)
⊢ |matrix(if x=y then if x=n - 1 then 1 else a else 0)|
= |matrix(if x=n - 1 then 1 else if x=n - 1 then if y=n - 1 then a else 0 else a*I + J[x,y])|
∈ |r|
BY
{ ((InstLemma `det-multiple-row-ops` [⌜r⌝;⌜n⌝;⌜matrix(if x=n - 1
                                                      then 1
                                                      else if x=n - 1 then if y=n - 1 then a else 0 else a*I + J[x,y])⌝;
    ⌜n - 1⌝;⌜-r 1⌝]⋅
    THENA Auto
    )
   THEN NthHypEqTrans (-1)
   THEN Thin (-1)) }

1
1. r : CRng
2. n : ℤ
3. 0 < n
4. a : |r|
5. ¬(n = 1 ∈ ℤ)
⊢ |matrix(if x=n - 1
          then matrix(if x=n - 1 then 1 else if x=n - 1 then if y=n - 1 then a else 0 else a*I + J[x,y])[x,y]
          else (matrix(if x=n - 1 then 1 else if x=n - 1 then if y=n - 1 then a else 0 else a*I + J[x,y])[x,y] 
                +r 
                ((-r 1) 
                 * 
                 matrix(if x=n - 1 then 1 else if x=n - 1 then if y=n - 1 then a else 0 else a*I + J[x,y])[n - 1,y])))|
= |matrix(if x=y then if x=n - 1 then 1 else a else 0)|
∈ |r|

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  CRng
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  a  :  |r|
5.  \mneg{}(n  =  1)
\mvdash{}  |matrix(if  x=y  then  if  x=n  -  1  then  1  else  a  else  0)|
=  |matrix(if  x=n  -  1  then  1  else  if  x=n  -  1  then  if  y=n  -  1  then  a  else  0  else  a*I  +  J[x,y])|


By

---

Latex:
((InstLemma  `det-multiple-row-ops`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}matrix(if  x=n  -  1
                                                                                                        then  1
                                                                                                        else  if  x=n  -  1
                                                                                                                  then  if  y=n  -  1  then  a  else  0
                                                                                                                  else  a*I  +  J[x,y])\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}-r  1\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  NthHypEqTrans  (-1)
  THEN  Thin  (-1))

---

Home Index