let D be non empty set ; for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D holds block_diagonal ((F1 ^ F2),d) = block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)
let d be Element of D; for F1, F2 being FinSequence_of_Matrix of D holds block_diagonal ((F1 ^ F2),d) = block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)
let F1, F2 be FinSequence_of_Matrix of D; block_diagonal ((F1 ^ F2),d) = block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)
set F12 = F1 ^ F2;
set D1 = block_diagonal (F1,d);
set D2 = block_diagonal (F2,d);
set D12 = block_diagonal ((F1 ^ F2),d);
set FD = F1 ^ <*(block_diagonal (F2,d))*>;
set FD2 = block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d);
set LF1 = Len F1;
set WF1 = Width F1;
set LF2 = Len F2;
set WF2 = Width F2;
set LF = Len (F1 ^ F2);
set WF = Width (F1 ^ F2);
A1:
Len (F1 ^ F2) = (Len F1) ^ (Len F2)
by Th14;
len (block_diagonal ((F1 ^ F2),d)) = Sum (Len (F1 ^ F2))
by Def5;
then A2:
len (block_diagonal ((F1 ^ F2),d)) = (Sum (Len F1)) + (Sum (Len F2))
by A1, RVSUM_1:75;
A3:
Sum (Width <*(block_diagonal (F2,d))*>) = width (block_diagonal (F2,d))
by Lm5;
A4:
Len (F1 ^ <*(block_diagonal (F2,d))*>) = (Len F1) ^ (Len <*(block_diagonal (F2,d))*>)
by Th14;
len (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) = Sum (Len (F1 ^ <*(block_diagonal (F2,d))*>))
by Def5;
then A5:
len (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) = (Sum (Len <*(block_diagonal (F2,d))*>)) + (Sum (Len F1))
by A4, RVSUM_1:75;
A6:
Sum (Len F1) = len (block_diagonal (F1,d))
by Def5;
A7:
Width (F1 ^ F2) = (Width F1) ^ (Width F2)
by Th18;
A8:
Width (F1 ^ <*(block_diagonal (F2,d))*>) = (Width F1) ^ (Width <*(block_diagonal (F2,d))*>)
by Th18;
width (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) = Sum (Width (F1 ^ <*(block_diagonal (F2,d))*>))
by Def5;
then A9:
width (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) = (Sum (Width <*(block_diagonal (F2,d))*>)) + (Sum (Width F1))
by A8, RVSUM_1:75;
A10:
Sum (Width F1) = width (block_diagonal (F1,d))
by Def5;
A11:
len (block_diagonal (F2,d)) = Sum (Len F2)
by Def5;
A12:
width (block_diagonal ((F1 ^ F2),d)) = Sum (Width (F1 ^ F2))
by Def5;
then A13:
width (block_diagonal ((F1 ^ F2),d)) = (Sum (Width F1)) + (Sum (Width F2))
by A7, RVSUM_1:75;
A14:
Sum (Len <*(block_diagonal (F2,d))*>) = len (block_diagonal (F2,d))
by Lm4;
A15:
block_diagonal (<*(block_diagonal (F2,d))*>,d) = block_diagonal (F2,d)
by Th34;
A16:
width (block_diagonal (F2,d)) = Sum (Width F2)
by Def5;
A17: Indices (block_diagonal ((F1 ^ F2),d)) =
[:(Seg (len (block_diagonal ((F1 ^ F2),d)))),(Seg (width (block_diagonal ((F1 ^ F2),d)))):]
by FINSEQ_1:def 3
.=
Indices (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d))
by A2, A13, A11, A16, A5, A9, A14, A3, FINSEQ_1:def 3
;
now for i, j being Nat st [i,j] in Indices (block_diagonal ((F1 ^ F2),d)) holds
(block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (i,j)A18:
dom (block_diagonal ((F1 ^ F2),d)) = Seg (len (block_diagonal ((F1 ^ F2),d)))
by FINSEQ_1:def 3;
let i,
j be
Nat;
( [i,j] in Indices (block_diagonal ((F1 ^ F2),d)) implies (block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (i,j) )assume A19:
[i,j] in Indices (block_diagonal ((F1 ^ F2),d))
;
(block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (i,j)
i in dom (block_diagonal ((F1 ^ F2),d))
by A19, ZFMISC_1:87;
then A20:
1
<= i
by A18, FINSEQ_1:1;
j in Seg (width (block_diagonal ((F1 ^ F2),d)))
by A19, ZFMISC_1:87;
then A21:
1
<= j
by FINSEQ_1:1;
now (block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (i,j)per cases
( ( i <= Sum (Len F1) & j <= Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) or ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j > Sum (Width F1) ) )
;
suppose A22:
(
i <= Sum (Len F1) &
j <= Sum (Width F1) )
;
(block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (i,j)then A23:
i in dom (block_diagonal (F1,d))
by A6, A20, FINSEQ_3:25;
j in Seg (width (block_diagonal (F1,d)))
by A10, A21, A22;
then A24:
[i,j] in Indices (block_diagonal (F1,d))
by A23, ZFMISC_1:87;
hence (block_diagonal ((F1 ^ F2),d)) * (
i,
j) =
(block_diagonal (F1,d)) * (
i,
j)
by Th26
.=
(block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (
i,
j)
by A24, Th26
;
verum end; suppose A26:
(
i > Sum (Len F1) &
j > Sum (Width F1) )
;
(block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (i,j)then reconsider ii =
i - (Sum (Len F1)),
jj =
j - (Sum (Width F1)) as
Element of
NAT by NAT_1:21;
A27:
jj <> 0
by A26;
A28:
i = ii + (Sum (Len F1))
;
A29:
j = jj + (Sum (Width F1))
;
ii <> 0
by A26;
then A30:
[ii,jj] in Indices (block_diagonal (F2,d))
by A19, A28, A29, A27, Th27;
hence (block_diagonal ((F1 ^ F2),d)) * (
i,
j) =
(block_diagonal (F2,d)) * (
ii,
jj)
by A28, A29, Th28
.=
(block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (
i,
j)
by A15, A28, A29, A30, Th28
;
verum end; hence
(block_diagonal ((F1 ^ F2),d)) * (
i,
j)
= (block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)) * (
i,
j)
;
verum end;
hence
block_diagonal ((F1 ^ F2),d) = block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)
by A12, A7, A2, A11, A16, A5, A9, A14, A3, MATRIX_0:21, RVSUM_1:75; verum