:: Laplace Expansion
:: by Karol P\c{a}k and Andrzej Trybulec
::
:: Received August 13, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: LAPLACE:1
theorem Th2: :: LAPLACE:2
theorem Th3: :: LAPLACE:3
theorem Th4: :: LAPLACE:4
theorem Th5: :: LAPLACE:5
theorem Th6: :: LAPLACE:6
theorem Th7: :: LAPLACE:7
theorem Th8: :: LAPLACE:8
theorem Th9: :: LAPLACE:9
theorem Th10: :: LAPLACE:10
for
n,
i,
j being
Nat st
i in Seg (n + 1) &
n >= 2 holds
ex
Proj being
Function of
(2Set (Seg n)),
(2Set (Seg (n + 1))) st
(
rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 1)) } &
Proj is
one-to-one & ( for
k,
m being
Nat st
k < m &
{k,m} in 2Set (Seg n) holds
( (
m < i &
k < i implies
Proj . {k,m} = {k,m} ) & (
m >= i &
k < i implies
Proj . {k,m} = {k,(m + 1)} ) & (
m >= i &
k >= i implies
Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) )
theorem Th11: :: LAPLACE:11
theorem Th12: :: LAPLACE:12
for
X,
Y,
D being non
empty set for
f being
Function of
X,
(Fin Y) for
g being
Function of
(Fin Y),
D for
F being
BinOp of
D st ( for
A,
B being
Element of
Fin Y st
A misses B holds
F . (g . A),
(g . B) = g . (A \/ B) ) &
F is
commutative &
F is
associative &
F is
having_a_unity &
g . {} = the_unity_wrt F holds
for
I being
Element of
Fin X st ( for
x,
y being
set st
x in I &
y in I &
f . x meets f . y holds
x = y ) holds
(
F $$ I,
(g * f) = F $$ (f .: I),
g &
F $$ (f .: I),
g = g . (union (f .: I)) &
union (f .: I) is
Element of
Fin Y )
definition
let i,
j,
n be
Nat;
let K be
Field;
let M be
Matrix of
n,
K;
assume that A1:
i in Seg n
and A2:
j in Seg n
;
func Delete M,
i,
j -> Matrix of
n -' 1,
K equals :
Def1:
:: LAPLACE:def 1
Deleting M,
i,
j;
coherence
Deleting M,i,j is Matrix of n -' 1,K
end;
:: deftheorem Def1 defines Delete LAPLACE:def 1 :
theorem Th13: :: LAPLACE:13
for
n being
Nat for
K being
Field for
M being
Matrix of
n,
K for
i,
j being
Nat st
i in Seg n &
j in Seg n holds
for
k,
m being
Nat st
k in Seg (n -' 1) &
m in Seg (n -' 1) holds
( (
k < i &
m < j implies
(Delete M,i,j) * k,
m = M * k,
m ) & (
k < i &
m >= j implies
(Delete M,i,j) * k,
m = M * k,
(m + 1) ) & (
k >= i &
m < j implies
(Delete M,i,j) * k,
m = M * (k + 1),
m ) & (
k >= i &
m >= j implies
(Delete M,i,j) * k,
m = M * (k + 1),
(m + 1) ) )
theorem Th14: :: LAPLACE:14
theorem Th15: :: LAPLACE:15
definition
let c,
n,
m be
Nat;
let D be non
empty set ;
let M be
Matrix of
n,
m,
D;
let pD be
FinSequence of
D;
func ReplaceCol M,
c,
pD -> Matrix of
n,
m,
D means :
Def2:
:: LAPLACE:def 2
(
len it = len M &
width it = width M & ( for
i,
j being
Nat st
[i,j] in Indices M holds
( (
j <> c implies
it * i,
j = M * i,
j ) & (
j = c implies
it * i,
c = pD . i ) ) ) )
if len pD = len M otherwise it = M;
consistency
for b1 being Matrix of n,m,D holds verum
;
existence
( ( len pD = len M implies ex b1 being Matrix of n,m,D st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies b1 * i,j = M * i,j ) & ( j = c implies b1 * i,c = pD . i ) ) ) ) ) & ( not len pD = len M implies ex b1 being Matrix of n,m,D st b1 = M ) )
uniqueness
for b1, b2 being Matrix of n,m,D holds
( ( len pD = len M & len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies b1 * i,j = M * i,j ) & ( j = c implies b1 * i,c = pD . i ) ) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
( ( j <> c implies b2 * i,j = M * i,j ) & ( j = c implies b2 * i,c = pD . i ) ) ) implies b1 = b2 ) & ( not len pD = len M & b1 = M & b2 = M implies b1 = b2 ) )
end;
:: deftheorem Def2 defines ReplaceCol LAPLACE:def 2 :
for
c,
n,
m being
Nat for
D being non
empty set for
M being
Matrix of
n,
m,
D for
pD being
FinSequence of
D for
b7 being
Matrix of
n,
m,
D holds
( (
len pD = len M implies (
b7 = ReplaceCol M,
c,
pD iff (
len b7 = len M &
width b7 = width M & ( for
i,
j being
Nat st
[i,j] in Indices M holds
( (
j <> c implies
b7 * i,
j = M * i,
j ) & (
j = c implies
b7 * i,
c = pD . i ) ) ) ) ) ) & ( not
len pD = len M implies (
b7 = ReplaceCol M,
c,
pD iff
b7 = M ) ) );
theorem :: LAPLACE:16
for
n,
m,
c being
Nat for
D being non
empty set for
AD being
Matrix of
n,
m,
D for
pD being
FinSequence of
D for
i being
Nat st
i in Seg (width AD) holds
( (
i = c &
len pD = len AD implies
Col (RCol AD,c,pD),
i = pD ) & (
i <> c implies
Col (RCol AD,c,pD),
i = Col AD,
i ) )
theorem :: LAPLACE:17
theorem :: LAPLACE:18
theorem Th19: :: LAPLACE:19
for
n,
m,
c being
Nat for
D being non
empty set for
pD being
FinSequence of
D for
A being
Matrix of
n,
m,
D for
A' being
Matrix of
m,
n,
D st
A' = A @ & (
m = 0 implies
n = 0 ) holds
ReplaceCol A,
c,
pD = (ReplaceLine A',c,pD) @
definition
let i,
n be
Nat;
let perm be
Element of
Permutations (n + 1);
assume A1:
i in Seg (n + 1)
;
func Rem perm,
i -> Element of
Permutations n means :
Def3:
:: LAPLACE:def 3
for
k being
Nat st
k in Seg n holds
( (
k < i implies ( (
perm . k < perm . i implies
it . k = perm . k ) & (
perm . k >= perm . i implies
it . k = (perm . k) - 1 ) ) ) & (
k >= i implies ( (
perm . (k + 1) < perm . i implies
it . k = perm . (k + 1) ) & (
perm . (k + 1) >= perm . i implies
it . k = (perm . (k + 1)) - 1 ) ) ) );
existence
ex b1 being Element of Permutations n st
for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies b1 . k = perm . k ) & ( perm . k >= perm . i implies b1 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b1 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b1 . k = (perm . (k + 1)) - 1 ) ) ) )
uniqueness
for b1, b2 being Element of Permutations n st ( for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies b1 . k = perm . k ) & ( perm . k >= perm . i implies b1 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b1 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b1 . k = (perm . (k + 1)) - 1 ) ) ) ) ) & ( for k being Nat st k in Seg n holds
( ( k < i implies ( ( perm . k < perm . i implies b2 . k = perm . k ) & ( perm . k >= perm . i implies b2 . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b2 . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b2 . k = (perm . (k + 1)) - 1 ) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines Rem LAPLACE:def 3 :
for
i,
n being
Nat for
perm being
Element of
Permutations (n + 1) st
i in Seg (n + 1) holds
for
b4 being
Element of
Permutations n holds
(
b4 = Rem perm,
i iff for
k being
Nat st
k in Seg n holds
( (
k < i implies ( (
perm . k < perm . i implies
b4 . k = perm . k ) & (
perm . k >= perm . i implies
b4 . k = (perm . k) - 1 ) ) ) & (
k >= i implies ( (
perm . (k + 1) < perm . i implies
b4 . k = perm . (k + 1) ) & (
perm . (k + 1) >= perm . i implies
b4 . k = (perm . (k + 1)) - 1 ) ) ) ) );
theorem Th20: :: LAPLACE:20
theorem Th21: :: LAPLACE:21
theorem Th22: :: LAPLACE:22
:: deftheorem defines Minor LAPLACE:def 4 :
definition
let i,
j,
n be
Nat;
let K be
Field;
let M be
Matrix of
n,
K;
func Cofactor M,
i,
j -> Element of
K equals :: LAPLACE:def 5
((power K) . (- (1_ K)),(i + j)) * (Minor M,i,j);
coherence
((power K) . (- (1_ K)),(i + j)) * (Minor M,i,j) is Element of K
;
end;
:: deftheorem defines Cofactor LAPLACE:def 5 :
theorem Th23: :: LAPLACE:23
theorem Th24: :: LAPLACE:24
definition
let n be
Nat;
let K be
Field;
let M be
Matrix of
n,
K;
func Matrix_of_Cofactor M -> Matrix of
n,
K means :
Def6:
:: LAPLACE:def 6
for
i,
j being
Nat st
[i,j] in Indices it holds
it * i,
j = Cofactor M,
i,
j;
existence
ex b1 being Matrix of n,K st
for i, j being Nat st [i,j] in Indices b1 holds
b1 * i,j = Cofactor M,i,j
uniqueness
for b1, b2 being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * i,j = Cofactor M,i,j ) & ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * i,j = Cofactor M,i,j ) holds
b1 = b2
end;
:: deftheorem Def6 defines Matrix_of_Cofactor LAPLACE:def 6 :
definition
let n,
i be
Nat;
let K be
Field;
let M be
Matrix of
n,
K;
func LaplaceExpL M,
i -> FinSequence of
K means :
Def7:
:: LAPLACE:def 7
(
len it = n & ( for
j being
Nat st
j in dom it holds
it . j = (M * i,j) * (Cofactor M,i,j) ) );
existence
ex b1 being FinSequence of K st
( len b1 = n & ( for j being Nat st j in dom b1 holds
b1 . j = (M * i,j) * (Cofactor M,i,j) ) )
uniqueness
for b1, b2 being FinSequence of K st len b1 = n & ( for j being Nat st j in dom b1 holds
b1 . j = (M * i,j) * (Cofactor M,i,j) ) & len b2 = n & ( for j being Nat st j in dom b2 holds
b2 . j = (M * i,j) * (Cofactor M,i,j) ) holds
b1 = b2
end;
:: deftheorem Def7 defines LaplaceExpL LAPLACE:def 7 :
definition
let n,
j be
Nat;
let K be
Field;
let M be
Matrix of
n,
K;
func LaplaceExpC M,
j -> FinSequence of
K means :
Def8:
:: LAPLACE:def 8
(
len it = n & ( for
i being
Nat st
i in dom it holds
it . i = (M * i,j) * (Cofactor M,i,j) ) );
existence
ex b1 being FinSequence of K st
( len b1 = n & ( for i being Nat st i in dom b1 holds
b1 . i = (M * i,j) * (Cofactor M,i,j) ) )
uniqueness
for b1, b2 being FinSequence of K st len b1 = n & ( for i being Nat st i in dom b1 holds
b1 . i = (M * i,j) * (Cofactor M,i,j) ) & len b2 = n & ( for i being Nat st i in dom b2 holds
b2 . i = (M * i,j) * (Cofactor M,i,j) ) holds
b1 = b2
end;
:: deftheorem Def8 defines LaplaceExpC LAPLACE:def 8 :
theorem Th25: :: LAPLACE:25
theorem Th26: :: LAPLACE:26
theorem :: LAPLACE:27
theorem Th28: :: LAPLACE:28
theorem Th29: :: LAPLACE:29
theorem Th30: :: LAPLACE:30
theorem Th31: :: LAPLACE:31
theorem Th32: :: LAPLACE:32
theorem Th33: :: LAPLACE:33
theorem Th34: :: LAPLACE:34
theorem Th35: :: LAPLACE:35
theorem :: LAPLACE:36
theorem Th37: :: LAPLACE:37
theorem Th38: :: LAPLACE:38
:: deftheorem defines * LAPLACE:def 9 :
:: deftheorem defines * LAPLACE:def 10 :
theorem :: LAPLACE:39
theorem :: LAPLACE:40