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: ( Sum (Len <*(1. K,i)*>) = len (1. K,i) & Sum (Width <*(1. K,i)*>) = width (1. K,i) & Sum (Len <*(1. K,j)*>) = len (1. K,j) ) by Lm4, Lm5;
A2: ( Sum (Len <*(1. K,i),(1. K,j)*>) = (len (1. K,i)) + (len (1. K,j)) & len (1. K,i) = i & len (1. K,j) = j & width (1. K,i) = i ) by Th16, MATRIX_1:25;
reconsider B = block_diagonal <*(1. K,i),(1. K,j)*>,(0. K) as Matrix of i + j,K by A2;
A3: ( Indices B = [:(Seg (i + j)),(Seg (i + j)):] & Indices (1. K,j) = [:(Seg j),(Seg j):] & Indices (block_diagonal <*(1. K,i)*>,(0. K)) = [:(Seg i),(Seg i):] & Indices (block_diagonal <*(1. K,j)*>,(0. K)) = [:(Seg j),(Seg j):] & Indices (1. K,i) = [:(Seg i),(Seg i):] ) by A1, A2, MATRIX_1:25;

A4: now

let n be Nat; :: thesis: ( [n,n] in Indices B implies B * n,n = 1_ K )
assume A5: [n,n] in Indices B ; :: thesis: B * n,n = 1_ K
A6: n in Seg (i + j) by A3, A5, ZFMISC_1:106;
then A7: 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 A6, A7;
then A8: [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 A3, Th26
.= (1. K,i) * n,n by Th34
.= 1_ K by A3, A8, MATRIX_1:def 12 ;
:: thesis: verum

end;

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

then ( n -' i = n - i & n - i <> 0 ) by XREAL_1:235;
then A9: ( n -' i > 0 & n = (n -' i) + i ) ;
A10: [(n -' i),(n -' i)] in [:(Seg j),(Seg j):] by A1, A2, A3, A5, A9, Th27;
hence B * n,n = (block_diagonal <*(1. K,j)*>,(0. K)) * (n -' i),(n -' i) by A3, Th28, A1, A2, A9
.= (1. K,j) * (n -' i),(n -' i) by Th34
.= 1_ K by A3, A10, MATRIX_1:def 12 ;
:: thesis: verum

end;

end;

end;

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

end;

now

let n, m be Nat; :: thesis: ( [n,m] in Indices B & n <> m implies B * n,m = 0. K )
assume A11: ( [n,m] in Indices B & n <> m ) ; :: thesis: B * n,m = 0. K
A12: ( n in Seg (i + j) & m in Seg (i + j) ) by A3, A11, ZFMISC_1:106;
then A13: ( n >= 1 & m >= 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 ( n <= i & m <= i ) ; :: thesis: B * n,m = 0. K

then ( n in Seg i & m in Seg i ) by A12, A13;
then A14: [n,m] in [:(Seg i),(Seg i):] by ZFMISC_1:106;
hence B * n,m = (block_diagonal <*(1. K,i)*>,(0. K)) * n,m by A3, Th26
.= (1. K,i) * n,m by Th34
.= 0. K by A3, A11, A14, MATRIX_1:def 12 ;
:: thesis: verum

end;

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

then ( n -' i = n - i & n - i <> 0 & m -' i = m - i & m - i <> 0 ) by XREAL_1:235;
then A15: ( n -' i > 0 & n = (n -' i) + i & m -' i > 0 & m = (m -' i) + i ) ;
then A16: [(n -' i),(m -' i)] in [:(Seg j),(Seg j):] by A1, A2, A3, A11, Th27;
hence B * n,m = (block_diagonal <*(1. K,j)*>,(0. K)) * (n -' i),(m -' i) by A3, Th28, A1, A2, A15
.= (1. K,j) * (n -' i),(m -' i) by Th34
.= 0. K by A3, A11, A15, A16, 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 A1, A2, A11, Th29; :: thesis: verum

end;

end;

end;

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

end;

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