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:75;
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:73;
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:76;
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:73;
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:75;
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:76;
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 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 ((<*(block_diagonal (F1,d))*> ^ F2),d)) * (i,j)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:87;
then A22:
1
<= i
by A20, FINSEQ_1:1;
j in Seg (width (block_diagonal ((F1 ^ F2),d)))
by A21, ZFMISC_1:87;
then A23:
1
<= j
by FINSEQ_1:1;
now (block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal ((<*(block_diagonal (F1,d))*> ^ F2),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 A24:
(
i <= Sum (Len F1) &
j <= Sum (Width F1) )
;
(block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal ((<*(block_diagonal (F1,d))*> ^ F2),d)) * (i,j)then A25:
i in dom (block_diagonal (F1,d))
by A12, A22, FINSEQ_3:25;
j in Seg (width (block_diagonal (F1,d)))
by A6, A23, A24;
then A26:
[i,j] in Indices (block_diagonal (F1,d))
by A25, ZFMISC_1:87;
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, A26, Th26
;
verum end; suppose A27:
( (
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,j)hence (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, A27, Th29
;
verum end; suppose A28:
(
i > Sum (Len F1) &
j > Sum (Width F1) )
;
(block_diagonal ((F1 ^ F2),d)) * (i,j) = (block_diagonal ((<*(block_diagonal (F1,d))*> ^ F2),d)) * (i,j)then reconsider ii =
i - (Sum (Len F1)),
jj =
j - (Sum (Width F1)) as
Element of
NAT by NAT_1:21;
A29:
jj <> 0
by A28;
A30:
i = ii + (Sum (Len F1))
;
A31:
j = jj + (Sum (Width F1))
;
ii <> 0
by A28;
then A32:
[ii,jj] in Indices (block_diagonal (F2,d))
by A21, A30, A31, A29, Th27;
hence (block_diagonal ((F1 ^ F2),d)) * (
i,
j) =
(block_diagonal (F2,d)) * (
ii,
jj)
by A30, A31, Th28
.=
(block_diagonal ((<*(block_diagonal (F1,d))*> ^ F2),d)) * (
i,
j)
by A17, A13, A4, A11, A30, A31, A32, 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_0:21, RVSUM_1:75; verum