let n be Nat; :: thesis: 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))

let K be Field; :: thesis: for i being Nat

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

Det M = Sum (LaplaceExpL (M,i))

reconsider N = n as Element of NAT by ORDINAL1:def 12;

set P = Permutations n;

set KK = the carrier of K;

set aa = the addF of K;

A1: the addF of K is having_a_unity by FVSUM_1:8;

let i be Nat; :: thesis: for M being Matrix of n,K st i in Seg n holds

Det M = Sum (LaplaceExpL (M,i))

let M be Matrix of n,K; :: thesis: ( i in Seg n implies Det M = Sum (LaplaceExpL (M,i)) )

assume A2: i in Seg n ; :: thesis: Det M = Sum (LaplaceExpL (M,i))

reconsider X = finSeg N as non empty set by A2;

set Path = Path_product M;

deffunc H_{1}( Element of Fin (Permutations n)) -> Element of the carrier of K = the addF of K $$ ($1,(Path_product M));

consider g being Function of (Fin (Permutations n)), the carrier of K such that

A3: for x being Element of Fin (Permutations n) holds g . x = H_{1}(x)
from FUNCT_2:sch 4();

A4: for A, B being Element of Fin (Permutations n) st A misses B holds

the addF of K . ((g . A),(g . B)) = g . (A \/ B)_{2}( object ) -> set = { p where p is Element of Permutations n : p . i = $1 } ;

consider f being Function such that

A8: ( dom f = X & ( for x being object st x in X holds

f . x = H_{2}(x) ) )
from FUNCT_1:sch 3();

rng f c= Fin (Permutations n)

A12: g . (In ((Permutations n),(Fin (Permutations n)))) = Det M by A3;

set gf = g * f;

A13: dom (g * f) = X by FUNCT_2:def 1;

then A14: (g * f) * (id X) = g * f by RELAT_1:52;

A15: Permutations n c= union (f .: X)

len (LaplaceExpL (M,i)) = n by Def7;

then A21: dom (LaplaceExpL (M,i)) = Seg n by FINSEQ_1:def 3;

then A22: dom (id X) = dom (LaplaceExpL (M,i)) ;

reconsider X9 = X as Element of Fin X by FINSUB_1:def 5;

Permutations n in Fin (Permutations n) by FINSUB_1:def 5;

then A23: In ((Permutations n),(Fin (Permutations n))) = Permutations n by SUBSET_1:def 8;

g . ({}. (Fin (Permutations n))) = the addF of K $$ (({}. (Permutations n)),(Path_product M)) by A3;

then A24: g . {} = the_unity_wrt the addF of K by FVSUM_1:8, SETWISEO:31;

set Laa = [#] ((LaplaceExpL (M,i)),(the_unity_wrt the addF of K));

A38: rng (id X) = X9 ;

A39: ([#] ((LaplaceExpL (M,i)),(the_unity_wrt the addF of K))) | (dom (LaplaceExpL (M,i))) = LaplaceExpL (M,i) by SETWOP_2:21;

union (f .: X) c= Permutations n

then A44: the addF of K $$ ((f .: X9),g) = g . (In ((Permutations n),(Fin (Permutations n)))) by A25, A4, A1, A24, A23, Th12;

the addF of K $$ (X9,(g * f)) = the addF of K $$ ((f .: X9),g) by A25, A4, A1, A24, Th12;

hence Det M = the addF of K $$ ((findom (LaplaceExpL (M,i))),([#] ((LaplaceExpL (M,i)),(the_unity_wrt the addF of K)))) by A22, A38, A39, A14, A37, A44, A12, SETWOP_2:5

.= Sum (LaplaceExpL (M,i)) by FVSUM_1:8, SETWOP_2:def 2 ;

:: thesis: verum

for i being Nat

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

Det M = Sum (LaplaceExpL (M,i))

let K be Field; :: thesis: for i being Nat

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

Det M = Sum (LaplaceExpL (M,i))

reconsider N = n as Element of NAT by ORDINAL1:def 12;

set P = Permutations n;

set KK = the carrier of K;

set aa = the addF of K;

A1: the addF of K is having_a_unity by FVSUM_1:8;

let i be Nat; :: thesis: for M being Matrix of n,K st i in Seg n holds

Det M = Sum (LaplaceExpL (M,i))

let M be Matrix of n,K; :: thesis: ( i in Seg n implies Det M = Sum (LaplaceExpL (M,i)) )

assume A2: i in Seg n ; :: thesis: Det M = Sum (LaplaceExpL (M,i))

reconsider X = finSeg N as non empty set by A2;

set Path = Path_product M;

deffunc H

consider g being Function of (Fin (Permutations n)), the carrier of K such that

A3: for x being Element of Fin (Permutations n) holds g . x = H

A4: for A, B being Element of Fin (Permutations n) st A misses B holds

the addF of K . ((g . A),(g . B)) = g . (A \/ B)

proof

deffunc H
let A, B be Element of Fin (Permutations n); :: thesis: ( A misses B implies the addF of K . ((g . A),(g . B)) = g . (A \/ B) )

assume A5: A misses B ; :: thesis: the addF of K . ((g . A),(g . B)) = g . (A \/ B)

A6: g . A = H_{1}(A)
by A3;

A7: g . B = H_{1}(B)
by A3;

g . (A \/ B) = H_{1}(A \/ B)
by A3;

hence the addF of K . ((g . A),(g . B)) = g . (A \/ B) by A5, A6, A7, FVSUM_1:8, SETWOP_2:4; :: thesis: verum

end;assume A5: A misses B ; :: thesis: the addF of K . ((g . A),(g . B)) = g . (A \/ B)

A6: g . A = H

A7: g . B = H

g . (A \/ B) = H

hence the addF of K . ((g . A),(g . B)) = g . (A \/ B) by A5, A6, A7, FVSUM_1:8, SETWOP_2:4; :: thesis: verum

consider f being Function such that

A8: ( dom f = X & ( for x being object st x in X holds

f . x = H

rng f c= Fin (Permutations n)

proof

then reconsider f = f as Function of X,(Fin (Permutations n)) by A8, FUNCT_2:2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Fin (Permutations n) )

assume x in rng f ; :: thesis: x in Fin (Permutations n)

then consider y being object such that

A9: y in dom f and

A10: f . y = x by FUNCT_1:def 3;

A11: H_{2}(y) c= Permutations n
_{2}(y) in Fin (Permutations n)
by A11, FINSUB_1:def 5;

hence x in Fin (Permutations n) by A8, A9, A10; :: thesis: verum

end;assume x in rng f ; :: thesis: x in Fin (Permutations n)

then consider y being object such that

A9: y in dom f and

A10: f . y = x by FUNCT_1:def 3;

A11: H

proof

H
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in H_{2}(y) or z in Permutations n )

assume z in H_{2}(y)
; :: thesis: z in Permutations n

then ex p being Element of Permutations n st

( p = z & p . i = y ) ;

hence z in Permutations n ; :: thesis: verum

end;assume z in H

then ex p being Element of Permutations n st

( p = z & p . i = y ) ;

hence z in Permutations n ; :: thesis: verum

hence x in Fin (Permutations n) by A8, A9, A10; :: thesis: verum

A12: g . (In ((Permutations n),(Fin (Permutations n)))) = Det M by A3;

set gf = g * f;

A13: dom (g * f) = X by FUNCT_2:def 1;

then A14: (g * f) * (id X) = g * f by RELAT_1:52;

A15: Permutations n c= union (f .: X)

proof

set L = LaplaceExpL (M,i);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Permutations n or x in union (f .: X) )

assume A16: x in Permutations n ; :: thesis: x in union (f .: X)

then reconsider p = x as Permutation of X by MATRIX_1:def 12;

A17: x in H_{2}(p . i)
by A16;

A18: rng p = X by FUNCT_2:def 3;

dom p = X by FUNCT_2:52;

then A19: p . i in X by A2, A18, FUNCT_1:def 3;

then A20: f . (p . i) in f .: X by A8, FUNCT_1:def 6;

f . (p . i) = H_{2}(p . i)
by A8, A19;

hence x in union (f .: X) by A17, A20, TARSKI:def 4; :: thesis: verum

end;assume A16: x in Permutations n ; :: thesis: x in union (f .: X)

then reconsider p = x as Permutation of X by MATRIX_1:def 12;

A17: x in H

A18: rng p = X by FUNCT_2:def 3;

dom p = X by FUNCT_2:52;

then A19: p . i in X by A2, A18, FUNCT_1:def 3;

then A20: f . (p . i) in f .: X by A8, FUNCT_1:def 6;

f . (p . i) = H

hence x in union (f .: X) by A17, A20, TARSKI:def 4; :: thesis: verum

len (LaplaceExpL (M,i)) = n by Def7;

then A21: dom (LaplaceExpL (M,i)) = Seg n by FINSEQ_1:def 3;

then A22: dom (id X) = dom (LaplaceExpL (M,i)) ;

reconsider X9 = X as Element of Fin X by FINSUB_1:def 5;

Permutations n in Fin (Permutations n) by FINSUB_1:def 5;

then A23: In ((Permutations n),(Fin (Permutations n))) = Permutations n by SUBSET_1:def 8;

g . ({}. (Fin (Permutations n))) = the addF of K $$ (({}. (Permutations n)),(Path_product M)) by A3;

then A24: g . {} = the_unity_wrt the addF of K by FVSUM_1:8, SETWISEO:31;

A25: now :: thesis: for x, y being object st x in X9 & y in X9 & f . x meets f . y holds

x = y

x = y

let x, y be object ; :: thesis: ( x in X9 & y in X9 & f . x meets f . y implies x = y )

assume that

A26: x in X9 and

A27: y in X9 and

A28: f . x meets f . y ; :: thesis: x = y

consider z being object such that

A29: z in f . x and

A30: z in f . y by A28, XBOOLE_0:3;

f . y = H_{2}(y)
by A8, A27;

then A31: ex p being Element of Permutations n st

( p = z & p . i = y ) by A30;

f . x = H_{2}(x)
by A8, A26;

then ex p being Element of Permutations n st

( p = z & p . i = x ) by A29;

hence x = y by A31; :: thesis: verum

end;assume that

A26: x in X9 and

A27: y in X9 and

A28: f . x meets f . y ; :: thesis: x = y

consider z being object such that

A29: z in f . x and

A30: z in f . y by A28, XBOOLE_0:3;

f . y = H

then A31: ex p being Element of Permutations n st

( p = z & p . i = y ) by A30;

f . x = H

then ex p being Element of Permutations n st

( p = z & p . i = x ) by A29;

hence x = y by A31; :: thesis: verum

now :: thesis: for x being object st x in dom (g * f) holds

(LaplaceExpL (M,i)) . x = (g * f) . x

then A37:
LaplaceExpL (M,i) = g * f
by A21, A13, FUNCT_1:2;(LaplaceExpL (M,i)) . x = (g * f) . x

A32:
rng f c= Fin (Permutations n)
by RELAT_1:def 19;

let x be object ; :: thesis: ( x in dom (g * f) implies (LaplaceExpL (M,i)) . x = (g * f) . x )

assume A33: x in dom (g * f) ; :: thesis: (LaplaceExpL (M,i)) . x = (g * f) . x

consider k being Nat such that

A34: k = x and

1 <= k and

k <= n by A13, A33;

f . k in rng f by A8, A33, A34, FUNCT_1:def 3;

then reconsider Fk = H_{2}(k) as Element of Fin (Permutations n) by A8, A33, A34, A32;

A35: f . k = Fk by A8, A33, A34;

(g * f) . k = g . (f . k) by A8, A33, A34, FUNCT_1:13;

then A36: (g * f) . k = H_{1}(Fk)
by A3, A35;

H_{1}(Fk) = (M * (i,k)) * (Cofactor (M,i,k))
by A2, A33, A34, Th23;

hence (LaplaceExpL (M,i)) . x = (g * f) . x by A21, A33, A34, A36, Def7; :: thesis: verum

end;let x be object ; :: thesis: ( x in dom (g * f) implies (LaplaceExpL (M,i)) . x = (g * f) . x )

assume A33: x in dom (g * f) ; :: thesis: (LaplaceExpL (M,i)) . x = (g * f) . x

consider k being Nat such that

A34: k = x and

1 <= k and

k <= n by A13, A33;

f . k in rng f by A8, A33, A34, FUNCT_1:def 3;

then reconsider Fk = H

A35: f . k = Fk by A8, A33, A34;

(g * f) . k = g . (f . k) by A8, A33, A34, FUNCT_1:13;

then A36: (g * f) . k = H

H

hence (LaplaceExpL (M,i)) . x = (g * f) . x by A21, A33, A34, A36, Def7; :: thesis: verum

set Laa = [#] ((LaplaceExpL (M,i)),(the_unity_wrt the addF of K));

A38: rng (id X) = X9 ;

A39: ([#] ((LaplaceExpL (M,i)),(the_unity_wrt the addF of K))) | (dom (LaplaceExpL (M,i))) = LaplaceExpL (M,i) by SETWOP_2:21;

union (f .: X) c= Permutations n

proof

then
Permutations n = union (f .: X)
by A15, XBOOLE_0:def 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (f .: X) or x in Permutations n )

assume x in union (f .: X) ; :: thesis: x in Permutations n

then consider y being set such that

A40: x in y and

A41: y in f .: X by TARSKI:def 4;

consider z being object such that

A42: z in dom f and

z in X and

A43: f . z = y by A41, FUNCT_1:def 6;

y = H_{2}(z)
by A8, A42, A43;

then ex p being Element of Permutations n st

( x = p & p . i = z ) by A40;

hence x in Permutations n ; :: thesis: verum

end;assume x in union (f .: X) ; :: thesis: x in Permutations n

then consider y being set such that

A40: x in y and

A41: y in f .: X by TARSKI:def 4;

consider z being object such that

A42: z in dom f and

z in X and

A43: f . z = y by A41, FUNCT_1:def 6;

y = H

then ex p being Element of Permutations n st

( x = p & p . i = z ) by A40;

hence x in Permutations n ; :: thesis: verum

then A44: the addF of K $$ ((f .: X9),g) = g . (In ((Permutations n),(Fin (Permutations n)))) by A25, A4, A1, A24, A23, Th12;

the addF of K $$ (X9,(g * f)) = the addF of K $$ ((f .: X9),g) by A25, A4, A1, A24, Th12;

hence Det M = the addF of K $$ ((findom (LaplaceExpL (M,i))),([#] ((LaplaceExpL (M,i)),(the_unity_wrt the addF of K)))) by A22, A38, A39, A14, A37, A44, A12, SETWOP_2:5

.= Sum (LaplaceExpL (M,i)) by FVSUM_1:8, SETWOP_2:def 2 ;

:: thesis: verum