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