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 Seg (width M1) implies Col M,i = (Col M1,i) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col 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 Seg (width M1) implies Col M,i = (Col M1,i) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col 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 Seg (width M1) implies Col M,i = (Col M1,i) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col 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 Seg (width M1) implies Col M,i = (Col M1,i) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i) ) ) )
set m1 = <*M1*>;
set m2 = <*M2*>;
set m12 = <*M1,M2*>;
set B = block_diagonal <*M1,M2*>,d;
A1: Seg (len M) = dom M by FINSEQ_1:def 3;
A2: Seg (len M1) = dom M1 by FINSEQ_1:def 3;
A3: dom M2 = Seg (len M2) by FINSEQ_1:def 3;
A4: Sum (Len <*M1,M2*>) = (len M1) + (len M2) by Th16;
A5: ( Sum (Len <*M1,M2*>) = 0 implies Sum (Width <*M1,M2*>) = 0 ) by Th13;
then A6: len M = Sum (Len <*M1,M2*>) by MATRIX13:1;
A7: width M = Sum (Width <*M1,M2*>) by A5, MATRIX13:1;
A8: Sum (Width <*M1,M2*>) = (width M1) + (width M2) by Th20;
then width M1 <= width M by A7, NAT_1:12;
then A9: Seg (width M1) c= Seg (width M) by FINSEQ_1:7;
thus ( M = block_diagonal <*M1,M2*>,d implies for i being Nat holds
( ( i in Seg (width M1) implies Col M,i = (Col M1,i) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i) ) ) ) :: thesis: ( ( for i being Nat holds
( ( i in Seg (width M1) implies Col M,i = (Col M1,i) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i) ) ) ) implies M = block_diagonal <*M1,M2*>,d )

proof

A10: dom ((width M2) |-> d) = Seg (width M2) by FINSEQ_2:144;
A11: dom ((width M1) |-> d) = Seg (width M1) by FINSEQ_2:144;
set L2 = (len M2) |-> d;
set L1 = (len M1) |-> d;
assume A12: M = block_diagonal <*M1,M2*>,d ; :: thesis: for i being Nat holds
( ( i in Seg (width M1) implies Col M,i = (Col M1,i) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i) ) )
let i be Nat; :: thesis: ( ( i in Seg (width M1) implies Col M,i = (Col M1,i) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i) ) )
set CM = Col M,i;
set CM1 = Col M1,i;
A13: len (Col M,i) = len M by FINSEQ_1:def 18;
A14: dom ((len M1) |-> d) = Seg (len M1) by FINSEQ_2:144;
A15: dom ((len M2) |-> d) = Seg (len M2) by FINSEQ_2:144;
A16: len (Col M1,i) = len M1 by FINSEQ_1:def 18;
then A17: dom (Col M1,i) = dom M1 by FINSEQ_3:31;
A18: len ((len M2) |-> d) = len M2 by FINSEQ_1:def 18;
then A19: dom ((len M2) |-> d) = dom M2 by FINSEQ_3:31;
thus ( i in Seg (width M1) implies Col M,i = (Col M1,i) ^ ((len M2) |-> d) ) :: thesis: ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i) )

proof

assume A20: i in Seg (width M1) ; :: thesis: Col M,i = (Col M1,i) ^ ((len M2) |-> d)
A21: len ((Col M1,i) ^ ((len M2) |-> d)) = (len (Col M1,i)) + (len ((len M2) |-> d)) by FINSEQ_1:35;

now

let j be Nat; :: thesis: ( 1 <= j & j <= len (Col M,i) implies ((Col M1,i) ^ ((len M2) |-> d)) . j = (Col M,i) . j )
assume that
A22: 1 <= j and
A23: j <= len (Col M,i) ; :: thesis: ((Col M1,i) ^ ((len M2) |-> d)) . j = (Col M,i) . j
j in dom M by A13, A22, A23, FINSEQ_3:27;
then A24: (Col M,i) . j = (Line M,j) . i by A9, A20, GOBOARD1:17;
A25: dom (Line M1,j) = Seg (width M1) by FINSEQ_2:144;
A26: j in dom ((Col M1,i) ^ ((len M2) |-> d)) by A6, A4, A13, A16, A18, A21, A22, A23, FINSEQ_3:27;

now

per cases ( j in dom (Col M1,i) or ex k being Nat st
( k in dom ((len M2) |-> d) & j = (len (Col M1,i)) + k ) ) by A26, FINSEQ_1:38;

suppose A27: j in dom (Col M1,i) ; :: thesis: (Col M,i) . j = ((Col M1,i) ^ ((len M2) |-> d)) . j

hence (Col M,i) . j = ((Line M1,j) ^ ((width M2) |-> d)) . i by A12, A17, A24, Th23
.= (Line M1,j) . i by A20, A25, FINSEQ_1:def 7
.= (Col M1,i) . j by A17, A20, A27, GOBOARD1:17
.= ((Col M1,i) ^ ((len M2) |-> d)) . j by A27, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex k being Nat st
( k in dom ((len M2) |-> d) & j = (len (Col M1,i)) + k ) ; :: thesis: (Col M,i) . j = ((Col M1,i) ^ ((len M2) |-> d)) . j

then consider k being Nat such that
A28: k in dom ((len M2) |-> d) and
A29: j = (len (Col M1,i)) + k ;
thus (Col M,i) . j = (((width M1) |-> d) ^ (Line M2,k)) . i by A12, A16, A19, A24, A28, A29, Th23
.= ((width M1) |-> d) . i by A11, A20, FINSEQ_1:def 7
.= d by A20, FINSEQ_2:71
.= ((len M2) |-> d) . k by A15, A28, FINSEQ_2:71
.= ((Col M1,i) ^ ((len M2) |-> d)) . j by A28, A29, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

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

end;

hence Col M,i = (Col M1,i) ^ ((len M2) |-> d) by A6, A13, A16, A18, A21, Th16, FINSEQ_1:18; :: thesis: verum

end;

set CM2 = Col M2,i;
set CMi = Col M,(i + (width M1));
A30: len (Col M,(i + (width M1))) = len M by FINSEQ_1:def 18;
A31: len (Col M2,i) = len M2 by FINSEQ_1:def 18;
then A32: dom (Col M2,i) = dom M2 by FINSEQ_3:31;
A33: len (((len M1) |-> d) ^ (Col M2,i)) = (len ((len M1) |-> d)) + (len (Col M2,i)) by FINSEQ_1:35;
assume A34: i in Seg (width M2) ; :: thesis: Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i)
A35: len ((len M1) |-> d) = len M1 by FINSEQ_1:def 18;
then A36: dom ((len M1) |-> d) = dom M1 by FINSEQ_3:31;

now

A37: len ((width M1) |-> d) = width M1 by FINSEQ_1:def 18;
let j be Nat; :: thesis: ( 1 <= j & j <= len (Col M,(i + (width M1))) implies (((len M1) |-> d) ^ (Col M2,i)) . j = (Col M,(i + (width M1))) . j )
assume that
A38: 1 <= j and
A39: j <= len (Col M,(i + (width M1))) ; :: thesis: (((len M1) |-> d) ^ (Col M2,i)) . j = (Col M,(i + (width M1))) . j
A40: j in dom M by A30, A38, A39, FINSEQ_3:27;
i + (width M1) in Seg (width M) by A7, A8, A34, FINSEQ_1:81;
then A41: (Col M,(i + (width M1))) . j = (Line M,j) . (i + (width M1)) by A40, GOBOARD1:17;
A42: len (Line M1,j) = width M1 by FINSEQ_1:def 18;
A43: j in dom (((len M1) |-> d) ^ (Col M2,i)) by A6, A4, A30, A31, A35, A33, A38, A39, FINSEQ_3:27;

now

per cases ( j in dom ((len M1) |-> d) or ex k being Nat st
( k in dom (Col M2,i) & j = (len ((len M1) |-> d)) + k ) ) by A43, FINSEQ_1:38;

suppose A44: j in dom ((len M1) |-> d) ; :: thesis: (Col M,(i + (width M1))) . j = (((len M1) |-> d) ^ (Col M2,i)) . j

hence (Col M,(i + (width M1))) . j = ((Line M1,j) ^ ((width M2) |-> d)) . (i + (width M1)) by A12, A36, A41, Th23
.= ((width M2) |-> d) . i by A10, A34, A42, FINSEQ_1:def 7
.= d by A34, FINSEQ_2:71
.= ((len M1) |-> d) . j by A14, A44, FINSEQ_2:71
.= (((len M1) |-> d) ^ (Col M2,i)) . j by A44, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex k being Nat st
( k in dom (Col M2,i) & j = (len ((len M1) |-> d)) + k ) ; :: thesis: (Col M,(i + (width M1))) . j = (((len M1) |-> d) ^ (Col M2,i)) . j

then consider k being Nat such that
A45: k in dom (Col M2,i) and
A46: j = (len ((len M1) |-> d)) + k ;
A47: dom (Line M2,k) = Seg (width M2) by FINSEQ_2:144;
thus (Col M,(i + (width M1))) . j = (((width M1) |-> d) ^ (Line M2,k)) . (i + (width M1)) by A12, A35, A32, A41, A45, A46, Th23
.= (Line M2,k) . i by A34, A37, A47, FINSEQ_1:def 7
.= (Col M2,i) . k by A32, A34, A45, GOBOARD1:17
.= (((len M1) |-> d) ^ (Col M2,i)) . j by A45, A46, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

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

end;

hence Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i) by A6, A30, A31, A35, A33, Th16, FINSEQ_1:18; :: thesis: verum

end;

assume A48: for i being Nat holds
( ( i in Seg (width M1) implies Col M,i = (Col M1,i) ^ ((len M2) |-> d) ) & ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i) ) ) ; :: thesis: M = block_diagonal <*M1,M2*>,d
len M1 <= len M by A6, A4, NAT_1:12;
then A49: Seg (len M1) c= Seg (len M) by FINSEQ_1:7;

now

set W2 = (width M2) |-> d;
set W1 = (width M1) |-> d;
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) ) )
set LM = Line M,i;
set LMi = Line M,(i + (len M1));
set LM1 = Line M1,i;
set LM2 = Line M2,i;
A50: len (Line M,(i + (len M1))) = width M by FINSEQ_1:def 18;
A51: len ((width M2) |-> d) = width M2 by FINSEQ_1:def 18;
then A52: dom ((width M2) |-> d) = Seg (width M2) by FINSEQ_1:def 3;
A53: len (Line M,i) = width M by FINSEQ_1:def 18;
then A54: dom (Line M,i) = Seg (width M) by FINSEQ_1:def 3;
A55: len (Line M1,i) = width M1 by FINSEQ_1:def 18;
then A56: dom (Line M1,i) = Seg (width M1) by FINSEQ_1:def 3;
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

assume A57: i in dom M1 ; :: thesis: Line M,i = (Line M1,i) ^ ((width M2) |-> d)
A58: len ((Line M1,i) ^ ((width M2) |-> d)) = (len (Line M1,i)) + (len ((width M2) |-> d)) by FINSEQ_1:35;

now

A59: dom ((len M1) |-> d) = Seg (len M1) by FINSEQ_2:144;
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
A60: 1 <= j and
A61: j <= len (Line M,i) ; :: thesis: (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . j
j in Seg (width M) by A54, A60, A61, FINSEQ_3:27;
then A62: (Line M,i) . j = (Col M,j) . i by A49, A1, A2, A57, GOBOARD1:17;
A63: dom (Col M1,j) = Seg (len M1) by FINSEQ_2:144;
A64: j in dom ((Line M1,i) ^ ((width M2) |-> d)) by A7, A8, A53, A55, A51, A58, A60, A61, FINSEQ_3:27;

now

per cases ( j in dom (Line M1,i) or ex n being Nat st
( n in dom ((width M2) |-> d) & j = (len (Line M1,i)) + n ) ) by A64, FINSEQ_1:38;

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

hence (Line M,i) . j = ((Col M1,j) ^ ((len M2) |-> d)) . i by A48, A56, A62
.= (Col M1,j) . i by A2, A57, A63, FINSEQ_1:def 7
.= (Line M1,i) . j by A56, A57, A65, GOBOARD1:17
.= ((Line M1,i) ^ ((width M2) |-> d)) . j by A65, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom ((width M2) |-> d) & j = (len (Line M1,i)) + n ) ; :: thesis: (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . j

then consider n being Nat such that
A66: n in dom ((width M2) |-> d) and
A67: j = (len (Line M1,i)) + n ;
thus (Line M,i) . j = (((len M1) |-> d) ^ (Col M2,n)) . i by A48, A55, A52, A62, A66, A67
.= ((len M1) |-> d) . i by A2, A57, A59, FINSEQ_1:def 7
.= d by A2, A57, FINSEQ_2:71
.= ((width M2) |-> d) . n by A52, A66, FINSEQ_2:71
.= ((Line M1,i) ^ ((width M2) |-> d)) . j by A66, A67, 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 A7, A53, A55, A51, A58, Th20, FINSEQ_1:18; :: thesis: verum

end;

A68: len (Line M2,i) = width M2 by FINSEQ_1:def 18;
then A69: dom (Line M2,i) = Seg (width M2) by FINSEQ_1:def 3;
A70: len ((width M1) |-> d) = width M1 by FINSEQ_1:def 18;
then A71: dom ((width M1) |-> d) = Seg (width M1) by FINSEQ_1:def 3;
thus ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) :: thesis: verum

proof

assume A72: i in dom M2 ; :: thesis: Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i)
A73: len (((width M1) |-> d) ^ (Line M2,i)) = (len ((width M1) |-> d)) + (len (Line M2,i)) by FINSEQ_1:35;

now

A74: len ((len M1) |-> d) = len M1 by FINSEQ_1:def 18;
A75: dom ((len M2) |-> d) = Seg (len M2) by FINSEQ_2:144;
A76: dom M2 = Seg (len M2) by FINSEQ_1:def 3;
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
A77: 1 <= j and
A78: j <= len (Line M,(i + (len M1))) ; :: thesis: (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . j
j in Seg (width M) by A53, A50, A54, A77, A78, FINSEQ_3:27;
then A79: (Line M,(i + (len M1))) . j = (Col M,j) . (i + (len M1)) by A6, A4, A1, A72, A76, FINSEQ_1:81, GOBOARD1:17;
A80: len (Col M1,j) = len M1 by FINSEQ_1:def 18;
A81: j in dom (((width M1) |-> d) ^ (Line M2,i)) by A7, A8, A50, A68, A70, A73, A77, A78, FINSEQ_3:27;

now

per cases ( j in dom ((width M1) |-> d) or ex n being Nat st
( n in dom (Line M2,i) & j = (len ((width M1) |-> d)) + n ) ) by A81, FINSEQ_1:38;

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

hence (Line M,(i + (len M1))) . j = ((Col M1,j) ^ ((len M2) |-> d)) . (i + (len M1)) by A48, A71, A79
.= ((len M2) |-> d) . i by A3, A72, A80, A75, FINSEQ_1:def 7
.= d by A3, A72, FINSEQ_2:71
.= ((width M1) |-> d) . j by A71, A82, FINSEQ_2:71
.= (((width M1) |-> d) ^ (Line M2,i)) . j by A82, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom (Line M2,i) & j = (len ((width M1) |-> d)) + n ) ; :: thesis: (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . j

then consider n being Nat such that
A83: n in dom (Line M2,i) and
A84: j = (len ((width M1) |-> d)) + n ;
A85: dom (Col M2,n) = Seg (len M2) by FINSEQ_2:144;
thus (Line M,(i + (len M1))) . j = (((len M1) |-> d) ^ (Col M2,n)) . (i + (len M1)) by A48, A70, A69, A79, A83, A84
.= (Col M2,n) . i by A3, A72, A74, A85, FINSEQ_1:def 7
.= (Line M2,i) . n by A69, A72, A83, GOBOARD1:17
.= (((width M1) |-> d) ^ (Line M2,i)) . j by A83, A84, 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 A7, A50, A68, A70, A73, Th20, FINSEQ_1:18; :: thesis: verum

end;

end;

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