let n be Nat; for K being Field
for M being Matrix of n,K
for f being FinSequence of K
for i being Nat st len f = n & i in Seg n holds
mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i)
let K be Field; for M being Matrix of n,K
for f being FinSequence of K
for i being Nat st len f = n & i in Seg n holds
mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i)
let M be Matrix of n,K; for f being FinSequence of K
for i being Nat st len f = n & i in Seg n holds
mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i)
let f be FinSequence of K; for i being Nat st len f = n & i in Seg n holds
mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i)
let i be Nat; ( len f = n & i in Seg n implies mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i) )
assume that
A1:
len f = n
and
A2:
i in Seg n
; mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i)
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set KK = the carrier of K;
set C = Matrix_of_Cofactor M;
reconsider Tp = f, TC = Col ((Matrix_of_Cofactor M),i) as Element of N -tuples_on the carrier of K by A1, FINSEQ_2:92, MATRIX_0:24;
set R = RLine ((M @),i,f);
set LL = LaplaceExpL ((RLine ((M @),i,f)),i);
set MCT = mlt (TC,Tp);
A3:
len (LaplaceExpL ((RLine ((M @),i,f)),i)) = n
by Def7;
A4:
now for j being Nat st 1 <= j & j <= n holds
(mlt (TC,Tp)) . j = (LaplaceExpL ((RLine ((M @),i,f)),i)) . jA5:
Indices (M @) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A6:
dom (LaplaceExpL ((RLine ((M @),i,f)),i)) = Seg n
by A3, FINSEQ_1:def 3;
A7:
width (M @) = n
by MATRIX_0:24;
let j be
Nat;
( 1 <= j & j <= n implies (mlt (TC,Tp)) . j = (LaplaceExpL ((RLine ((M @),i,f)),i)) . j )assume that A8:
1
<= j
and A9:
j <= n
;
(mlt (TC,Tp)) . j = (LaplaceExpL ((RLine ((M @),i,f)),i)) . jA10:
j in Seg n
by A8, A9;
then
Delete (
(M @),
i,
j)
= (Delete (M,j,i)) @
by A2, Th14;
then A11:
Cofactor (
(M @),
i,
j)
= Cofactor (
M,
j,
i)
by MATRIXR2:43;
Indices (Matrix_of_Cofactor M) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then
[j,i] in Indices (Matrix_of_Cofactor M)
by A2, A10, ZFMISC_1:87;
then A12:
(Matrix_of_Cofactor M) * (
j,
i)
= Cofactor (
M,
j,
i)
by Def6;
n = len (Matrix_of_Cofactor M)
by MATRIX_0:24;
then
dom (Matrix_of_Cofactor M) = Seg n
by FINSEQ_1:def 3;
then A13:
(Col ((Matrix_of_Cofactor M),i)) . j = (Matrix_of_Cofactor M) * (
j,
i)
by A10, MATRIX_0:def 8;
A14:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then
[i,j] in Indices M
by A2, A10, ZFMISC_1:87;
then
(RLine ((M @),i,f)) * (
i,
j)
= f . j
by A1, A7, A14, A5, MATRIX11:def 3;
then A15:
(mlt (TC,Tp)) . j = (Cofactor (M,j,i)) * ((RLine ((M @),i,f)) * (i,j))
by A10, A13, A12, FVSUM_1:61;
Cofactor (
(RLine ((M @),i,f)),
i,
j)
= Cofactor (
(M @),
i,
j)
by A2, A10, Th15;
hence
(mlt (TC,Tp)) . j = (LaplaceExpL ((RLine ((M @),i,f)),i)) . j
by A10, A11, A6, A15, Def7;
verum end;
len (mlt (TC,Tp)) = n
by CARD_1:def 7;
hence
mlt ((Col ((Matrix_of_Cofactor M),i)),f) = LaplaceExpL ((RLine ((M @),i,f)),i)
by A3, A4; verum