let n, m be Nat; for K being Field
for N being Matrix of n,K
for N1 being Matrix of m,K holds Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)
let K be Field; for N being Matrix of n,K
for N1 being Matrix of m,K holds Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)
let N be Matrix of n,K; for N1 being Matrix of m,K holds Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)
let N1 be Matrix of m,K; Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)
defpred S1[ Nat] means for n, m being Nat
for N being Matrix of n,K
for N1 being Matrix of m,K st n = $1 holds
Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1);
A1:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A2:
S1[
i]
;
S1[i + 1]
set i1 =
i + 1;
let n,
m be
Nat;
for N being Matrix of n,K
for N1 being Matrix of m,K st n = i + 1 holds
Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)let N be
Matrix of
n,
K;
for N1 being Matrix of m,K st n = i + 1 holds
Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)let N1 be
Matrix of
m,
K;
( n = i + 1 implies Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1) )
assume A3:
n = i + 1
;
Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)
1
<= (i + m) + 1
by NAT_1:11;
then A4:
1
in Seg (n + m)
by A3;
1
<= i + 1
by NAT_1:11;
then A5:
1
in Seg n
by A3;
set L0 =
(len N1) |-> (0. K);
reconsider nn =
n as
Element of
NAT by ORDINAL1:def 13;
set D =
Det N1;
set L1 =
LaplaceExpL N,1;
set NN =
<*N,N1*>;
reconsider M =
N as
Matrix of
K ;
set bN =
block_diagonal <*N,N1*>,
(0. K);
set L =
LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1;
A6:
width N = n
by MATRIX_1:25;
set Ln =
(LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) | n;
A7:
len (LaplaceExpL N,1) = n
by LAPLACE:def 7;
set L9n =
(LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) /^ n;
A8:
LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1
= ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) | n) ^ ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) /^ n)
by RFINSEQ:21;
A9:
len N = n
by MATRIX_1:25;
then A10:
dom N = Seg n
by FINSEQ_1:def 3;
reconsider L1 =
LaplaceExpL N,1 as
Element of
nn -tuples_on the
carrier of
K by A7, FINSEQ_2:110;
A11:
len N1 = m
by MATRIX_1:25;
then A12:
len ((len N1) |-> (0. K)) = m
by FINSEQ_1:def 18;
A13:
Sum (Len <*N,N1*>) = (len N) + (len N1)
by Th16;
then A14:
len (LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) = n + m
by A9, A11, LAPLACE:def 7;
then A15:
len ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) | n) = n
by FINSEQ_1:80, NAT_1:11;
A16:
width (block_diagonal <*N,N1*>,(0. K)) = Sum (Len <*N,N1*>)
by MATRIX_1:25;
A17:
now A18:
i = n -' 1
by A3, NAT_D:34;
let j be
Nat;
( 1 <= j & j <= n implies ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) | n) . j = ((Det N1) * L1) . j )assume that A19:
1
<= j
and A20:
j <= n
;
((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) | n) . j = ((Det N1) * L1) . jA21:
len (Delete N,1,j) = n -' 1
by MATRIX_1:def 3;
A22:
j in dom ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) | n)
by A15, A19, A20, FINSEQ_3:27;
then
j in (dom (LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1)) /\ (Seg n)
by RELAT_1:90;
then A23:
j in dom (LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1)
by XBOOLE_0:def 4;
j in dom L1
by A7, A19, A20, FINSEQ_3:27;
then A24:
(N * 1,j) * (Cofactor N,1,j) = L1 . j
by LAPLACE:def 7;
A25:
((i + m) + 1) -' 1
= i + m
by NAT_D:34;
A26:
dom (Line N,1) = Seg n
by A6, FINSEQ_2:144;
A27:
dom ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) | n) = Seg n
by A15, FINSEQ_1:def 3;
A28:
dom (LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) = Seg (n + m)
by A14, FINSEQ_1:def 3;
then A29:
Delete (block_diagonal <*N,N1*>,(0. K)),1,
j =
Deleting (block_diagonal <*N,N1*>,(0. K)),1,
j
by A13, A9, A11, A4, A23, LAPLACE:def 1
.=
block_diagonal (<*(Deleting N,1,j)*> ^ <*N1*>),
(0. K)
by A5, A10, A22, A27, Th47
.=
block_diagonal <*(Delete N,1,j),N1*>,
(0. K)
by A5, A22, A27, LAPLACE:def 1
;
(Minor N,1,j) * (Det N1) =
Det (block_diagonal <*(Delete N,1,j),N1*>,(0. K))
by A2, A3, NAT_D:34
.=
Minor (block_diagonal <*N,N1*>,(0. K)),1,
j
by A3, A13, A9, A11, A29, A18, A25, A21, Th16
;
then A30:
Cofactor (block_diagonal <*N,N1*>,(0. K)),1,
j = (Det N1) * (Cofactor N,1,j)
by GROUP_1:def 4;
A31:
(block_diagonal <*N,N1*>,(0. K)) * 1,
j =
(Line (block_diagonal <*M,N1*>,(0. K)),1) . j
by A16, A13, A9, A11, A23, A28, MATRIX_1:def 8
.=
((Line N,1) ^ ((width N1) |-> (0. K))) . j
by A5, A10, Th23
.=
(Line N,1) . j
by A22, A27, A26, FINSEQ_1:def 7
.=
N * 1,
j
by A6, A22, A27, MATRIX_1:def 8
;
thus ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) | n) . j =
(LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) . j
by A22, FUNCT_1:70
.=
(N * 1,j) * ((Det N1) * (Cofactor N,1,j))
by A23, A30, A31, LAPLACE:def 7
.=
(Det N1) * ((N * 1,j) * (Cofactor N,1,j))
by GROUP_1:def 4
.=
((Det N1) * L1) . j
by A22, A27, A24, FVSUM_1:63
;
verum end;
n <= n + m
by NAT_1:11;
then A32:
len ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) /^ n) = (n + m) - n
by A14, RFINSEQ:def 2;
A33:
width N1 = m
by MATRIX_1:25;
now A34:
len (Line N,1) = n
by A6, FINSEQ_1:def 18;
let i be
Nat;
( 1 <= i & i <= m implies ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) /^ n) . i = ((len N1) |-> (0. K)) . i )assume that A35:
1
<= i
and A36:
i <= m
;
((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) /^ n) . i = ((len N1) |-> (0. K)) . iA37:
i in Seg m
by A35, A36, FINSEQ_1:3;
A38:
i in dom ((len N1) |-> (0. K))
by A12, A35, A36, FINSEQ_3:27;
A39:
i in dom ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) /^ n)
by A32, A35, A36, FINSEQ_3:27;
then A40:
n + i in dom (LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1)
by FINSEQ_5:29;
dom (LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) = Seg (width (block_diagonal <*N,N1*>,(0. K)))
by A16, A13, A9, A11, A14, FINSEQ_1:def 3;
then A41:
(block_diagonal <*N,N1*>,(0. K)) * 1,
(i + n) =
(Line (block_diagonal <*M,N1*>,(0. K)),1) . (i + n)
by A40, MATRIX_1:def 8
.=
((Line N,1) ^ ((len N1) |-> (0. K))) . (i + n)
by A11, A33, A5, A10, Th23
.=
((len N1) |-> (0. K)) . i
by A38, A34, FINSEQ_1:def 7
.=
0. K
by A11, A37, FINSEQ_2:71
;
thus ((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) /^ n) . i =
((LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) /^ n) /. i
by A39, PARTFUN1:def 8
.=
(LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) /. (i + n)
by A39, FINSEQ_5:30
.=
(LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) . (i + n)
by A40, PARTFUN1:def 8
.=
((block_diagonal <*N,N1*>,(0. K)) * 1,(i + n)) * (Cofactor (block_diagonal <*N,N1*>,(0. K)),1,(i + n))
by A40, LAPLACE:def 7
.=
0. K
by A41, VECTSP_1:36
.=
((len N1) |-> (0. K)) . i
by A11, A37, FINSEQ_2:71
;
verum end;
then A42:
(LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) /^ n = (len N1) |-> (0. K)
by A32, A12, FINSEQ_1:18;
len ((Det N1) * L1) = nn
by A7, MATRIXR1:16;
then
(LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) | n = (Det N1) * L1
by A15, A17, FINSEQ_1:18;
then Sum (LaplaceExpL (block_diagonal <*N,N1*>,(0. K)),1) =
(Sum ((Det N1) * L1)) + (Sum ((len N1) |-> (0. K)))
by A42, A8, RLVECT_1:58
.=
(Sum ((Det N1) * L1)) + (Sum ((len N1) |-> ((0. K) * (0. K))))
by VECTSP_1:36
.=
(Sum ((Det N1) * L1)) + (Sum ((0. K) * ((len N1) |-> (0. K))))
by FVSUM_1:66
.=
((Det N1) * (Sum L1)) + (Sum ((0. K) * ((len N1) |-> (0. K))))
by FVSUM_1:92
.=
((Det N1) * (Sum L1)) + ((0. K) * (Sum ((len N1) |-> (0. K))))
by FVSUM_1:92
.=
((Det N1) * (Sum L1)) + (0. K)
by VECTSP_1:36
.=
(Det N1) * (Sum L1)
by RLVECT_1:def 7
.=
(Det N1) * (Det N)
by A5, LAPLACE:25
;
hence
Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)
by A13, A9, A11, A4, LAPLACE:25;
verum
end;
A43:
S1[ 0 ]
proof
let n,
m be
Nat;
for N being Matrix of n,K
for N1 being Matrix of m,K st n = 0 holds
Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)let N be
Matrix of
n,
K;
for N1 being Matrix of m,K st n = 0 holds
Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)let N1 be
Matrix of
m,
K;
( n = 0 implies Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1) )
assume A44:
n = 0
;
Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)
A45:
len N = n
by MATRIX_1:def 3;
then
N = {}
by A44;
then A46:
block_diagonal <*N,N1*>,
(0. K) =
block_diagonal <*N1*>,
(0. K)
by Th40
.=
N1
by Th34
;
len N1 = m
by MATRIX_1:def 3;
then
Sum (Len <*N,N1*>) = 0 + m
by A44, A45, Th16;
hence Det (block_diagonal <*N,N1*>,(0. K)) =
(Det N1) * (1_ K)
by A46, VECTSP_1:def 16
.=
(Det N) * (Det N1)
by A44, MATRIXR2:41
;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A43, A1);
hence
Det (block_diagonal <*N,N1*>,(0. K)) = (Det N) * (Det N1)
; verum