let D be non empty set ; :: thesis: for d being Element of D
for M1, M2 being Matrix of D
for M being Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D holds
( M = block_diagonal <*M1,M2*>,d iff for i being Nat holds
( ( i in dom M1 implies Line M,i = (Line M1,i) ^ ((width M2) |-> d) ) & ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) ) )
let d be Element of D; :: thesis: for M1, M2 being Matrix of D
for M being Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D holds
( M = block_diagonal <*M1,M2*>,d iff for i being Nat holds
( ( i in dom M1 implies Line M,i = (Line M1,i) ^ ((width M2) |-> d) ) & ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) ) )
let M1, M2 be Matrix of D; :: thesis: for M being Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D holds
( M = block_diagonal <*M1,M2*>,d iff for i being Nat holds
( ( i in dom M1 implies Line M,i = (Line M1,i) ^ ((width M2) |-> d) ) & ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) ) )
let M be Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D; :: thesis: ( M = block_diagonal <*M1,M2*>,d iff for i being Nat holds
( ( i in dom M1 implies Line M,i = (Line M1,i) ^ ((width M2) |-> d) ) & ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) ) )
set F1 = <*M1*>;
set F2 = <*M2*>;
set F12 = <*M1,M2*>;
set B = block_diagonal <*M1,M2*>,d;
set L1 = len M1;
set L2 = len M2;
set W1 = width M1;
set W2 = width M2;
A1: Sum <*(width M1)*> = width M1 by RVSUM_1:103;
len (block_diagonal <*M1,M2*>,d) = Sum (Len <*M1,M2*>) by Def5;
then A2: len (block_diagonal <*M1,M2*>,d) = (len M1) + (len M2) by Th16;
A3: len <*M1,M2*> = len (Len <*M1,M2*>) by FINSEQ_1:def 18;
A4: (Len <*M1,M2*>) | 0 = <*> REAL ;
A5: (Width <*M1,M2*>) | 0 = <*> REAL ;
A6: 1 -' 1 = 0 by XREAL_1:234;
A7: width (block_diagonal <*M1,M2*>,d) = Sum (Width <*M1,M2*>) by Def5;
then A8: width (block_diagonal <*M1,M2*>,d) = (width M1) + (width M2) by Th20;
A9: len <*(width M1)*> = 1 by FINSEQ_1:57;
A10: len <*M1*> = 1 by FINSEQ_1:57;
A11: Len <*M1*> = <*(len M1)*> by Th15;
A12: Len <*M1,M2*> = (Len <*M1*>) ^ (Len <*M2*>) by Th14;
then A13: (Len <*M1,M2*>) . 1 = len M1 by A11, FINSEQ_1:58;
A14: len <*(len M1)*> = 1 by FINSEQ_1:57;
then A15: (Len <*M1,M2*>) | 1 = <*(len M1)*> by A12, A11, FINSEQ_5:26;
A16: Width <*M1*> = <*(width M1)*> by Th19;
A17: Sum <*(len M1)*> = len M1 by RVSUM_1:103;
Width <*M1,M2*> = (Width <*M1*>) ^ (Width <*M2*>) by Th18;
then A18: (Width <*M1,M2*>) | 1 = <*(width M1)*> by A16, A9, FINSEQ_5:26;
A19: Len <*M2*> = <*(len M2)*> by Th15;
then A20: len (Len <*M1,M2*>) = 1 + 1 by A12, A11, A14, FINSEQ_2:19;
A21: (Len <*M1,M2*>) . 2 = len M2 by A12, A11, A19, A14, FINSEQ_1:59;
len (Width <*M1,M2*>) = len <*M1,M2*> by FINSEQ_1:def 18;
then A22: (Width <*M1,M2*>) | 2 = Width <*M1,M2*> by A20, A3, FINSEQ_1:79;
A23: dom (Len <*M1,M2*>) = {1,2} by A20, FINSEQ_1:4, FINSEQ_1:def 3;
then A24: 1 in dom (Len <*M1,M2*>) by TARSKI:def 2;
then A25: (Len <*M1,M2*>) /. 1 = (Len <*M1,M2*>) . 1 by PARTFUN1:def 8;
A26: 2 -' 1 = 2 - 1 by XREAL_1:235;
( Sum (Len <*M1,M2*>) = 0 implies Sum (Width <*M1,M2*>) = 0 ) by Th13;
then A27: width M = (width M1) + (width M2) by A7, A8, MATRIX13:1;
A28: 2 in dom (Len <*M1,M2*>) by A23, TARSKI:def 2;
then A29: (Len <*M1,M2*>) /. 2 = (Len <*M1,M2*>) . 2 by PARTFUN1:def 8;

hereby :: thesis: ( ( for i being Nat holds
( ( i in dom M1 implies Line M,i = (Line M1,i) ^ ((width M2) |-> d) ) & ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) ) ) implies M = block_diagonal <*M1,M2*>,d )

assume A30: M = block_diagonal <*M1,M2*>,d ; :: thesis: for i being Nat holds
( ( i in dom M1 implies Line M,i = (Line M1,i) ^ ((width M2) |-> d) ) & ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) )
let i be Nat; :: thesis: ( ( i in dom M1 implies Line M,i = (Line M1,i) ^ ((width M2) |-> d) ) & ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) )
thus ( i in dom M1 implies Line M,i = (Line M1,i) ^ ((width M2) |-> d) ) :: thesis: ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) )

proof

set W2d = (width M2) |-> d;
set LM1 = Line M1,i;
set LM = Line M,i;
A31: len M1 <= (len M1) + (len M2) by NAT_1:11;
A32: len (Line M1,i) = width M1 by FINSEQ_1:def 18;
assume A33: i in dom M1 ; :: thesis: Line M,i = (Line M1,i) ^ ((width M2) |-> d)
then A34: 1 <= i by FINSEQ_3:27;
i <= len M1 by A33, FINSEQ_3:27;
then i <= (len M1) + (len M2) by A31, XXREAL_0:2;
then A35: i in dom (block_diagonal <*M1,M2*>,d) by A2, A34, FINSEQ_3:27;
A36: len ((width M2) |-> d) = width M2 by FINSEQ_1:def 18;
A37: len ((Line M1,i) ^ ((width M2) |-> d)) = (len (Line M1,i)) + (len ((width M2) |-> d)) by FINSEQ_1:35;
A38: len (Line M,i) = (width M1) + (width M2) by A27, FINSEQ_1:def 18;
A39: i in Seg (len M1) by A33, FINSEQ_1:def 3;

now

A40: min (Len <*M1,M2*>),(i + 0 ) = 1 by A24, A6, A13, A25, A4, A39, Th10, RVSUM_1:102;
let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M,i) implies (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . j )
assume that
A41: 1 <= j and
A42: j <= len (Line M,i) ; :: thesis: (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . j
A43: j in Seg (width (block_diagonal <*M1,M2*>,d)) by A8, A38, A41, A42, FINSEQ_1:3;
then A44: [i,j] in Indices (block_diagonal <*M1,M2*>,d) by A35, ZFMISC_1:106;
A45: j in dom ((Line M1,i) ^ ((width M2) |-> d)) by A38, A32, A36, A37, A41, A42, FINSEQ_3:27;

now

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

suppose A46: j <= width M1 ; :: thesis: (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . j

then A47: j in Seg (width M1) by A41, FINSEQ_1:3;
A48: j in dom (Line M1,i) by A32, A41, A46, FINSEQ_3:27;
thus (Line M,i) . j = M * i,j by A8, A27, A43, MATRIX_1:def 8
.= (<*M1,M2*> . 1) * (i -' (Sum ((Len <*M1,M2*>) | 0 ))),(j -' (Sum ((Width <*M1,M2*>) | 0 ))) by A1, A6, A18, A30, A41, A44, A40, A46, Def5, RVSUM_1:102
.= (<*M1,M2*> . 1) * i,(j -' 0 ) by NAT_D:40, RVSUM_1:102
.= (<*M1,M2*> . 1) * i,j by NAT_D:40
.= M1 * i,j by FINSEQ_1:58
.= (Line M1,i) . j by A47, MATRIX_1:def 8
.= ((Line M1,i) ^ ((width M2) |-> d)) . j by A48, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A49: j > width M1 ; :: thesis: (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . j

A50: dom ((width M2) |-> d) = Seg (width M2) by A36, FINSEQ_1:def 3;
not j in dom (Line M1,i) by A32, A49, FINSEQ_3:27;
then consider k being Nat such that
A51: k in dom ((width M2) |-> d) and
A52: j = (len (Line M1,i)) + k by A45, FINSEQ_1:38;
thus (Line M,i) . j = M * i,j by A8, A27, A43, MATRIX_1:def 8
.= d by A1, A18, A30, A44, A40, A49, Def5
.= ((width M2) |-> d) . k by A51, A50, FINSEQ_2:71
.= ((Line M1,i) ^ ((width M2) |-> d)) . j by A51, A52, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . j ; :: thesis: verum

end;

hence Line M,i = (Line M1,i) ^ ((width M2) |-> d) by A38, A32, A36, A37, FINSEQ_1:18; :: thesis: verum

end;

thus ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) :: thesis: verum

proof

set LM2 = Line M2,i;
set W1d = (width M1) |-> d;
set LM = Line M,(i + (len M1));
A53: len (Line M2,i) = width M2 by FINSEQ_1:def 18;
A54: len (((width M1) |-> d) ^ (Line M2,i)) = (len ((width M1) |-> d)) + (len (Line M2,i)) by FINSEQ_1:35;
A55: len ((width M1) |-> d) = width M1 by FINSEQ_1:def 18;
A56: len (Line M,(i + (len M1))) = (width M1) + (width M2) by A27, FINSEQ_1:def 18;
assume i in dom M2 ; :: thesis: Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i)
then A57: i in Seg (len M2) by FINSEQ_1:def 3;
then (len M1) + i in Seg ((len M1) + (len M2)) by FINSEQ_1:81;
then A58: (len M1) + i in dom (block_diagonal <*M1,M2*>,d) by A2, FINSEQ_1:def 3;

now

A59: min (Len <*M1,M2*>),(i + (len M1)) = 2 by A17, A28, A26, A21, A29, A15, A57, Th10;
let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M,(i + (len M1))) implies (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . j )
assume that
A60: 1 <= j and
A61: j <= len (Line M,(i + (len M1))) ; :: thesis: (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . j
A62: j in Seg (width (block_diagonal <*M1,M2*>,d)) by A8, A56, A60, A61, FINSEQ_1:3;
then A63: [(i + (len M1)),j] in Indices (block_diagonal <*M1,M2*>,d) by A58, ZFMISC_1:106;
A64: j in dom (((width M1) |-> d) ^ (Line M2,i)) by A56, A53, A55, A54, A60, A61, FINSEQ_3:27;

now

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

suppose A65: j <= width M1 ; :: thesis: (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . j

A66: dom ((width M1) |-> d) = Seg (width M1) by A55, FINSEQ_1:def 3;
A67: j in Seg (width M1) by A60, A65, FINSEQ_1:3;
thus (Line M,(i + (len M1))) . j = (block_diagonal <*M1,M2*>,d) * (i + (len M1)),j by A30, A62, MATRIX_1:def 8
.= d by A1, A26, A18, A63, A59, A65, Def5
.= ((width M1) |-> d) . j by A67, FINSEQ_2:71
.= (((width M1) |-> d) ^ (Line M2,i)) . j by A67, A66, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A68: j > width M1 ; :: thesis: (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . j

A69: dom (Line M2,i) = Seg (width M2) by A53, FINSEQ_1:def 3;
not j in dom ((width M1) |-> d) by A55, A68, FINSEQ_3:27;
then consider k being Nat such that
A70: k in dom (Line M2,i) and
A71: j = (width M1) + k by A55, A64, FINSEQ_1:38;
thus (Line M,(i + (len M1))) . j = (block_diagonal <*M1,M2*>,d) * (i + (len M1)),j by A30, A62, MATRIX_1:def 8
.= (<*M1,M2*> . 2) * ((i + (len M1)) -' (len M1)),(j -' (width M1)) by A7, A8, A1, A17, A26, A15, A18, A22, A56, A61, A63, A59, A68, Def5
.= (<*M1,M2*> . 2) * i,(j -' (width M1)) by NAT_D:34
.= (<*M1,M2*> . ((len <*M1*>) + 1)) * i,k by A10, A71, NAT_D:34
.= M2 * i,k by FINSEQ_1:59
.= (Line M2,i) . k by A70, A69, MATRIX_1:def 8
.= (((width M1) |-> d) ^ (Line M2,i)) . j by A55, A70, A71, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . j ; :: thesis: verum

end;

hence Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) by A56, A53, A55, A54, FINSEQ_1:18; :: thesis: verum

end;

end;

assume A72: for i being Nat holds
( ( i in dom M1 implies Line M,i = (Line M1,i) ^ ((width M2) |-> d) ) & ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) ) ; :: thesis: M = block_diagonal <*M1,M2*>,d
A73: Sum ((Width <*M1,M2*>) | 2) = (width M1) + (width M2) by A22, Th20;

now

set W1d = (width M1) |-> d;
set W2d = (width M2) |-> d;
A74: Indices M = Indices (block_diagonal <*M1,M2*>,d) by MATRIX_1:27;
let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * i,j = (block_diagonal <*M1,M2*>,d) * i,j )
assume A75: [i,j] in Indices M ; :: thesis: M * i,j = (block_diagonal <*M1,M2*>,d) * i,j
A76: i in dom (block_diagonal <*M1,M2*>,d) by A75, A74, ZFMISC_1:106;
then A77: 1 <= i by FINSEQ_3:27;
A78: j in Seg (width (block_diagonal <*M1,M2*>,d)) by A75, A74, ZFMISC_1:106;
then A79: 1 <= j by FINSEQ_1:3;
A80: i in Seg ((len M1) + (len M2)) by A2, A76, FINSEQ_1:def 3;
set LM1 = Line M1,i;
A81: len (Line M1,i) = width M1 by FINSEQ_1:def 18;
A82: len ((width M1) |-> d) = width M1 by FINSEQ_1:def 18;
A83: len ((width M2) |-> d) = width M2 by FINSEQ_1:def 18;
A84: len ((Line M1,i) ^ ((width M2) |-> d)) = (len (Line M1,i)) + (len ((width M2) |-> d)) by FINSEQ_1:35;
A85: j <= width (block_diagonal <*M1,M2*>,d) by A78, FINSEQ_1:3;

now

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

suppose A86: i <= len M1 ; :: thesis: M * i,j = (block_diagonal <*M1,M2*>,d) * i,j

then i in Seg (len M1) by A76, A77;
then A87: min (Len <*M1,M2*>),(i + 0 ) = 1 by A24, A6, A13, A25, A4, Th10, RVSUM_1:102;

A88: now

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

suppose A89: j <= width M1 ; :: thesis: (block_diagonal <*M1,M2*>,d) * i,j = ((Line M1,i) ^ ((width M2) |-> d)) . j

then A90: j in Seg (width M1) by A79, FINSEQ_1:3;
A91: j in dom (Line M1,i) by A79, A81, A89, FINSEQ_3:27;
thus (block_diagonal <*M1,M2*>,d) * i,j = (<*M1,M2*> . 1) * (i -' 0 ),(j -' 0 ) by A1, A6, A4, A5, A18, A75, A74, A79, A87, A89, Def5, RVSUM_1:102
.= (<*M1,M2*> . 1) * i,(j -' 0 ) by NAT_D:40
.= (<*M1,M2*> . 1) * i,j by NAT_D:40
.= M1 * i,j by FINSEQ_1:58
.= (Line M1,i) . j by A90, MATRIX_1:def 8
.= ((Line M1,i) ^ ((width M2) |-> d)) . j by A91, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A92: j > width M1 ; :: thesis: (block_diagonal <*M1,M2*>,d) * i,j = ((Line M1,i) ^ ((width M2) |-> d)) . j

then A93: not j in dom (Line M1,i) by A81, FINSEQ_3:27;
A94: dom ((width M2) |-> d) = Seg (width M2) by A83, FINSEQ_1:def 3;
dom ((Line M1,i) ^ ((width M2) |-> d)) = Seg (width (block_diagonal <*M1,M2*>,d)) by A8, A81, A83, A84, FINSEQ_1:def 3;
then consider k being Nat such that
A95: k in dom ((width M2) |-> d) and
A96: j = (len (Line M1,i)) + k by A78, A93, FINSEQ_1:38;
thus (block_diagonal <*M1,M2*>,d) * i,j = d by A1, A18, A75, A74, A87, A92, Def5
.= ((width M2) |-> d) . k by A95, A94, FINSEQ_2:71
.= ((Line M1,i) ^ ((width M2) |-> d)) . j by A95, A96, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

i in dom M1 by A77, A86, FINSEQ_3:27;
then Line M,i = (Line M1,i) ^ ((width M2) |-> d) by A72;
hence M * i,j = (block_diagonal <*M1,M2*>,d) * i,j by A8, A27, A78, A88, MATRIX_1:def 8; :: thesis: verum

end;

suppose A97: i > len M1 ; :: thesis: M * i,j = (block_diagonal <*M1,M2*>,d) * i,j

then reconsider iL = i - (len M1) as Element of NAT by NAT_1:21;
A98: iL <> 0 by A97;
set LM2 = Line M2,iL;
i = iL + (len M1) ;
then iL in Seg (len M2) by A80, A98, FINSEQ_1:82;
then A99: min (Len <*M1,M2*>),(iL + (len M1)) = 2 by A17, A28, A26, A21, A29, A15, Th10;

A100: now

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

suppose A101: j <= width M1 ; :: thesis: (block_diagonal <*M1,M2*>,d) * i,j = (((width M1) |-> d) ^ (Line M2,iL)) . j

then A102: j in Seg (width M1) by A79, FINSEQ_1:3;
A103: j in dom ((width M1) |-> d) by A79, A82, A101, FINSEQ_3:27;
thus (block_diagonal <*M1,M2*>,d) * i,j = d by A1, A26, A18, A75, A74, A99, A101, Def5
.= ((width M1) |-> d) . j by A102, FINSEQ_2:71
.= (((width M1) |-> d) ^ (Line M2,iL)) . j by A103, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A104: j > width M1 ; :: thesis: (block_diagonal <*M1,M2*>,d) * i,j = (((width M1) |-> d) ^ (Line M2,iL)) . j

len (Line M2,iL) = width M2 by MATRIX_1:def 8;
then A105: dom ((width M2) |-> d) = dom (Line M2,iL) by A83, FINSEQ_3:31;
A106: not j in dom (Line M1,i) by A81, A104, FINSEQ_3:27;
A107: dom ((width M2) |-> d) = Seg (width M2) by A83, FINSEQ_1:def 3;
dom ((Line M1,i) ^ ((width M2) |-> d)) = Seg (width (block_diagonal <*M1,M2*>,d)) by A8, A81, A83, A84, FINSEQ_1:def 3;
then consider k being Nat such that
A108: k in dom ((width M2) |-> d) and
A109: j = (width M1) + k by A78, A81, A106, FINSEQ_1:38;
thus (block_diagonal <*M1,M2*>,d) * i,j = (<*M1,M2*> . 2) * ((iL + (len M1)) -' (len M1)),(j -' (width M1)) by A8, A1, A17, A26, A15, A18, A73, A75, A74, A85, A99, A104, Def5
.= (<*M1,M2*> . 2) * iL,(j -' (width M1)) by NAT_D:34
.= (<*M1,M2*> . ((len <*M1*>) + 1)) * iL,k by A10, A109, NAT_D:34
.= M2 * iL,k by FINSEQ_1:59
.= (Line M2,iL) . k by A108, A107, MATRIX_1:def 8
.= (((width M1) |-> d) ^ (Line M2,iL)) . j by A82, A108, A109, A105, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

Seg (len M2) = dom M2 by FINSEQ_1:def 3;
then Line M,(iL + (len M1)) = ((width M1) |-> d) ^ (Line M2,iL) by A72, A80, A98, FINSEQ_1:82;
hence M * i,j = (block_diagonal <*M1,M2*>,d) * i,j by A8, A27, A78, A100, MATRIX_1:def 8; :: thesis: verum

end;

end;

end;

hence M * i,j = (block_diagonal <*M1,M2*>,d) * i,j ; :: thesis: verum

end;

hence M = block_diagonal <*M1,M2*>,d by MATRIX_1:28; :: thesis: verum