let K be Field; :: thesis: for A1, B1, A2, B2 being Matrix of K st width A1 = len B1 & width A2 = len B2 holds
(block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K)) = block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)
let A1, B1, A2, B2 be Matrix of K; :: thesis: ( width A1 = len B1 & width A2 = len B2 implies (block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K)) = block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K) )
assume that
A1: width A1 = len B1 and
A2: width A2 = len B2 ; :: thesis: (block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K)) = block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)
A3: width (A1 * B1) = width B1 by A1, MATRIX_3:def 4;
set b12 = <*B1,B2*>;
set a12 = <*A1,A2*>;
set b2 = <*B2*>;
set b1 = <*B1*>;
set a2 = <*A2*>;
set a1 = <*A1*>;
set ab = <*A1,A2*> (#) <*B1,B2*>;
A4: Len <*B1,B2*> = (Len <*B1*>) ^ (Len <*B2*>) by Th14;
set bB = block_diagonal <*B1,B2*>,(0. K);
set bA = block_diagonal <*A1,A2*>,(0. K);
A5: Sum (Width <*A1,A2*>) = width (block_diagonal <*A1,A2*>,(0. K)) by Def5;
A6: Sum (Len <*B1,B2*>) = len (block_diagonal <*B1,B2*>,(0. K)) by Def5;
A7: Width <*A1*> = <*(width A1)*> by Th19;
set bAbB = (block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K));
set bAB = block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K);
A8: Sum (Len (<*A1,A2*> (#) <*B1,B2*>)) = len (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) by Def5;
A9: Sum (Width (<*A1,A2*> (#) <*B1,B2*>)) = width (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) by Def5;
A10: Sum (Len <*A1,A2*>) = (len A1) + (len A2) by Th16;
A11: Sum (Width <*B1,B2*>) = (width B1) + (width B2) by Th20;
A12: len (A2 * B2) = len A2 by A2, MATRIX_3:def 4;
A13: <*A1,A2*> (#) <*B1,B2*> = <*(A1 * B1),(A2 * B2)*> by Th77;
A14: Width <*A2*> = <*(width A2)*> by Th19;
A15: Len <*B2*> = <*(len B2)*> by Th15;
A16: Len <*B1*> = <*(len B1)*> by Th15;
A17: Width <*A1,A2*> = (Width <*A1*>) ^ (Width <*A2*>) by Th18;
then A18: Len (<*A1,A2*> (#) <*B1,B2*>) = Len <*A1,A2*> by A1, A2, A4, A7, A14, A16, A15, Th73;
A19: Width (<*A1,A2*> (#) <*B1,B2*>) = Width <*B1,B2*> by A1, A2, A17, A4, A7, A14, A16, A15, Th73;
Sum (Len <*A1,A2*>) = len (block_diagonal <*A1,A2*>,(0. K)) by Def5;
then A20: len ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) = Sum (Len <*A1,A2*>) by A1, A2, A17, A4, A7, A14, A16, A15, A5, A6, MATRIX_3:def 4;
A21: len (A1 * B1) = len A1 by A1, MATRIX_3:def 4;
Sum (Width <*B1,B2*>) = width (block_diagonal <*B1,B2*>,(0. K)) by Def5;
then A22: width ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) = Sum (Width <*B1,B2*>) by A1, A2, A17, A4, A7, A14, A16, A15, A5, A6, MATRIX_3:def 4;
A23: width (A2 * B2) = width B2 by A2, MATRIX_3:def 4;
A24: Indices (A1 * B1) = [:(Seg (len (A1 * B1))),(Seg (width (A1 * B1))):] by FINSEQ_1:def 3
.= [:(dom A1),(Seg (width B1)):] by A3, A21, FINSEQ_1:def 3 ;

now

A25: dom (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) = Seg (len (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K))) by FINSEQ_1:def 3;
let i, j be Nat; :: thesis: ( [i,j] in Indices (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) implies (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j = ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j )
assume A26: [i,j] in Indices (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) ; :: thesis: (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j = ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j
A27: j in Seg (width (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K))) by A26, ZFMISC_1:106;
A28: i in dom (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) by A26, ZFMISC_1:106;
then A29: 1 <= i by A25, FINSEQ_1:3;
Indices (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) = [:(Seg (len (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)))),(Seg (width (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)))):] by FINSEQ_1:def 3
.= Indices ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) by A8, A9, A20, A22, A18, A19, FINSEQ_1:def 3 ;
then A30: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (Line (block_diagonal <*A1,A2*>,(0. K)),i) "*" (Col (block_diagonal <*B1,B2*>,(0. K)),j) by A1, A2, A17, A4, A7, A14, A16, A15, A5, A6, A26, MATRIX_3:def 4
.= Sum (mlt (Line (block_diagonal <*A1,A2*>,(0. K)),i),(Col (block_diagonal <*B1,B2*>,(0. K)),j)) ;
A31: 1 <= j by A27, FINSEQ_1:3;

now

per cases ( i <= len A1 or i > len A1 ) ;

suppose A32: i <= len A1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then A33: i in dom (A1 * B1) by A21, A29, FINSEQ_3:27;
A34: i in dom A1 by A29, A32, FINSEQ_3:27;
then A35: Line (block_diagonal <*A1,A2*>,(0. K)),i = (Line A1,i) ^ ((width A2) |-> (0. K)) by Th23;

now

per cases ( j <= width B1 or j > width B1 ) ;

suppose j <= width B1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then A36: j in Seg (width B1) by A31, FINSEQ_1:3;
then A37: [i,j] in Indices (A1 * B1) by A24, A34, ZFMISC_1:106;
A38: dom (Line (A1 * B1),i) = Seg (width B1) by A3, FINSEQ_2:144;
Col (block_diagonal <*B1,B2*>,(0. K)),j = (Col B1,j) ^ ((len B2) |-> (0. K)) by A36, Th24;
hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (Sum (mlt (Line A1,i),(Col B1,j))) + (Sum (mlt ((width A2) |-> (0. K)),((len B2) |-> (0. K)))) by A1, A2, A30, A35, Lm9
.= (Sum (mlt (Line A1,i),(Col B1,j))) + (Sum ((0. K) * ((width A2) |-> (0. K)))) by A2, FVSUM_1:80
.= (Sum (mlt (Line A1,i),(Col B1,j))) + ((0. K) * (Sum ((width A2) |-> (0. K)))) by FVSUM_1:92
.= (Sum (mlt (Line A1,i),(Col B1,j))) + (0. K) by VECTSP_1:36
.= (Line A1,i) "*" (Col B1,j) by RLVECT_1:def 7
.= (A1 * B1) * i,j by A1, A37, MATRIX_3:def 4
.= (Line (A1 * B1),i) . j by A3, A36, MATRIX_1:def 8
.= ((Line (A1 * B1),i) ^ ((width (A2 * B2)) |-> (0. K))) . j by A36, A38, FINSEQ_1:def 7
.= (Line (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)),i) . j by A13, A33, Th23
.= (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j by A27, MATRIX_1:def 8 ;
:: thesis: verum

end;

suppose A39: j > width B1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then reconsider J = j - (width B1) as Element of NAT by NAT_1:21;
A40: j = J + (width B1) ;
A41: len (Line (A1 * B1),i) = width B1 by A3, FINSEQ_1:def 18;
A42: dom ((width (A2 * B2)) |-> (0. K)) = Seg (width B2) by A23, FINSEQ_2:144;
J <> 0 by A39;
then A43: J in Seg (width B2) by A9, A19, A11, A27, A40, FINSEQ_1:82;
then Col (block_diagonal <*B1,B2*>,(0. K)),(J + (width B1)) = ((len B1) |-> (0. K)) ^ (Col B2,J) by Th24;
hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (Sum (mlt (Line A1,i),((len B1) |-> (0. K)))) + (Sum (mlt ((width A2) |-> (0. K)),(Col B2,J))) by A1, A2, A30, A35, Lm9
.= (Sum (mlt (Line A1,i),((len B1) |-> (0. K)))) + (Sum ((0. K) * (Col B2,J))) by A2, FVSUM_1:80
.= (Sum ((0. K) * (Line A1,i))) + (Sum ((0. K) * (Col B2,J))) by A1, FVSUM_1:80
.= (Sum ((0. K) * (Line A1,i))) + ((0. K) * (Sum (Col B2,J))) by FVSUM_1:92
.= ((0. K) * (Sum (Line A1,i))) + ((0. K) * (Sum (Col B2,J))) by FVSUM_1:92
.= ((0. K) * (Sum (Line A1,i))) + (0. K) by VECTSP_1:36
.= (0. K) + (0. K) by VECTSP_1:36
.= 0. K by RLVECT_1:def 7
.= ((width (A2 * B2)) |-> (0. K)) . J by A23, A43, FINSEQ_2:71
.= ((Line (A1 * B1),i) ^ ((width (A2 * B2)) |-> (0. K))) . (J + (width (A1 * B1))) by A3, A43, A41, A42, FINSEQ_1:def 7
.= (Line (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)),i) . j by A13, A3, A33, Th23
.= (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j by A27, MATRIX_1:def 8 ;
:: thesis: verum

end;

end;

end;

hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j ; :: thesis: verum

end;

suppose A44: i > len A1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then reconsider I = i - (len A1) as Element of NAT by NAT_1:21;
A45: i = I + (len A1) ;
A46: dom A2 = dom (A2 * B2) by A12, FINSEQ_3:31;
I <> 0 by A44;
then I in Seg (len A2) by A8, A18, A10, A28, A25, A45, FINSEQ_1:82;
then A47: I in dom A2 by FINSEQ_1:def 3;
then A48: Line (block_diagonal <*A1,A2*>,(0. K)),(I + (len A1)) = ((width A1) |-> (0. K)) ^ (Line A2,I) by Th23;

now

per cases ( j <= width B1 or j > width B1 ) ;

suppose A49: j <= width B1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

A50: dom ((width (A1 * B1)) |-> (0. K)) = Seg (width B1) by A3, FINSEQ_2:144;
A51: j in Seg (width B1) by A31, A49, FINSEQ_1:3;
then Col (block_diagonal <*B1,B2*>,(0. K)),j = (Col B1,j) ^ ((len B2) |-> (0. K)) by Th24;
hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (Sum (mlt ((width A1) |-> (0. K)),(Col B1,j))) + (Sum (mlt (Line A2,I),((len B2) |-> (0. K)))) by A1, A2, A30, A48, Lm9
.= (Sum (mlt ((width A1) |-> (0. K)),(Col B1,j))) + (Sum ((0. K) * (Line A2,I))) by A2, FVSUM_1:80
.= (Sum ((0. K) * (Col B1,j))) + (Sum ((0. K) * (Line A2,I))) by A1, FVSUM_1:80
.= (Sum ((0. K) * (Col B1,j))) + ((0. K) * (Sum (Line A2,I))) by FVSUM_1:92
.= ((0. K) * (Sum (Col B1,j))) + ((0. K) * (Sum (Line A2,I))) by FVSUM_1:92
.= ((0. K) * (Sum (Col B1,j))) + (0. K) by VECTSP_1:36
.= (0. K) + (0. K) by VECTSP_1:36
.= 0. K by RLVECT_1:def 7
.= ((width (A1 * B1)) |-> (0. K)) . j by A3, A51, FINSEQ_2:71
.= (((width (A1 * B1)) |-> (0. K)) ^ (Line (A2 * B2),I)) . j by A51, A50, FINSEQ_1:def 7
.= (Line (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)),(I + (len A1))) . j by A13, A21, A47, A46, Th23
.= (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j by A27, MATRIX_1:def 8 ;
:: thesis: verum

end;

suppose A52: j > width B1 ; :: thesis: ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j

then reconsider J = j - (width B1) as Element of NAT by NAT_1:21;
A53: j = J + (width B1) ;
J <> 0 by A52;
then A54: J in Seg (width B2) by A9, A19, A11, A27, A53, FINSEQ_1:82;
then A55: [I,J] in Indices (A2 * B2) by A23, A47, A46, ZFMISC_1:106;
A56: len ((width (A1 * B1)) |-> (0. K)) = width B1 by A3, FINSEQ_1:def 18;
A57: dom (Line (A2 * B2),I) = Seg (width B2) by A23, FINSEQ_2:144;
Col (block_diagonal <*B1,B2*>,(0. K)),(J + (width B1)) = ((len B1) |-> (0. K)) ^ (Col B2,J) by A54, Th24;
hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (Sum (mlt ((width A1) |-> (0. K)),((len B1) |-> (0. K)))) + (Sum (mlt (Line A2,I),(Col B2,J))) by A1, A2, A30, A48, Lm9
.= (Sum ((0. K) * ((width A1) |-> (0. K)))) + (Sum (mlt (Line A2,I),(Col B2,J))) by A1, FVSUM_1:80
.= ((0. K) * (Sum ((width A1) |-> (0. K)))) + (Sum (mlt (Line A2,I),(Col B2,J))) by FVSUM_1:92
.= (0. K) + (Sum (mlt (Line A2,I),(Col B2,J))) by VECTSP_1:36
.= (Line A2,I) "*" (Col B2,J) by RLVECT_1:def 7
.= (A2 * B2) * I,J by A2, A55, MATRIX_3:def 4
.= (Line (A2 * B2),I) . J by A23, A54, MATRIX_1:def 8
.= (((width (A1 * B1)) |-> (0. K)) ^ (Line (A2 * B2),I)) . (J + (width B1)) by A54, A57, A56, FINSEQ_1:def 7
.= (Line (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)),(I + (len A1))) . j by A13, A21, A47, A46, Th23
.= (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j by A27, MATRIX_1:def 8 ;
:: thesis: verum

end;

end;

end;

hence ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j = (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j ; :: thesis: verum

end;

end;

end;

hence (block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K)) * i,j = ((block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K))) * i,j ; :: thesis: verum

end;

hence (block_diagonal <*A1,A2*>,(0. K)) * (block_diagonal <*B1,B2*>,(0. K)) = block_diagonal (<*A1,A2*> (#) <*B1,B2*>),(0. K) by A8, A9, A20, A22, A18, A19, MATRIX_1:21; :: thesis: verum