LAPLACE: Laplace Expansion

:: Laplace Expansion
:: by Karol P\c{a}k and Andrzej Trybulec
::
:: Received August 13, 2007
:: Copyright (c) 2007 Association of Mizar Users

begin

theorem Th1: :: LAPLACE:1

for f being FinSequence
for i being Nat st i in dom f holds
len (Del f,i) = (len f) -' 1

proof end;

theorem Th2: :: LAPLACE:2

for K being Field
for i, j, n being Nat
for M being Matrix of n,K st i in dom M holds
len (Deleting M,i,j) = n -' 1

proof end;

theorem Th3: :: LAPLACE:3

for j being Nat
for K being Field
for A being Matrix of K st j in Seg (width A) holds
width (DelCol A,j) = (width A) -' 1

proof end;

theorem Th4: :: LAPLACE:4

for K being Field
for A being Matrix of K
for i being Nat st len A > 1 holds
width A = width (DelLine A,i)

proof end;

theorem Th5: :: LAPLACE:5

for j, n being Nat
for K being Field
for M being Matrix of n,K
for i being Nat st j in Seg (width M) holds
width (Deleting M,i,j) = n -' 1

proof end;

definition

let G be non empty multMagma ;
let B be Function of [:the carrier of G,NAT :],the carrier of G;
let g be Element of G;
let i be Nat;
:: original: .
redefine func B . g,i -> Element of G;
coherence

proof end;

end;

theorem Th6: :: LAPLACE:6

for n being Nat holds card (Permutations n) = n !

proof end;

theorem Th7: :: LAPLACE:7

for n, i, j being Nat st i in Seg (n + 1) & j in Seg (n + 1) holds
card { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } = n !

proof end;

theorem Th8: :: LAPLACE:8

for n being Nat
for K being Fanoian Field
for p2 being Element of Permutations (n + 2)
for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } holds
the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(card Y)

proof end;

theorem Th9: :: LAPLACE:9

for n being Nat
for K being Fanoian Field
for p2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds
ex X being Element of Fin (2Set (Seg (n + 2))) st
( X = { {N,i} where N is Element of NAT : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(i + j) )

proof end;

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)} ) ) ) )

proof end;

theorem Th11: :: LAPLACE:11

for n being Nat st n < 2 holds
for p being Element of Permutations n holds
( p is even & p = idseq n )

proof end;

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 )

proof end;

begin

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

proof end;

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) ) )

proof end;

theorem Th14: :: LAPLACE:14

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
(Delete M,i,j) @ = Delete (M @ ),j,i

proof end;

theorem Th15: :: LAPLACE:15

for n being Nat
for K being Field
for M being Matrix of n,K
for f being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg n holds
Delete M,i,j = Delete (RLine M,i,f),i,j

proof end;

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 ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ReplaceCol LAPLACE:def 2 :

notation

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;
synonym RCol M,c,pD for ReplaceCol M,c,pD;

end;

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 ) )

proof end;

theorem :: LAPLACE:17

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 st not c in Seg (width AD) holds
RCol AD,c,pD = AD

proof end;

theorem :: LAPLACE:18

for n, m, c being Nat
for D being non empty set
for AD being Matrix of n,m,D holds RCol AD,c,(Col AD,c) = AD

proof end;

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 A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds
ReplaceCol A,c,pD = (ReplaceLine A9,c,pD) @

proof end;

begin

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Rem LAPLACE:def 3 :

theorem Th20: :: LAPLACE:20

for n, i, j being Nat st i in Seg (n + 1) & j in Seg (n + 1) holds
for P being set st P = { p1 where p1 is Element of Permutations (n + 1) : p1 . i = j } holds
ex Proj being Function of P,(Permutations n) st
( Proj is bijective & ( for q1 being Element of Permutations (n + 1) st q1 . i = j holds
Proj . q1 = Rem q1,i ) )

proof end;

theorem Th21: :: LAPLACE:21

for n being Nat
for p1 being Element of Permutations (n + 1)
for K being Field
for a being Element of K
for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds
- a,p1 = ((power K) . (- (1_ K)),(i + j)) * (- a,(Rem p1,i))

proof end;

theorem Th22: :: LAPLACE:22

for n being Nat
for p1 being Element of Permutations (n + 1)
for K being Field
for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds
for M being Matrix of n + 1,K
for DM being Matrix of n,K st DM = Delete M,i,j holds
(Path_product M) . p1 = (((power K) . (- (1_ K)),(i + j)) * (M * i,j)) * ((Path_product DM) . (Rem p1,i))

proof end;

begin

definition

let i, j, n be Nat;
let K be Field;
let M be Matrix of n,K;
func Minor M,i,j -> Element of K equals :: LAPLACE:def 4
Det (Delete M,i,j);
coherence ;

end;

:: 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 ;

end;

:: deftheorem defines Cofactor LAPLACE:def 5 :

theorem Th23: :: LAPLACE:23

for n being Nat
for K being Field
for i, j being Nat st i in Seg n & j in Seg n holds
for P being Element of Fin (Permutations n) st P = { p where p is Element of Permutations n : p . i = j } holds
for M being Matrix of n,K holds the addF of K $$ P,(Path_product M) = (M * i,j) * (Cofactor M,i,j)

proof end;

theorem Th24: :: LAPLACE:24

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
Minor M,i,j = Minor (M @ ),j,i

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Matrix_of_Cofactor LAPLACE:def 6 :

begin

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

proof end;

uniqueness

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines LaplaceExpC LAPLACE:def 8 :

theorem Th25: :: LAPLACE:25

for n being Nat
for K being Field
for i being Nat
for M being Matrix of n,K st i in Seg n holds
Det M = Sum (LaplaceExpL M,i)

proof end;

theorem Th26: :: LAPLACE:26

for n being Nat
for K being Field
for M being Matrix of n,K
for i being Nat st i in Seg n holds
LaplaceExpC M,i = LaplaceExpL (M @ ),i

proof end;

theorem :: LAPLACE:27

for n being Nat
for K being Field
for j being Nat
for M being Matrix of n,K st j in Seg n holds
Det M = Sum (LaplaceExpC M,j)

proof end;

theorem Th28: :: LAPLACE:28

for n being Nat
for K being Field
for f being FinSequence of K
for M being Matrix of n,K
for p being Element of Permutations n
for i being Nat st len f = n & i in Seg n holds
mlt (Line (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine M,i,f),i

proof end;

theorem Th29: :: LAPLACE:29

for i, n, j being Nat
for K being Field
for M being Matrix of n,K st i in Seg n holds
(Line M,j) "*" (Col ((Matrix_of_Cofactor M) @ ),i) = Det (RLine M,i,(Line M,j))

proof end;

theorem Th30: :: LAPLACE:30

for n being Nat
for K being Field
for M being Matrix of n,K st Det M <> 0. K holds
M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) = 1. K,n

proof end;

theorem Th31: :: LAPLACE:31

for n being Nat
for K being Field
for M being Matrix of n,K
for f being FinSequence of K
for i being Nat st len f = n & i in Seg n holds
mlt (Col (Matrix_of_Cofactor M),i),f = LaplaceExpL (RLine (M @ ),i,f),i

proof end;

theorem Th32: :: LAPLACE:32

for i, n, j being Nat
for K being Field
for M being Matrix of n,K st i in Seg n & j in Seg n holds
(Line ((Matrix_of_Cofactor M) @ ),i) "*" (Col M,j) = Det (RLine (M @ ),i,(Line (M @ ),j))

proof end;

theorem Th33: :: LAPLACE:33

for n being Nat
for K being Field
for M being Matrix of n,K st Det M <> 0. K holds
(((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n

proof end;

theorem Th34: :: LAPLACE:34

for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is invertible iff Det M <> 0. K )

proof end;

theorem Th35: :: LAPLACE:35

for n being Nat
for K being Field
for M being Matrix of n,K st Det M <> 0. K holds
M ~ = ((Det M) " ) * ((Matrix_of_Cofactor M) @ )

proof end;

theorem :: LAPLACE:36

for n being Nat
for K being Field
for M being Matrix of n,K st M is invertible holds
for i, j being Nat st [i,j] in Indices (M ~ ) holds
(M ~ ) * i,j = (((Det M) " ) * ((power K) . (- (1_ K)),(i + j))) * (Minor M,j,i)

proof end;

theorem Th37: :: LAPLACE:37

for n being Nat
for K being Field
for A being Matrix of n,K st Det A <> 0. K holds
for x, b being Matrix of K st len x = n & A * x = b holds
( x = (A ~ ) * b & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceCol A,i,(Col b,j))) ) )

proof end;

theorem Th38: :: LAPLACE:38

for n being Nat
for K being Field
for A being Matrix of n,K st Det A <> 0. K holds
for x, b being Matrix of K st width x = n & x * A = b holds
( x = b * (A ~ ) & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceLine A,j,(Line b,i))) ) )

proof end;

begin

definition

let D be non empty set ;
let f be FinSequence of D;
:: original: <*
redefine func <*f*> -> Matrix of 1, len f,D;
coherence by MATRIX_1:11;

end;

definition

let K be Field;
let M be Matrix of K;
let f be FinSequence of K;
func M * f -> Matrix of K equals :: LAPLACE:def 9
M * (<*f*> @ );
coherence ;
func f * M -> Matrix of K equals :: LAPLACE:def 10
<*f*> * M;
coherence ;

end;

:: deftheorem defines * LAPLACE:def 9 :

:: deftheorem defines * LAPLACE:def 10 :

theorem :: LAPLACE:39

for n being Nat
for K being Field
for A being Matrix of n,K st Det A <> 0. K holds
for x, b being FinSequence of K st len x = n & A * x = <*b*> @ holds
( <*x*> @ = (A ~ ) * b & ( for i being Nat st i in Seg n holds
x . i = ((Det A) " ) * (Det (ReplaceCol A,i,b)) ) )

proof end;

theorem :: LAPLACE:40

for n being Nat
for K being Field
for A being Matrix of n,K st Det A <> 0. K holds
for x, b being FinSequence of K st len x = n & x * A = <*b*> holds
( <*x*> = b * (A ~ ) & ( for i being Nat st i in Seg n holds
x . i = ((Det A) " ) * (Det (ReplaceLine A,i,b)) ) )

proof end;