let D be non empty set ; 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; 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; 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; ( 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 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:5;
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)) ) ) )
( ( 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:124;
A11:
dom ((width M1) |-> d) = Seg (width M1)
by FINSEQ_2:124;
set L2 =
(len M2) |-> d;
set L1 =
(len M1) |-> d;
assume A12:
M = block_diagonal (
<*M1,M2*>,
d)
;
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;
( ( 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 CARD_1:def 7;
A14:
dom ((len M1) |-> d) = Seg (len M1)
by FINSEQ_2:124;
A15:
dom ((len M2) |-> d) = Seg (len M2)
by FINSEQ_2:124;
A16:
len (Col (M1,i)) = len M1
by CARD_1:def 7;
then A17:
dom (Col (M1,i)) = dom M1
by FINSEQ_3:29;
A18:
len ((len M2) |-> d) = len M2
by CARD_1:def 7;
then A19:
dom ((len M2) |-> d) = dom M2
by FINSEQ_3:29;
thus
(
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)) )proof
assume A20:
i in Seg (width M1)
;
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:22;
now for j being Nat st 1 <= j & j <= len (Col (M,i)) holds
((Col (M1,i)) ^ ((len M2) |-> d)) . j = (Col (M,i)) . jlet j be
Nat;
( 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))
;
((Col (M1,i)) ^ ((len M2) |-> d)) . j = (Col (M,i)) . j
j in dom M
by A13, A22, A23, FINSEQ_3:25;
then A24:
(Col (M,i)) . j = (Line (M,j)) . i
by A9, A20, MATRIX_0:42;
A25:
dom (Line (M1,j)) = Seg (width M1)
by FINSEQ_2:124;
A26:
j in dom ((Col (M1,i)) ^ ((len M2) |-> d))
by A6, A4, A13, A16, A18, A21, A22, A23, FINSEQ_3:25;
now (Col (M,i)) . j = ((Col (M1,i)) ^ ((len M2) |-> d)) . jper 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:25;
suppose A27:
j in dom (Col (M1,i))
;
(Col (M,i)) . j = ((Col (M1,i)) ^ ((len M2) |-> d)) . jhence (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, MATRIX_0:42
.=
((Col (M1,i)) ^ ((len M2) |-> d)) . j
by A27, FINSEQ_1:def 7
;
verum end; suppose
ex
k being
Nat st
(
k in dom ((len M2) |-> d) &
j = (len (Col (M1,i))) + k )
;
(Col (M,i)) . j = ((Col (M1,i)) ^ ((len M2) |-> d)) . jthen 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:57
.=
((len M2) |-> d) . k
by A15, A28, FINSEQ_2:57
.=
((Col (M1,i)) ^ ((len M2) |-> d)) . j
by A28, A29, FINSEQ_1:def 7
;
verum end; end; end; hence
((Col (M1,i)) ^ ((len M2) |-> d)) . j = (Col (M,i)) . j
;
verum end;
hence
Col (
M,
i)
= (Col (M1,i)) ^ ((len M2) |-> d)
by A6, A13, A16, A18, A21, Th16;
verum
end;
set CM2 =
Col (
M2,
i);
set CMi =
Col (
M,
(i + (width M1)));
A30:
len (Col (M,(i + (width M1)))) = len M
by CARD_1:def 7;
A31:
len (Col (M2,i)) = len M2
by CARD_1:def 7;
then A32:
dom (Col (M2,i)) = dom M2
by FINSEQ_3:29;
A33:
len (((len M1) |-> d) ^ (Col (M2,i))) = (len ((len M1) |-> d)) + (len (Col (M2,i)))
by FINSEQ_1:22;
assume A34:
i in Seg (width M2)
;
Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i))
A35:
len ((len M1) |-> d) = len M1
by CARD_1:def 7;
then A36:
dom ((len M1) |-> d) = dom M1
by FINSEQ_3:29;
now for j being Nat st 1 <= j & j <= len (Col (M,(i + (width M1)))) holds
(((len M1) |-> d) ^ (Col (M2,i))) . j = (Col (M,(i + (width M1)))) . jA37:
len ((width M1) |-> d) = width M1
by CARD_1:def 7;
let j be
Nat;
( 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))))
;
(((len M1) |-> d) ^ (Col (M2,i))) . j = (Col (M,(i + (width M1)))) . jA40:
j in dom M
by A30, A38, A39, FINSEQ_3:25;
i + (width M1) in Seg (width M)
by A7, A8, A34, FINSEQ_1:60;
then A41:
(Col (M,(i + (width M1)))) . j = (Line (M,j)) . (i + (width M1))
by A40, MATRIX_0:42;
A42:
len (Line (M1,j)) = width M1
by CARD_1:def 7;
A43:
j in dom (((len M1) |-> d) ^ (Col (M2,i)))
by A6, A4, A30, A31, A35, A33, A38, A39, FINSEQ_3:25;
now (Col (M,(i + (width M1)))) . j = (((len M1) |-> d) ^ (Col (M2,i))) . jper 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:25;
suppose A44:
j in dom ((len M1) |-> d)
;
(Col (M,(i + (width M1)))) . j = (((len M1) |-> d) ^ (Col (M2,i))) . jhence (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:57
.=
((len M1) |-> d) . j
by A14, A44, FINSEQ_2:57
.=
(((len M1) |-> d) ^ (Col (M2,i))) . j
by A44, FINSEQ_1:def 7
;
verum end; suppose
ex
k being
Nat st
(
k in dom (Col (M2,i)) &
j = (len ((len M1) |-> d)) + k )
;
(Col (M,(i + (width M1)))) . j = (((len M1) |-> d) ^ (Col (M2,i))) . jthen 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:124;
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, MATRIX_0:42
.=
(((len M1) |-> d) ^ (Col (M2,i))) . j
by A45, A46, FINSEQ_1:def 7
;
verum end; end; end; hence
(((len M1) |-> d) ^ (Col (M2,i))) . j = (Col (M,(i + (width M1)))) . j
;
verum end;
hence
Col (
M,
(i + (width M1)))
= ((len M1) |-> d) ^ (Col (M2,i))
by A6, A30, A31, A35, A33, Th16;
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)) ) )
; 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:5;
now 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 W2 =
(width M2) |-> d;
set W1 =
(width M1) |-> d;
let i be
Nat;
( ( 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 CARD_1:def 7;
A51:
len ((width M2) |-> d) = width M2
by CARD_1:def 7;
then A52:
dom ((width M2) |-> d) = Seg (width M2)
by FINSEQ_1:def 3;
A53:
len (Line (M,i)) = width M
by CARD_1:def 7;
then A54:
dom (Line (M,i)) = Seg (width M)
by FINSEQ_1:def 3;
A55:
len (Line (M1,i)) = width M1
by CARD_1:def 7;
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) )
( i in dom M2 implies Line (M,(i + (len M1))) = ((width M1) |-> d) ^ (Line (M2,i)) )proof
assume A57:
i in dom M1
;
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:22;
now for j being Nat st 1 <= j & j <= len (Line (M,i)) holds
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . jA59:
dom ((len M1) |-> d) = Seg (len M1)
by FINSEQ_2:124;
let j be
Nat;
( 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))
;
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j
j in Seg (width M)
by A54, A60, A61, FINSEQ_3:25;
then A62:
(Line (M,i)) . j = (Col (M,j)) . i
by A49, A1, A2, A57, MATRIX_0:42;
A63:
dom (Col (M1,j)) = Seg (len M1)
by FINSEQ_2:124;
A64:
j in dom ((Line (M1,i)) ^ ((width M2) |-> d))
by A7, A8, A53, A55, A51, A58, A60, A61, FINSEQ_3:25;
now (Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . jper 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:25;
suppose A65:
j in dom (Line (M1,i))
;
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . jhence (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, MATRIX_0:42
.=
((Line (M1,i)) ^ ((width M2) |-> d)) . j
by A65, FINSEQ_1:def 7
;
verum end; suppose
ex
n being
Nat st
(
n in dom ((width M2) |-> d) &
j = (len (Line (M1,i))) + n )
;
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . jthen 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:57
.=
((width M2) |-> d) . n
by A52, A66, FINSEQ_2:57
.=
((Line (M1,i)) ^ ((width M2) |-> d)) . j
by A66, A67, FINSEQ_1:def 7
;
verum end; end; end; hence
(Line (M,i)) . j = ((Line (M1,i)) ^ ((width M2) |-> d)) . j
;
verum end;
hence
Line (
M,
i)
= (Line (M1,i)) ^ ((width M2) |-> d)
by A7, A53, A55, A51, A58, Th20;
verum
end; A68:
len (Line (M2,i)) = width M2
by CARD_1:def 7;
then A69:
dom (Line (M2,i)) = Seg (width M2)
by FINSEQ_1:def 3;
A70:
len ((width M1) |-> d) = width M1
by CARD_1:def 7;
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)) )
verumproof
assume A72:
i in dom M2
;
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:22;
now for j being Nat st 1 <= j & j <= len (Line (M,(i + (len M1)))) holds
(Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . jA74:
len ((len M1) |-> d) = len M1
by CARD_1:def 7;
A75:
dom ((len M2) |-> d) = Seg (len M2)
by FINSEQ_2:124;
A76:
dom M2 = Seg (len M2)
by FINSEQ_1:def 3;
let j be
Nat;
( 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))))
;
(Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . j
j in Seg (width M)
by A50, A77, A78;
then A79:
(Line (M,(i + (len M1)))) . j = (Col (M,j)) . (i + (len M1))
by A6, A4, A1, A72, A76, FINSEQ_1:60, MATRIX_0:42;
A80:
len (Col (M1,j)) = len M1
by CARD_1:def 7;
A81:
j in dom (((width M1) |-> d) ^ (Line (M2,i)))
by A7, A8, A50, A68, A70, A73, A77, A78, FINSEQ_3:25;
now (Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . jper 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:25;
suppose A82:
j in dom ((width M1) |-> d)
;
(Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . jhence (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:57
.=
((width M1) |-> d) . j
by A71, A82, FINSEQ_2:57
.=
(((width M1) |-> d) ^ (Line (M2,i))) . j
by A82, FINSEQ_1:def 7
;
verum end; suppose
ex
n being
Nat st
(
n in dom (Line (M2,i)) &
j = (len ((width M1) |-> d)) + n )
;
(Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . jthen 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:124;
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, MATRIX_0:42
.=
(((width M1) |-> d) ^ (Line (M2,i))) . j
by A83, A84, FINSEQ_1:def 7
;
verum end; end; end; hence
(Line (M,(i + (len M1)))) . j = (((width M1) |-> d) ^ (Line (M2,i))) . j
;
verum end;
hence
Line (
M,
(i + (len M1)))
= ((width M1) |-> d) ^ (Line (M2,i))
by A7, A50, A68, A70, A73, Th20;
verum
end; end;
hence
M = block_diagonal (<*M1,M2*>,d)
by Th23; verum