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 (<*(block_diagonal F1,d)*> ^ F2),d
let d be Element of D; for F1, F2 being FinSequence_of_Matrix of D holds block_diagonal (F1 ^ F2),d = block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d
let F1, F2 be FinSequence_of_Matrix of D; block_diagonal (F1 ^ F2),d = block_diagonal (<*(block_diagonal F1,d)*> ^ F2),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 DF = <*(block_diagonal F1,d)*> ^ F2;
set DF2 = block_diagonal (<*(block_diagonal F1,d)*> ^ F2),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:105;
A3:
Len <*(block_diagonal F1,d)*> = <*(len (block_diagonal F1,d))*>
by Th15;
then A4:
Sum (Len <*(block_diagonal F1,d)*>) = len (block_diagonal F1,d)
by RVSUM_1:103;
A5:
block_diagonal <*(block_diagonal F1,d)*>,d = block_diagonal F1,d
by Th34;
A6:
Sum (Width F1) = width (block_diagonal F1,d)
by Def5;
A7:
Len (<*(block_diagonal F1,d)*> ^ F2) = (Len <*(block_diagonal F1,d)*>) ^ (Len F2)
by Th14;
A8:
Width (F1 ^ F2) = (Width F1) ^ (Width F2)
by Th18;
len (block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) = Sum (Len (<*(block_diagonal F1,d)*> ^ F2))
by Def5;
then A9:
len (block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) = (len (block_diagonal F1,d)) + (Sum (Len F2))
by A7, A3, RVSUM_1:106;
A10:
Width <*(block_diagonal F1,d)*> = <*(width (block_diagonal F1,d))*>
by Th19;
then A11:
Sum (Width <*(block_diagonal F1,d)*>) = width (block_diagonal F1,d)
by RVSUM_1:103;
A12:
Sum (Len F1) = len (block_diagonal F1,d)
by Def5;
A13:
width (block_diagonal F1,d) = Sum (Width F1)
by Def5;
A14:
width (block_diagonal (F1 ^ F2),d) = Sum (Width (F1 ^ F2))
by Def5;
then A15:
width (block_diagonal (F1 ^ F2),d) = (Sum (Width F1)) + (Sum (Width F2))
by A8, RVSUM_1:105;
A16:
Width (<*(block_diagonal F1,d)*> ^ F2) = (Width <*(block_diagonal F1,d)*>) ^ (Width F2)
by Th18;
A17:
len (block_diagonal F1,d) = Sum (Len F1)
by Def5;
width (block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) = Sum (Width (<*(block_diagonal F1,d)*> ^ F2))
by Def5;
then A18:
width (block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) = (width (block_diagonal F1,d)) + (Sum (Width F2))
by A16, A10, RVSUM_1:106;
A19: 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 (<*(block_diagonal F1,d)*> ^ F2),d)
by A2, A15, A17, A13, A9, A18, FINSEQ_1:def 3
;
now A20:
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 (<*(block_diagonal F1,d)*> ^ F2),d) * i,j )assume A21:
[i,j] in Indices (block_diagonal (F1 ^ F2),d)
;
(block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) * i,j
i in dom (block_diagonal (F1 ^ F2),d)
by A21, ZFMISC_1:106;
then A22:
1
<= i
by A20, FINSEQ_1:3;
A23:
j in Seg (width (block_diagonal (F1 ^ F2),d))
by A21, ZFMISC_1:106;
then A24:
1
<= j
by FINSEQ_1:3;
now 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 A25:
(
i <= Sum (Len F1) &
j <= Sum (Width F1) )
;
(block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) * i,jthen A26:
i in dom (block_diagonal F1,d)
by A12, A22, FINSEQ_3:27;
j in Seg (width (block_diagonal F1,d))
by A6, A23, A24, A25;
then A27:
[i,j] in Indices (block_diagonal F1,d)
by A26, ZFMISC_1:106;
hence (block_diagonal (F1 ^ F2),d) * i,
j =
(block_diagonal F1,d) * i,
j
by Th26
.=
(block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) * i,
j
by A5, A27, Th26
;
verum end; suppose A28:
( (
i > Sum (Len F1) &
j <= Sum (Width F1) ) or (
i <= Sum (Len F1) &
j > Sum (Width F1) ) )
;
(block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) * i,jhence (block_diagonal (F1 ^ F2),d) * i,
j =
d
by A21, Th29
.=
(block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) * i,
j
by A17, A13, A4, A11, A19, A21, A28, Th29
;
verum end; suppose A29:
(
i > Sum (Len F1) &
j > Sum (Width F1) )
;
(block_diagonal (F1 ^ F2),d) * i,j = (block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) * i,jthen reconsider ii =
i - (Sum (Len F1)),
jj =
j - (Sum (Width F1)) as
Element of
NAT by NAT_1:21;
A30:
jj <> 0
by A29;
A31:
i = ii + (Sum (Len F1))
;
A32:
j = jj + (Sum (Width F1))
;
ii <> 0
by A29;
then A33:
[ii,jj] in Indices (block_diagonal F2,d)
by A21, A31, A32, A30, Th27;
hence (block_diagonal (F1 ^ F2),d) * i,
j =
(block_diagonal F2,d) * ii,
jj
by A31, A32, Th28
.=
(block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) * i,
j
by A17, A13, A4, A11, A31, A32, A33, Th28
;
verum end; hence
(block_diagonal (F1 ^ F2),d) * i,
j = (block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d) * i,
j
;
verum end;
hence
block_diagonal (F1 ^ F2),d = block_diagonal (<*(block_diagonal F1,d)*> ^ F2),d
by A14, A8, A2, A17, A13, A9, A18, MATRIX_1:21, RVSUM_1:105; verum