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 H1( 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 = H1(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)
proof
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 = H1(A) by A3;
A7: g . B = H1(B) by A3;
g . (A \/ B) = H1(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;
deffunc H2( 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 = H2(x) ) ) from FUNCT_1:sch 3();
 rng f c= Fin (Permutations n)
proof
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: H2(y) c= Permutations n
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in H2(y) or z in Permutations n )
assume z in H2(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;
H2(y) in Fin (Permutations n) by A11, FINSUB_1:def 5;
hence x in Fin (Permutations n) by A8, A9, A10; :: thesis: verum
end;
then reconsider f = f as Function of X,(Fin (Permutations n)) by A8, FUNCT_2:2;
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
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 H2(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) = H2(p . i) by A8, A19;
hence x in union (f .: X) by A17, A20, TARSKI:def 4; :: thesis: verum
end;
set L = LaplaceExpL (M,i);
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
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 = H2(y) by A8, A27;
then A31: ex p being Element of Permutations n st
( p = z & p . i = y ) by A30;
f . x = H2(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;
now :: thesis: for x being object st x in dom (g * f) holds
(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 = H2(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 = H1(Fk) by A3, A35;
H1(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;
then A37: LaplaceExpL (M,i) = g * f by A21, A13, FUNCT_1:2;
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
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 = H2(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;
then Permutations n = union (f .: X) by A15, XBOOLE_0:def 10;
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