LAPLACE: Laplace Expansion

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

proof end;

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

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

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

proof end;

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;

Laplace expansion

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

proof end;

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

proof end;

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*> @);

func f * M -> Matrix of K equals :: LAPLACE:def 10
<*f*> * M;