let i, j be Nat; :: thesis: for K being Field holds block_diagonal <*(1. K,i),(1. K,j)*>,(0. K) = 1. K,(i + j)
let K be Field; :: thesis: 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_1:25;
A2: Sum (Len <*(1. K,j)*>) = len (1. K,j) by Lm4;
A3: len (1. K,j) = j by MATRIX_1:25;
then A4: Indices (block_diagonal <*(1. K,j)*>,(0. K)) = [:(Seg j),(Seg j):] by A2, MATRIX_1:25;
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_1:25;
A6: Indices (1. K,j) = [:(Seg j),(Seg j):] by MATRIX_1:25;
A7: width (1. K,i) = i by MATRIX_1:25;
A8: Indices (1. K,i) = [:(Seg i),(Seg i):] by MATRIX_1:25;
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_1:25;

A12: now

let n, m be Nat; :: thesis: ( [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 ; :: thesis: B * n,m = 0. K
A15: m in Seg (i + j) by A5, A13, ZFMISC_1:106;
then A16: m >= 1 by FINSEQ_1:3;
A17: n in Seg (i + j) by A5, A13, ZFMISC_1:106;
then A18: n >= 1 by FINSEQ_1:3;

now

per cases ( ( n <= i & m <= i ) or ( n > i & m > i ) or ( n <= i & m > i ) or ( n > i & m <= i ) ) ;

suppose A19: ( n <= i & m <= i ) ; :: thesis: B * n,m = 0. K

then A20: m in Seg i by A15, A16;
n in Seg i by A17, A18, A19;
then A21: [n,m] in [:(Seg i),(Seg i):] by A20, ZFMISC_1:106;
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, A21, MATRIX_1:def 12 ;
:: thesis: verum

end;

suppose A22: ( n > i & m > i ) ; :: thesis: B * n,m = 0. K

then A23: m - i <> 0 ;
n -' i = n - i by A22, XREAL_1:235;
then A24: n = (n -' i) + i ;
m -' i = m - i by A22, XREAL_1:235;
then A25: m = (m -' i) + i ;
n - i <> 0 by A22;
then A26: [(n -' i),(m -' i)] in [:(Seg j),(Seg j):] by A10, A9, A1, A7, A4, A13, A23, A24, A25, Th27;
hence B * n,m = (block_diagonal <*(1. K,j)*>,(0. K)) * (n -' i),(m -' i) by A10, A9, A1, A7, A4, A24, A25, Th28
.= (1. K,j) * (n -' i),(m -' i) by Th34
.= 0. K by A6, A14, A24, A25, A26, MATRIX_1:def 12 ;
:: thesis: verum

end;

suppose ( ( n <= i & m > i ) or ( n > i & m <= i ) ) ; :: thesis: B * n,m = 0. K

hence B * n,m = 0. K by A10, A9, A2, A1, A7, A13, Th29; :: thesis: verum

end;

end;

end;

hence B * n,m = 0. K ; :: thesis: verum

end;

now

let n be Nat; :: thesis: ( [n,n] in Indices B implies B * n,n = 1_ K )
assume A27: [n,n] in Indices B ; :: thesis: B * n,n = 1_ K
A28: n in Seg (i + j) by A5, A27, ZFMISC_1:106;
then A29: n >= 1 by FINSEQ_1:3;

now

per cases ( n <= i or n > i ) ;

suppose n <= i ; :: thesis: B * n,n = 1_ K

then n in Seg i by A28, A29;
then A30: [n,n] in [:(Seg i),(Seg i):] by ZFMISC_1:106;
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, A30, MATRIX_1:def 12 ;
:: thesis: verum

end;

suppose A31: n > i ; :: thesis: B * n,n = 1_ K

then n -' i = n - i by XREAL_1:235;
then A32: n = (n -' i) + i ;
n - i <> 0 by A31;
then A33: [(n -' i),(n -' i)] in [:(Seg j),(Seg j):] by A10, A9, A1, A7, A4, A27, A32, Th27;
hence B * n,n = (block_diagonal <*(1. K,j)*>,(0. K)) * (n -' i),(n -' i) by A10, A9, A1, A7, A4, A32, Th28
.= (1. K,j) * (n -' i),(n -' i) by Th34
.= 1_ K by A6, A33, MATRIX_1:def 12 ;
:: thesis: verum

end;

end;

end;

hence B * n,n = 1_ K ; :: thesis: verum

end;

hence block_diagonal <*(1. K,i),(1. K,j)*>,(0. K) = 1. K,(i + j) by A12, MATRIX_1:def 12; :: thesis: verum