:: by Karol P\c{a}k and Andrzej Trybulec

::

:: Received August 13, 2007

:: Copyright (c) 2007-2012 Association of Mizar Users

begin

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

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

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

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

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

B . (g,i) is Element of G

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

B . (g,i) is Element of G

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 !

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

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

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

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 )

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 )

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 ;

coherence

Deleting (M,i,j) is Matrix of n -' 1,K

end;
let K be Field;

let M be Matrix of n,K;

assume that

A1: i in Seg n and

A2: j in Seg n ;

coherence

Deleting (M,i,j) is Matrix of n -' 1,K

proof end;

:: deftheorem Def1 defines Delete LAPLACE:def 1 :

for i, j, n being Nat

for K being Field

for M being Matrix of n,K st i in Seg n & j in Seg n holds

Delete (M,i,j) = Deleting (M,i,j);

for i, j, n being Nat

for K being Field

for M being Matrix of n,K st i in Seg n & j in Seg n holds

Delete (M,i,j) = Deleting (M,i,j);

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

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)

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)

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;

for b_{1} being Matrix of n,m,D holds verum
;

existence

( ( len pD = len M implies ex b_{1} being Matrix of n,m,D st

( len b_{1} = len M & width b_{1} = width M & ( for i, j being Nat st [i,j] in Indices M holds

( ( j <> c implies b_{1} * (i,j) = M * (i,j) ) & ( j = c implies b_{1} * (i,c) = pD . i ) ) ) ) ) & ( not len pD = len M implies ex b_{1} being Matrix of n,m,D st b_{1} = M ) )

for b_{1}, b_{2} being Matrix of n,m,D holds

( ( len pD = len M & len b_{1} = len M & width b_{1} = width M & ( for i, j being Nat st [i,j] in Indices M holds

( ( j <> c implies b_{1} * (i,j) = M * (i,j) ) & ( j = c implies b_{1} * (i,c) = pD . i ) ) ) & len b_{2} = len M & width b_{2} = width M & ( for i, j being Nat st [i,j] in Indices M holds

( ( j <> c implies b_{2} * (i,j) = M * (i,j) ) & ( j = c implies b_{2} * (i,c) = pD . i ) ) ) implies b_{1} = b_{2} ) & ( not len pD = len M & b_{1} = M & b_{2} = M implies b_{1} = b_{2} ) )

end;
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 ( 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;

for b

existence

( ( len pD = len M implies ex b

( len b

( ( j <> c implies b

proof end;

uniqueness for b

( ( len pD = len M & len b

( ( j <> c implies b

( ( j <> c implies b

proof 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 b_{7} being Matrix of n,m,D holds

( ( len pD = len M implies ( b_{7} = ReplaceCol (M,c,pD) iff ( len b_{7} = len M & width b_{7} = width M & ( for i, j being Nat st [i,j] in Indices M holds

( ( j <> c implies b_{7} * (i,j) = M * (i,j) ) & ( j = c implies b_{7} * (i,c) = pD . i ) ) ) ) ) ) & ( not len pD = len M implies ( b_{7} = ReplaceCol (M,c,pD) iff b_{7} = M ) ) );

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 b

( ( len pD = len M implies ( b

( ( j <> c implies b

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

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

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

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

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

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

ex b_{1} being Element of Permutations n st

for k being Nat st k in Seg n holds

( ( k < i implies ( ( perm . k < perm . i implies b_{1} . k = perm . k ) & ( perm . k >= perm . i implies b_{1} . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b_{1} . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b_{1} . k = (perm . (k + 1)) - 1 ) ) ) )

for b_{1}, b_{2} being Element of Permutations n st ( for k being Nat st k in Seg n holds

( ( k < i implies ( ( perm . k < perm . i implies b_{1} . k = perm . k ) & ( perm . k >= perm . i implies b_{1} . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b_{1} . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b_{1} . k = (perm . (k + 1)) - 1 ) ) ) ) ) & ( for k being Nat st k in Seg n holds

( ( k < i implies ( ( perm . k < perm . i implies b_{2} . k = perm . k ) & ( perm . k >= perm . i implies b_{2} . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b_{2} . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b_{2} . k = (perm . (k + 1)) - 1 ) ) ) ) ) holds

b_{1} = b_{2}

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

ex b

for k being Nat st k in Seg n holds

( ( k < i implies ( ( perm . k < perm . i implies b

proof end;

uniqueness for b

( ( k < i implies ( ( perm . k < perm . i implies b

( ( k < i implies ( ( perm . k < perm . i implies b

b

proof 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 b_{4} being Element of Permutations n holds

( b_{4} = Rem (perm,i) iff for k being Nat st k in Seg n holds

( ( k < i implies ( ( perm . k < perm . i implies b_{4} . k = perm . k ) & ( perm . k >= perm . i implies b_{4} . k = (perm . k) - 1 ) ) ) & ( k >= i implies ( ( perm . (k + 1) < perm . i implies b_{4} . k = perm . (k + 1) ) & ( perm . (k + 1) >= perm . i implies b_{4} . k = (perm . (k + 1)) - 1 ) ) ) ) );

for i, n being Nat

for perm being Element of Permutations (n + 1) st i in Seg (n + 1) holds

for b

( b

( ( k < i implies ( ( perm . k < perm . i implies b

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

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

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

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;

coherence

Det (Delete (M,i,j)) is Element of K ;

end;
let K be Field;

let M be Matrix of n,K;

coherence

Det (Delete (M,i,j)) is Element of K ;

:: deftheorem defines Minor LAPLACE:def 4 :

for i, j, n being Nat

for K being Field

for M being Matrix of n,K holds Minor (M,i,j) = Det (Delete (M,i,j));

for i, j, n being Nat

for K being Field

for M being Matrix of n,K holds Minor (M,i,j) = Det (Delete (M,i,j));

definition

let i, j, n be Nat;

let K be Field;

let M be Matrix of n,K;

((power K) . ((- (1_ K)),(i + j))) * (Minor (M,i,j)) is Element of K ;

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

((power K) . ((- (1_ K)),(i + j))) * (Minor (M,i,j)) is Element of K ;

:: deftheorem defines Cofactor LAPLACE:def 5 :

for i, j, n being Nat

for K being Field

for M being Matrix of n,K holds Cofactor (M,i,j) = ((power K) . ((- (1_ K)),(i + j))) * (Minor (M,i,j));

for i, j, n being Nat

for K being Field

for M being Matrix of n,K holds Cofactor (M,i,j) = ((power K) . ((- (1_ K)),(i + j))) * (Minor (M,i,j));

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

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)

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;

ex b_{1} being Matrix of n,K st

for i, j being Nat st [i,j] in Indices b_{1} holds

b_{1} * (i,j) = Cofactor (M,i,j)

for b_{1}, b_{2} being Matrix of n,K st ( for i, j being Nat st [i,j] in Indices b_{1} holds

b_{1} * (i,j) = Cofactor (M,i,j) ) & ( for i, j being Nat st [i,j] in Indices b_{2} holds

b_{2} * (i,j) = Cofactor (M,i,j) ) holds

b_{1} = b_{2}

end;
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 for i, j being Nat st [i,j] in Indices it holds

it * (i,j) = Cofactor (M,i,j);

ex b

for i, j being Nat st [i,j] in Indices b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines Matrix_of_Cofactor LAPLACE:def 6 :

for n being Nat

for K being Field

for M, b_{4} being Matrix of n,K holds

( b_{4} = Matrix_of_Cofactor M iff for i, j being Nat st [i,j] in Indices b_{4} holds

b_{4} * (i,j) = Cofactor (M,i,j) );

for n being Nat

for K being Field

for M, b

( b

b

begin

definition

let n, i be Nat;

let K be Field;

let M be Matrix of n,K;

ex b_{1} being FinSequence of K st

( len b_{1} = n & ( for j being Nat st j in dom b_{1} holds

b_{1} . j = (M * (i,j)) * (Cofactor (M,i,j)) ) )

for b_{1}, b_{2} being FinSequence of K st len b_{1} = n & ( for j being Nat st j in dom b_{1} holds

b_{1} . j = (M * (i,j)) * (Cofactor (M,i,j)) ) & len b_{2} = n & ( for j being Nat st j in dom b_{2} holds

b_{2} . j = (M * (i,j)) * (Cofactor (M,i,j)) ) holds

b_{1} = b_{2}

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

existence ( len it = n & ( for j being Nat st j in dom it holds

it . j = (M * (i,j)) * (Cofactor (M,i,j)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines LaplaceExpL LAPLACE:def 7 :

for n, i being Nat

for K being Field

for M being Matrix of n,K

for b_{5} being FinSequence of K holds

( b_{5} = LaplaceExpL (M,i) iff ( len b_{5} = n & ( for j being Nat st j in dom b_{5} holds

b_{5} . j = (M * (i,j)) * (Cofactor (M,i,j)) ) ) );

for n, i being Nat

for K being Field

for M being Matrix of n,K

for b

( b

b

definition

let n, j be Nat;

let K be Field;

let M be Matrix of n,K;

ex b_{1} being FinSequence of K st

( len b_{1} = n & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (M * (i,j)) * (Cofactor (M,i,j)) ) )

for b_{1}, b_{2} being FinSequence of K st len b_{1} = n & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (M * (i,j)) * (Cofactor (M,i,j)) ) & len b_{2} = n & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (M * (i,j)) * (Cofactor (M,i,j)) ) holds

b_{1} = b_{2}

end;
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 ( len it = n & ( for i being Nat st i in dom it holds

it . i = (M * (i,j)) * (Cofactor (M,i,j)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines LaplaceExpC LAPLACE:def 8 :

for n, j being Nat

for K being Field

for M being Matrix of n,K

for b_{5} being FinSequence of K holds

( b_{5} = LaplaceExpC (M,j) iff ( len b_{5} = n & ( for i being Nat st i in dom b_{5} holds

b_{5} . i = (M * (i,j)) * (Cofactor (M,i,j)) ) ) );

for n, j being Nat

for K being Field

for M being Matrix of n,K

for b

( b

b

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

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)

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

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)

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

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)

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)

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

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)

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 )

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

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

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

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

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

<*f*> is Matrix of 1, len f,D by MATRIX_1:11;

end;
let f be FinSequence of D;

:: original: <*

redefine func <*f*> -> Matrix of 1, len f,D;

coherence

<*f*> is Matrix of 1, len f,D by MATRIX_1:11;

definition

let K be Field;

let M be Matrix of K;

let f be FinSequence of K;

coherence

M * (<*f*> @) is Matrix of K ;

coherence

<*f*> * M is Matrix of K ;

end;
let M be Matrix of K;

let f be FinSequence of K;

coherence

M * (<*f*> @) is Matrix of K ;

coherence

<*f*> * M is Matrix of K ;

:: deftheorem defines * LAPLACE:def 9 :

for K being Field

for M being Matrix of K

for f being FinSequence of K holds M * f = M * (<*f*> @);

for K being Field

for M being Matrix of K

for f being FinSequence of K holds M * f = M * (<*f*> @);

:: deftheorem defines * LAPLACE:def 10 :

for K being Field

for M being Matrix of K

for f being FinSequence of K holds f * M = <*f*> * M;

for K being Field

for M being Matrix of K

for f being FinSequence of K holds f * M = <*f*> * M;

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

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

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;