let n be 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)
let K be Field; 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 13;
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:10;
let i be Nat; 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; ( i in Seg n implies Det M = Sum (LaplaceExpL M,i) )
assume A2:
i in Seg n
; 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)
deffunc H2( set ) -> 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 set st x in X holds
f . x = H2(x) ) )
from FUNCT_1:sch 3();
rng f c= Fin (Permutations n)
then reconsider f = f as Function of X,(Fin (Permutations n)) by A8, FUNCT_2:4;
A12:
g . (FinOmega (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:78;
A15:
Permutations n c= union (f .: X)
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)
by RELAT_1:71;
reconsider X9 = X as Element of Fin X by FINSUB_1:def 5;
A23:
FinOmega (Permutations n) = Permutations n
by MATRIX_2:30, MATRIX_2:def 17;
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:10, SETWISEO:40;
now A32:
rng f c= Fin (Permutations n)
by RELAT_1:def 19;
let x be
set ;
( x in dom (g * f) implies (LaplaceExpL M,i) . x = (g * f) . x )assume A33:
x in dom (g * f)
;
(LaplaceExpL M,i) . x = (g * f) . xconsider k being
Element of
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 5;
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:23;
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;
verum end;
then A37:
LaplaceExpL M,i = g * f
by A21, A13, FUNCT_1:9;
set Laa = [#] (LaplaceExpL M,i),(the_unity_wrt the addF of K);
A38:
rng (id X) = X9
by RELAT_1:71;
A39:
([#] (LaplaceExpL M,i),(the_unity_wrt the addF of K)) | (dom (LaplaceExpL M,i)) = LaplaceExpL M,i
by SETWOP_2:23;
union (f .: X) c= Permutations n
then
Permutations n = union (f .: X)
by A15, XBOOLE_0:def 10;
then A44:
the addF of K $$ (f .: X9),g = g . (FinOmega (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:7
.=
Sum (LaplaceExpL M,i)
by FVSUM_1:10, SETWOP_2:def 2
;
verum