let m, n 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: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A2: 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 A3: n = i + 1 ; :: thesis: 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 12;
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_0:24;
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:8;
A9: len N = n by MATRIX_0:24;
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:92;
A11: len N1 = m by MATRIX_0:24;
then A12: len ((len N1) |-> (0. K)) = m by CARD_1:def 7;
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:59, NAT_1:11;
A16: width (block_diagonal (<*N,N1*>,(0. K))) = Sum (Len <*N,N1*>) by MATRIX_0:24;
A17: now :: thesis: for j being Nat st 1 <= j & j <= n holds
((LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) | n) . j = ((Det N1) * L1) . j
A18: i = n -' 1 by A3, NAT_D:34;
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 that
A19: 1 <= j and
A20: j <= n ; :: thesis: ((LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) | n) . j = ((Det N1) * L1) . j
A21: len (Delete (N,1,j)) = n -' 1 by MATRIX_0:def 2;
A22: j in dom ((LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) | n) by A15, A19, A20, FINSEQ_3:25;
then j in (dom (LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1))) /\ (Seg n) by RELAT_1:61;
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:25;
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:124;
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 3;
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_0:def 7
.= ((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_0:def 7 ;
thus ((LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) | n) . j = (LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) . j by A22, FUNCT_1:47
.= (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 3
.= ((Det N1) * L1) . j by A22, A27, A24, FVSUM_1:51 ; :: thesis: 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 1;
A33: width N1 = m by MATRIX_0:24;
now :: thesis: for i being Nat st 1 <= i & i <= m holds
((LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) /^ n) . i = ((len N1) |-> (0. K)) . i
A34: len (Line (N,1)) = n by A6, CARD_1:def 7;
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 that
A35: 1 <= i and
A36: i <= m ; :: thesis: ((LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) /^ n) . i = ((len N1) |-> (0. K)) . i
A37: i in Seg m by A35, A36;
A38: i in dom ((len N1) |-> (0. K)) by A12, A35, A36, FINSEQ_3:25;
A39: i in dom ((LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) /^ n) by A32, A35, A36, FINSEQ_3:25;
then A40: n + i in dom (LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) by FINSEQ_5:26;
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_0:def 7
.= ((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:57 ;
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 6
.= (LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) /. (i + n) by A39, FINSEQ_5:27
.= (LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) . (i + n) by A40, PARTFUN1:def 6
.= ((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
.= ((len N1) |-> (0. K)) . i by A11, A37, FINSEQ_2:57 ; :: thesis: verum
end;
then A42: (LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) /^ n = (len N1) |-> (0. K) by A32, A12;
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;
then Sum (LaplaceExpL ((block_diagonal (<*N,N1*>,(0. K))),1)) = (Sum ((Det N1) * L1)) + (Sum ((len N1) |-> (0. K))) by A42, A8, RLVECT_1:41
.= (Sum ((Det N1) * L1)) + (Sum ((len N1) |-> ((0. K) * (0. K))))
.= (Sum ((Det N1) * L1)) + (Sum ((0. K) * ((len N1) |-> (0. K)))) by FVSUM_1:53
.= ((Det N1) * (Sum L1)) + (Sum ((0. K) * ((len N1) |-> (0. K)))) by FVSUM_1:73
.= ((Det N1) * (Sum L1)) + ((0. K) * (Sum ((len N1) |-> (0. K)))) by FVSUM_1:73
.= ((Det N1) * (Sum L1)) + (0. K)
.= (Det N1) * (Sum L1) by RLVECT_1:def 4
.= (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; :: thesis: verum
end;
A43: 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 A44: n = 0 ; :: thesis: Det (block_diagonal (<*N,N1*>,(0. K))) = (Det N) * (Det N1)
A45: len N = n by MATRIX_0:def 2;
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_0:def 2;
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
.= (Det N) * (Det N1) by A44, MATRIXR2:41 ;
:: thesis: 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) ; :: thesis: verum