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 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; 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( 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)
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)
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;
now for x being object st x in dom (g * f) holds
(LaplaceExpL (M,i)) . x = (g * f) . xA32:
rng f c= Fin (Permutations n)
by RELAT_1:def 19;
let x be
object ;
( 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
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;
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
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
;
verum