let i, j be Nat; for K being Field holds block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K)) = 1. (K,(i + j))
let K be Field; block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K)) = 1. (K,(i + j))
set I = 1. (K,i);
set J = 1. (K,j);
set B = block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K));
A1:
len (1. (K,i)) = i
by MATRIX_0:24;
A2:
Sum (Len <*(1. (K,j))*>) = len (1. (K,j))
by Lm4;
A3:
len (1. (K,j)) = j
by MATRIX_0:24;
then A4:
Indices (block_diagonal (<*(1. (K,j))*>,(0. K))) = [:(Seg j),(Seg j):]
by A2, MATRIX_0:24;
Sum (Len <*(1. (K,i)),(1. (K,j))*>) = (len (1. (K,i))) + (len (1. (K,j)))
by Th16;
then reconsider B = block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K)) as Matrix of i + j,K by A1, A3;
A5:
Indices B = [:(Seg (i + j)),(Seg (i + j)):]
by MATRIX_0:24;
A6:
Indices (1. (K,j)) = [:(Seg j),(Seg j):]
by MATRIX_0:24;
A7:
width (1. (K,i)) = i
by MATRIX_0:24;
A8:
Indices (1. (K,i)) = [:(Seg i),(Seg i):]
by MATRIX_0:24;
A9:
Sum (Width <*(1. (K,i))*>) = width (1. (K,i))
by Lm5;
A10:
Sum (Len <*(1. (K,i))*>) = len (1. (K,i))
by Lm4;
then A11:
Indices (block_diagonal (<*(1. (K,i))*>,(0. K))) = [:(Seg i),(Seg i):]
by A1, MATRIX_0:24;
A12:
now for n, m being Nat st [n,m] in Indices B & n <> m holds
B * (n,m) = 0. Klet n,
m be
Nat;
( [n,m] in Indices B & n <> m implies B * (n,m) = 0. K )assume that A13:
[n,m] in Indices B
and A14:
n <> m
;
B * (n,m) = 0. K
m in Seg (i + j)
by A5, A13, ZFMISC_1:87;
then A15:
m >= 1
by FINSEQ_1:1;
n in Seg (i + j)
by A5, A13, ZFMISC_1:87;
then A16:
n >= 1
by FINSEQ_1:1;
now B * (n,m) = 0. Kper cases
( ( n <= i & m <= i ) or ( n > i & m > i ) or ( n <= i & m > i ) or ( n > i & m <= i ) )
;
suppose A17:
(
n <= i &
m <= i )
;
B * (n,m) = 0. Kthen A18:
m in Seg i
by A15;
n in Seg i
by A16, A17;
then A19:
[n,m] in [:(Seg i),(Seg i):]
by A18, ZFMISC_1:87;
hence B * (
n,
m) =
(block_diagonal (<*(1. (K,i))*>,(0. K))) * (
n,
m)
by A2, A11, Th26
.=
(1. (K,i)) * (
n,
m)
by Th34
.=
0. K
by A8, A14, A19, MATRIX_1:def 3
;
verum end; suppose A20:
(
n > i &
m > i )
;
B * (n,m) = 0. Kthen A21:
m - i <> 0
;
n -' i = n - i
by A20, XREAL_1:233;
then A22:
n = (n -' i) + i
;
m -' i = m - i
by A20, XREAL_1:233;
then A23:
m = (m -' i) + i
;
n - i <> 0
by A20;
then A24:
[(n -' i),(m -' i)] in [:(Seg j),(Seg j):]
by A10, A9, A1, A7, A4, A13, A21, A22, A23, Th27;
hence B * (
n,
m) =
(block_diagonal (<*(1. (K,j))*>,(0. K))) * (
(n -' i),
(m -' i))
by A10, A9, A1, A7, A4, A22, A23, Th28
.=
(1. (K,j)) * (
(n -' i),
(m -' i))
by Th34
.=
0. K
by A6, A14, A22, A23, A24, MATRIX_1:def 3
;
verum end; hence
B * (
n,
m)
= 0. K
;
verum end;
now for n being Nat st [n,n] in Indices B holds
B * (n,n) = 1_ Klet n be
Nat;
( [n,n] in Indices B implies B * (n,n) = 1_ K )assume A25:
[n,n] in Indices B
;
B * (n,n) = 1_ K
n in Seg (i + j)
by A5, A25, ZFMISC_1:87;
then A26:
n >= 1
by FINSEQ_1:1;
now B * (n,n) = 1_ Kper cases
( n <= i or n > i )
;
suppose
n <= i
;
B * (n,n) = 1_ Kthen
n in Seg i
by A26;
then A27:
[n,n] in [:(Seg i),(Seg i):]
by ZFMISC_1:87;
hence B * (
n,
n) =
(block_diagonal (<*(1. (K,i))*>,(0. K))) * (
n,
n)
by A2, A11, Th26
.=
(1. (K,i)) * (
n,
n)
by Th34
.=
1_ K
by A8, A27, MATRIX_1:def 3
;
verum end; suppose A28:
n > i
;
B * (n,n) = 1_ Kthen
n -' i = n - i
by XREAL_1:233;
then A29:
n = (n -' i) + i
;
n - i <> 0
by A28;
then A30:
[(n -' i),(n -' i)] in [:(Seg j),(Seg j):]
by A10, A9, A1, A7, A4, A25, A29, Th27;
hence B * (
n,
n) =
(block_diagonal (<*(1. (K,j))*>,(0. K))) * (
(n -' i),
(n -' i))
by A10, A9, A1, A7, A4, A29, Th28
.=
(1. (K,j)) * (
(n -' i),
(n -' i))
by Th34
.=
1_ K
by A6, A30, MATRIX_1:def 3
;
verum end; hence
B * (
n,
n)
= 1_ K
;
verum end;
hence
block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K)) = 1. (K,(i + j))
by A12, MATRIX_1:def 3; verum