Step
*
1
1
2
2
1
of Lemma
det-equal-rows
.....subterm..... T:t
3:n
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. j : ℕn
6. ¬(i = j ∈ ℤ)
7. matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)
8. Σ{r} x ∈ map(λf.(f o (i, j));filter(λa.(¬b(permutation-sign(n;a) =z 1));
permutations-list(n))). let k = Π(r) 0
≤ i
< n
M[i,x i] in
if permutation-sign(n;x)=1 then k else (-r k)
= Σ{r} x ∈ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)). let k = Π(r) 0
≤ i@0
< n
M[i@0,(λf.(f o (i, j))) x i@0] in
if permutation-sign(n;(λf.(f
o (i, j)))
x)=1
then k
else (-r k)
∈ |r|
9. filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)) ∈ {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} List
10. x : {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)}
⊢ (-r let k = Π(r) 0 ≤ i < n. M[i,x i] in if permutation-sign(n;x)=1 then k else (-r k))
= let k = Π(r) 0
≤ i@0
< n
M[i@0,(λf.(f o (i, j))) x i@0] in
if permutation-sign(n;(λf.(f o (i, j))) x)=1 then k else (-r k)
∈ |r|
BY
{ (((Reduce 0 THEN RWW "permutation-sign-compose sign-flip" 0) THENA Auto)
THEN (GenConclTerm ⌜permutation-sign(n;x)⌝⋅ THENA Auto)
) }
1
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. j : ℕn
6. ¬(i = j ∈ ℤ)
7. matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)
8. Σ{r} x ∈ map(λf.(f o (i, j));filter(λa.(¬b(permutation-sign(n;a) =z 1));
permutations-list(n))). let k = Π(r) 0
≤ i
< n
M[i,x i] in
if permutation-sign(n;x)=1 then k else (-r k)
= Σ{r} x ∈ filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)). let k = Π(r) 0
≤ i@0
< n
M[i@0,(λf.(f o (i, j))) x i@0] in
if permutation-sign(n;(λf.(f
o (i, j)))
x)=1
then k
else (-r k)
∈ |r|
9. filter(λa.(¬b(permutation-sign(n;a) =z 1));permutations-list(n)) ∈ {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} List
10. x : {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)}
11. v : {s:ℤ| |s| = 1 ∈ ℤ}
12. permutation-sign(n;x) = v ∈ {s:ℤ| |s| = 1 ∈ ℤ}
⊢ (-r let k = Π(r) 0 ≤ i < n. M[i,x i] in if v=1 then k else (-r k))
= let k = Π(r) 0
≤ i@0
< n
M[i@0,x ((i, j) i@0)] in
if v * (-1)=1 then k else (-r k)
∈ |r|
Latex:
Latex:
.....subterm..... T:t
3:n
1. r : CRng
2. n : \mBbbN{}
3. M : Matrix(n;n;r)
4. i : \mBbbN{}n
5. j : \mBbbN{}n
6. \mneg{}(i = j)
7. matrix-swap-rows(M;i;j) = M
8. \mSigma{}\{r\} x \mmember{} map(\mlambda{}f.(f o (i, j));filter(\mlambda{}a.(\mneg{}\msubb{}(permutation-sign(n;a) =\msubz{} 1));
permutations-list(n))). let k = \mPi{}(r) 0
\mleq{} i
< n
M[i,x i] in
if permutation-sign(n;x)=1
then k
else (-r k)
= \mSigma{}\{r\} x \mmember{} filter(\mlambda{}a.(\mneg{}\msubb{}(permutation-sign(n;a) =\msubz{} 1));
permutations-list(n)). let k = \mPi{}(r) 0
\mleq{} i@0
< n
M[i@0,(\mlambda{}f.(f o (i, j))) x i@0] in
if permutation-sign(n;(\mlambda{}f.(f o (i, j))) x)=1
then k
else (-r k)
9. filter(\mlambda{}a.(\mneg{}\msubb{}(permutation-sign(n;a) =\msubz{} 1));permutations-list(n)) \mmember{} \{p:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n| Inj(\mBbbN{}n;\mBbbN{}n;p)\} Li\000Cst
10. x : \{p:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n| Inj(\mBbbN{}n;\mBbbN{}n;p)\}
\mvdash{} (-r let k = \mPi{}(r) 0 \mleq{} i < n. M[i,x i] in if permutation-sign(n;x)=1 then k else (-r k))
= let k = \mPi{}(r) 0
\mleq{} i@0
< n
M[i@0,(\mlambda{}f.(f o (i, j))) x i@0] in
if permutation-sign(n;(\mlambda{}f.(f o (i, j))) x)=1 then k else (-r k)
By
Latex:
(((Reduce 0 THEN RWW "permutation-sign-compose sign-flip" 0) THENA Auto)
THEN (GenConclTerm \mkleeneopen{}permutation-sign(n;x)\mkleeneclose{}\mcdot{} THENA Auto)
)
Home
Index