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 ()) -> Element of the carrier of K = the addF of K \$\$ (\$1,());
consider g being Function of (Fin ()), the carrier of K such that
A3: for x being Element of Fin () holds g . x = H1(x) from A4: for A, B being Element of Fin () st A misses B holds
the addF of K . ((g . A),(g . B)) = g . (A \/ B)
proof
let A, B be Element of Fin (); :: 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 ; :: 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 rng f c= Fin ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Fin () )
assume x in rng f ; :: thesis: x in Fin ()
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:
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 () by ;
hence x in Fin () by A8, A9, A10; :: thesis: verum
end;
then reconsider f = f as Function of X,(Fin ()) by ;
A12: g . (In ((),(Fin ()))) = 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 ;
then A20: f . (p . i) in f .: X by ;
f . (p . i) = H2(p . i) by ;
hence x in union (f .: X) by ; :: 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 () by FINSUB_1:def 5;
then A23: In ((),(Fin ())) = Permutations n by SUBSET_1:def 8;
g . ({}. (Fin ())) = the addF of K \$\$ (({}. ()),()) by A3;
then A24: g . {} = the_unity_wrt the addF of K by ;
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 ;
f . y = H2(y) by ;
then A31: ex p being Element of Permutations n st
( p = z & p . i = y ) by A30;
f . x = H2(x) by ;
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 () 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 ;
f . k in rng f by ;
then reconsider Fk = H2(k) as Element of Fin () by A8, A33, A34, A32;
A35: f . k = Fk by A8, A33, A34;
(g * f) . k = g . (f . k) by ;
then A36: (g * f) . k = H1(Fk) by ;
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 ;
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:
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 ;
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 ;
then A44: the addF of K \$\$ ((f .: X9),g) = g . (In ((),(Fin ()))) 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
.= Sum (LaplaceExpL (M,i)) by ;
:: thesis: verum