let i, j be Nat; for D being non empty set
for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal (F1,d)) holds
(block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)
let D be non empty set ; for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal (F1,d)) holds
(block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)
let d be Element of D; for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal (F1,d)) holds
(block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)
let F1, F2 be FinSequence_of_Matrix of D; ( [i,j] in Indices (block_diagonal (F1,d)) implies (block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j) )
set B1 = block_diagonal (F1,d);
set L1 = Len F1;
set W1 = Width F1;
set L2 = Len F2;
set W2 = Width F2;
set F12 = F1 ^ F2;
set L = Len (F1 ^ F2);
set W = Width (F1 ^ F2);
set B12 = block_diagonal ((F1 ^ F2),d);
A1:
len F1 = len (Width F1)
by CARD_1:def 7;
A2:
len (block_diagonal (F1,d)) = Sum (Len F1)
by Def5;
assume A3:
[i,j] in Indices (block_diagonal (F1,d))
; (block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)
then
i in dom (block_diagonal (F1,d))
by ZFMISC_1:87;
then A4:
i in Seg (len (block_diagonal (F1,d)))
by FINSEQ_1:def 3;
then A5:
min ((Len F1),i) in dom (Len F1)
by A2, Def1;
then A6:
min ((Len F1),i) <= len (Len F1)
by FINSEQ_3:25;
(Len F1) ^ (Len F2) = Len (F1 ^ F2)
by Th14;
then A7:
min ((Len F1),i) = min ((Len (F1 ^ F2)),i)
by A4, A2, Th8;
A8:
dom (Len F1) = dom F1
by Def3;
A9:
(Width F1) ^ (Width F2) = Width (F1 ^ F2)
by Th18;
A10:
(Len F1) ^ (Len F2) = Len (F1 ^ F2)
by Th14;
A11:
Indices (block_diagonal (F1,d)) is Subset of (Indices (block_diagonal ((F1 ^ F2),d)))
by Th25;
A12:
len (Len F1) = len F1
by CARD_1:def 7;
then A13:
((Width F1) ^ (Width F2)) | (min ((Len (F1 ^ F2)),i)) = (Width F1) | (min ((Len F1),i))
by A7, A6, A1, FINSEQ_5:22;
A14:
(min ((Len F1),i)) -' 1 <= min ((Len F1),i)
by NAT_D:35;
then A15:
((Len F1) ^ (Len F2)) | ((min ((Len (F1 ^ F2)),i)) -' 1) = (Len F1) | ((min ((Len F1),i)) -' 1)
by A7, A6, FINSEQ_5:22, XXREAL_0:2;
A16:
((Width F1) ^ (Width F2)) | ((min ((Len (F1 ^ F2)),i)) -' 1) = (Width F1) | ((min ((Len F1),i)) -' 1)
by A7, A6, A14, A12, A1, FINSEQ_5:22, XXREAL_0:2;
per cases
( j <= Sum ((Width F1) | ((min ((Len F1),i)) -' 1)) or j > Sum ((Width F1) | (min ((Len F1),i))) or ( j > Sum ((Width F1) | ((min ((Len F1),i)) -' 1)) & j <= Sum ((Width F1) | (min ((Len F1),i))) ) )
;
suppose A17:
(
j <= Sum ((Width F1) | ((min ((Len F1),i)) -' 1)) or
j > Sum ((Width F1) | (min ((Len F1),i))) )
;
(block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)then
(block_diagonal (F1,d)) * (
i,
j)
= d
by A3, Def5;
hence
(block_diagonal (F1,d)) * (
i,
j)
= (block_diagonal ((F1 ^ F2),d)) * (
i,
j)
by A3, A11, A13, A16, A9, A17, Def5;
verum end; suppose A18:
(
j > Sum ((Width F1) | ((min ((Len F1),i)) -' 1)) &
j <= Sum ((Width F1) | (min ((Len F1),i))) )
;
(block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)then A19:
(block_diagonal (F1,d)) * (
i,
j)
= (F1 . (min ((Len F1),i))) * (
(i -' (Sum ((Len F1) | ((min ((Len F1),i)) -' 1)))),
(j -' (Sum ((Width F1) | ((min ((Len F1),i)) -' 1)))))
by A3, Def5;
(block_diagonal ((F1 ^ F2),d)) * (
i,
j)
= ((F1 ^ F2) . (min ((Len F1),i))) * (
(i -' (Sum ((Len F1) | ((min ((Len F1),i)) -' 1)))),
(j -' (Sum ((Width F1) | ((min ((Len F1),i)) -' 1)))))
by A3, A11, A7, A13, A16, A15, A9, A10, A18, Def5;
hence
(block_diagonal (F1,d)) * (
i,
j)
= (block_diagonal ((F1 ^ F2),d)) * (
i,
j)
by A5, A8, A19, FINSEQ_1:def 7;
verum end;