Step
*
1
2
1
1
2
2
1
1
1
of Lemma
det-kI+J
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|
BY
{ (Assert ⌜|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=n - 1 then 1 else if x=y then a else 0)|
∈ |r|⌝⋅
THENM (NthHypEqTrans (-1) THEN Thin (-1))
) }
1
.....assertion.....
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=n - 1 then 1 else if x=y then a else 0)|
∈ |r|
2
1. r : CRng
2. n : ℤ
3. 0 < n
4. a : |r|
5. ¬(n = 1 ∈ ℤ)
⊢ |matrix(if x=n - 1 then 1 else if x=y then a else 0)| = |matrix(if x=y then if x=n - 1 then 1 else a else 0)| ∈ |r|
Latex:
Latex:
1. r : CRng
2. n : \mBbbZ{}
3. 0 < n
4. a : |r|
5. \mneg{}(n = 1)
\mvdash{} |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)|
By
Latex:
(Assert \mkleeneopen{}|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=n - 1 then 1 else if x=y then a else 0)|\mkleeneclose{}\mcdot{}
THENM (NthHypEqTrans (-1) THEN Thin (-1))
)
Home
Index