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:
( len (block_diagonal <*M1,M2*>,d) = Sum (Len <*M1,M2*>) & width (block_diagonal <*M1,M2*>,d) = Sum (Width <*M1,M2*>) )
by Def5;
A2:
( Len <*M1,M2*> = (Len <*M1*>) ^ (Len <*M2*>) & Width <*M1,M2*> = (Width <*M1*>) ^ (Width <*M2*>) & Len <*M1*> = <*(len M1)*> & Len <*M2*> = <*(len M2)*> & Width <*M1*> = <*(width M1)*> )
by Th14, Th15, Th18, Th19;
A3:
( len (block_diagonal <*M1,M2*>,d) = (len M1) + (len M2) & width (block_diagonal <*M1,M2*>,d) = (width M1) + (width M2) & Sum <*(width M1)*> = width M1 & Sum <*(len M1)*> = len M1 )
by A1, Th16, Th20, RVSUM_1:103;
( Sum (Len <*M1,M2*>) = 0 implies Sum (Width <*M1,M2*>) = 0 )
by Th13;
then A4:
width M = (width M1) + (width M2)
by A1, A3, MATRIX13:1;
A5:
( len <*(len M1)*> = 1 & len <*(width M1)*> = 1 & len <*M1*> = 1 )
by FINSEQ_1:57;
then A6:
len (Len <*M1,M2*>) = 1 + 1
by A2, FINSEQ_2:19;
then A7:
dom (Len <*M1,M2*>) = {1,2}
by FINSEQ_1:4, FINSEQ_1:def 3;
A8:
( len (Width <*M1,M2*>) = len <*M1,M2*> & len <*M1,M2*> = len (Len <*M1,M2*>) )
by FINSEQ_1:def 18;
A9:
( 1 in dom (Len <*M1,M2*>) & 2 in dom (Len <*M1,M2*>) & 1 -' 1 = 0 & 2 -' 1 = 2 - 1 )
by A7, TARSKI:def 2, XREAL_1:234, XREAL_1:235;
then A10:
( (Len <*M1,M2*>) . 2 = len M2 & (Len <*M1,M2*>) /. 2 = (Len <*M1,M2*>) . 2 & (Len <*M1,M2*>) . 1 = len M1 & (Len <*M1,M2*>) /. 1 = (Len <*M1,M2*>) . 1 & (Len <*M1,M2*>) | 0 = <*> REAL & (Width <*M1,M2*>) | 0 = <*> REAL & (Len <*M1,M2*>) | 1 = <*(len M1)*> & (Width <*M1,M2*>) | 1 = <*(width M1)*> & (Width <*M1,M2*>) | 2 = Width <*M1,M2*> )
by A2, A5, A6, A8, FINSEQ_1:58, FINSEQ_1:59, FINSEQ_1:79, FINSEQ_5:26, PARTFUN1:def 8;
then A11:
Sum ((Width <*M1,M2*>) | 2) = (width M1) + (width M2)
by Th20;
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 A12:
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
assume
i in dom M1
;
:: thesis: Line M,i = (Line M1,i) ^ ((width M2) |-> d)
then A13:
( 1
<= i &
i <= len M1 &
len M1 <= (len M1) + (len M2) &
i in Seg (len M1) )
by FINSEQ_1:def 3, FINSEQ_3:27, NAT_1:11;
then
i <= (len M1) + (len M2)
by XXREAL_0:2;
then A14:
i in dom (block_diagonal <*M1,M2*>,d)
by A3, A13, FINSEQ_3:27;
set LM =
Line M,
i;
set LM1 =
Line M1,
i;
set W2d =
(width M2) |-> d;
A15:
(
len (Line M,i) = (width M1) + (width M2) &
len (Line M1,i) = width M1 &
len ((width M2) |-> d) = width M2 &
len ((Line M1,i) ^ ((width M2) |-> d)) = (len (Line M1,i)) + (len ((width M2) |-> d)) )
by A4, FINSEQ_1:35, FINSEQ_1:def 18, MATRIX_1:def 8;
now 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 A16:
( 1
<= j &
j <= len (Line M,i) )
;
:: thesis: (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . jA17:
(
j in Seg (width (block_diagonal <*M1,M2*>,d)) &
j in dom ((Line M1,i) ^ ((width M2) |-> d)) )
by A15, A16, A3, FINSEQ_1:3, FINSEQ_3:27;
then A18:
[i,j] in Indices (block_diagonal <*M1,M2*>,d)
by A14, ZFMISC_1:106;
A19:
min (Len <*M1,M2*>),
(i + 0 ) = 1
by A10, A9, A13, Th10, RVSUM_1:102;
now per cases
( j <= width M1 or j > width M1 )
;
suppose A20:
j <= width M1
;
:: thesis: (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . jthen A21:
(
j in Seg (width M1) &
j in dom (Line M1,i) )
by A15, A16, FINSEQ_1:3, FINSEQ_3:27;
thus (Line M,i) . j =
M * i,
j
by A3, A4, A17, MATRIX_1:def 8
.=
(<*M1,M2*> . 1) * (i -' (Sum ((Len <*M1,M2*>) | 0 ))),
(j -' (Sum ((Width <*M1,M2*>) | 0 )))
by A12, A16, A18, A9, A19, A10, Def5, A20, A3, 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 A21, MATRIX_1:def 8
.=
((Line M1,i) ^ ((width M2) |-> d)) . j
by A21, FINSEQ_1:def 7
;
:: thesis: verum end; suppose A22:
j > width M1
;
:: thesis: (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . jthen
not
j in dom (Line M1,i)
by A15, FINSEQ_3:27;
then consider k being
Nat such that A23:
(
k in dom ((width M2) |-> d) &
j = (len (Line M1,i)) + k )
by A17, FINSEQ_1:38;
A24:
dom ((width M2) |-> d) = Seg (width M2)
by A15, FINSEQ_1:def 3;
thus (Line M,i) . j =
M * i,
j
by A3, A4, A17, MATRIX_1:def 8
.=
d
by A12, A18, A19, A10, Def5, A22, A3
.=
((width M2) |-> d) . k
by A23, A24, FINSEQ_2:71
.=
((Line M1,i) ^ ((width M2) |-> d)) . j
by A23, FINSEQ_1:def 7
;
:: thesis: verum 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 A15, FINSEQ_1:18;
:: thesis: verum
end; thus
(
i in dom M2 implies
Line M,
(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) )
:: thesis: verumproof
set LM =
Line M,
(i + (len M1));
set W1d =
(width M1) |-> d;
set LM2 =
Line M2,
i;
assume
i in dom M2
;
:: thesis: Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i)
then A25:
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 A26:
(len M1) + i in dom (block_diagonal <*M1,M2*>,d)
by A3, FINSEQ_1:def 3;
A27:
(
len (Line M,(i + (len M1))) = (width M1) + (width M2) &
len (Line M2,i) = width M2 &
len ((width M1) |-> d) = width M1 &
len (((width M1) |-> d) ^ (Line M2,i)) = (len ((width M1) |-> d)) + (len (Line M2,i)) )
by A4, FINSEQ_1:35, FINSEQ_1:def 18, MATRIX_1:def 8;
now 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 A28:
( 1
<= j &
j <= len (Line M,(i + (len M1))) )
;
:: thesis: (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . jA29:
(
j in Seg (width (block_diagonal <*M1,M2*>,d)) &
j in dom (((width M1) |-> d) ^ (Line M2,i)) )
by A3, A27, A28, FINSEQ_1:3, FINSEQ_3:27;
then A30:
[(i + (len M1)),j] in Indices (block_diagonal <*M1,M2*>,d)
by A26, ZFMISC_1:106;
A31:
min (Len <*M1,M2*>),
(i + (len M1)) = 2
by A25, A9, Th10, A3, A10;
now per cases
( j <= width M1 or j > width M1 )
;
suppose A32:
j <= width M1
;
:: thesis: (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . jthen A33:
(
j in Seg (width M1) &
dom ((width M1) |-> d) = Seg (width M1) )
by A28, A27, FINSEQ_1:3, FINSEQ_1:def 3;
thus (Line M,(i + (len M1))) . j =
(block_diagonal <*M1,M2*>,d) * (i + (len M1)),
j
by A12, A29, MATRIX_1:def 8
.=
d
by A30, A9, A10, A31, Def5, A3, A32
.=
((width M1) |-> d) . j
by A33, FINSEQ_2:71
.=
(((width M1) |-> d) ^ (Line M2,i)) . j
by A33, FINSEQ_1:def 7
;
:: thesis: verum end; suppose A34:
j > width M1
;
:: thesis: (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . jthen
not
j in dom ((width M1) |-> d)
by A27, FINSEQ_3:27;
then consider k being
Nat such that A35:
(
k in dom (Line M2,i) &
j = (width M1) + k )
by A27, A29, FINSEQ_1:38;
A36:
dom (Line M2,i) = Seg (width M2)
by A27, FINSEQ_1:def 3;
thus (Line M,(i + (len M1))) . j =
(block_diagonal <*M1,M2*>,d) * (i + (len M1)),
j
by A12, A29, MATRIX_1:def 8
.=
(<*M1,M2*> . 2) * ((i + (len M1)) -' (len M1)),
(j -' (width M1))
by A27, A28, A3, A30, A9, A10, A31, A1, A34, Def5
.=
(<*M1,M2*> . 2) * i,
(j -' (width M1))
by NAT_D:34
.=
(<*M1,M2*> . ((len <*M1*>) + 1)) * i,
k
by A5, A35, NAT_D:34
.=
M2 * i,
k
by FINSEQ_1:59
.=
(Line M2,i) . k
by A35, A36, MATRIX_1:def 8
.=
(((width M1) |-> d) ^ (Line M2,i)) . j
by A27, A35, FINSEQ_1:def 7
;
:: thesis: verum 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 A27, FINSEQ_1:18;
:: thesis: verum
end;
end;
assume A37:
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
now let i,
j be
Nat;
:: thesis: ( [i,j] in Indices M implies M * i,j = (block_diagonal <*M1,M2*>,d) * i,j )assume A38:
[i,j] in Indices M
;
:: thesis: M * i,j = (block_diagonal <*M1,M2*>,d) * i,jA39:
Indices M = Indices (block_diagonal <*M1,M2*>,d)
by MATRIX_1:27;
then A40:
(
i in dom (block_diagonal <*M1,M2*>,d) &
j in Seg (width (block_diagonal <*M1,M2*>,d)) )
by A38, ZFMISC_1:106;
then A41:
( 1
<= i & 1
<= j &
i in Seg ((len M1) + (len M2)) &
j <= width (block_diagonal <*M1,M2*>,d) )
by A3, FINSEQ_1:3, FINSEQ_1:def 3, FINSEQ_3:27;
set LM1 =
Line M1,
i;
set W2d =
(width M2) |-> d;
set W1d =
(width M1) |-> d;
A42:
(
len (Line M1,i) = width M1 &
len ((width M2) |-> d) = width M2 &
len ((width M1) |-> d) = width M1 &
len ((Line M1,i) ^ ((width M2) |-> d)) = (len (Line M1,i)) + (len ((width M2) |-> d)) )
by FINSEQ_1:35, FINSEQ_1:def 18, MATRIX_1:def 8;
now per cases
( i <= len M1 or i > len M1 )
;
suppose A43:
i <= len M1
;
:: thesis: M * i,j = (block_diagonal <*M1,M2*>,d) * i,jthen
i in dom M1
by A41, FINSEQ_3:27;
then A44:
Line M,
i = (Line M1,i) ^ ((width M2) |-> d)
by A37;
i in Seg (len M1)
by A43, A41;
then A45:
min (Len <*M1,M2*>),
(i + 0 ) = 1
by A10, A9, Th10, RVSUM_1:102;
now per cases
( j <= width M1 or j > width M1 )
;
suppose A46:
j <= width M1
;
:: thesis: (block_diagonal <*M1,M2*>,d) * i,j = ((Line M1,i) ^ ((width M2) |-> d)) . jthen A47:
(
j in Seg (width M1) &
j in dom (Line M1,i) )
by A41, A42, FINSEQ_1:3, FINSEQ_3:27;
thus (block_diagonal <*M1,M2*>,d) * i,
j =
(<*M1,M2*> . 1) * (i -' 0 ),
(j -' 0 )
by A9, A10, A38, A39, A41, A45, A46, Def5, A3, 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 A47, MATRIX_1:def 8
.=
((Line M1,i) ^ ((width M2) |-> d)) . j
by A47, FINSEQ_1:def 7
;
:: thesis: verum end; suppose A48:
j > width M1
;
:: thesis: (block_diagonal <*M1,M2*>,d) * i,j = ((Line M1,i) ^ ((width M2) |-> d)) . jthen
( not
j in dom (Line M1,i) &
dom ((Line M1,i) ^ ((width M2) |-> d)) = Seg (width (block_diagonal <*M1,M2*>,d)) )
by A3, A42, FINSEQ_1:def 3, FINSEQ_3:27;
then consider k being
Nat such that A49:
(
k in dom ((width M2) |-> d) &
j = (len (Line M1,i)) + k )
by A40, FINSEQ_1:38;
A50:
dom ((width M2) |-> d) = Seg (width M2)
by A42, FINSEQ_1:def 3;
thus (block_diagonal <*M1,M2*>,d) * i,
j =
d
by A3, A10, A38, A39, A45, A48, Def5
.=
((width M2) |-> d) . k
by A49, A50, FINSEQ_2:71
.=
((Line M1,i) ^ ((width M2) |-> d)) . j
by A49, FINSEQ_1:def 7
;
:: thesis: verum end; hence
M * i,
j = (block_diagonal <*M1,M2*>,d) * i,
j
by A44, A3, A4, A40, MATRIX_1:def 8;
:: thesis: verum end; suppose A51:
i > len M1
;
:: thesis: M * i,j = (block_diagonal <*M1,M2*>,d) * i,jthen reconsider iL =
i - (len M1) as
Element of
NAT by NAT_1:21;
set LM2 =
Line M2,
iL;
iL <> 0
by A51;
then
(
iL > 0 &
i = iL + (len M1) )
;
then A52:
(
iL in Seg (len M2) &
Seg (len M2) = dom M2 )
by A41, FINSEQ_1:82, FINSEQ_1:def 3;
then A53:
Line M,
(iL + (len M1)) = ((width M1) |-> d) ^ (Line M2,iL)
by A37;
A54:
min (Len <*M1,M2*>),
(iL + (len M1)) = 2
by A9, Th10, A3, A10, A52;
now per cases
( j <= width M1 or j > width M1 )
;
suppose A55:
j <= width M1
;
:: thesis: (block_diagonal <*M1,M2*>,d) * i,j = (((width M1) |-> d) ^ (Line M2,iL)) . jthen A56:
(
j in dom ((width M1) |-> d) &
j in Seg (width M1) &
width M1 <> 0 )
by A41, A42, FINSEQ_1:3, FINSEQ_3:27;
thus (block_diagonal <*M1,M2*>,d) * i,
j =
d
by A9, A10, A38, A39, A55, A54, Def5, A3
.=
((width M1) |-> d) . j
by A56, FINSEQ_2:71
.=
(((width M1) |-> d) ^ (Line M2,iL)) . j
by A56, FINSEQ_1:def 7
;
:: thesis: verum end; suppose A57:
j > width M1
;
:: thesis: (block_diagonal <*M1,M2*>,d) * i,j = (((width M1) |-> d) ^ (Line M2,iL)) . jthen A58:
( not
j in dom (Line M1,i) &
dom ((Line M1,i) ^ ((width M2) |-> d)) = Seg (width (block_diagonal <*M1,M2*>,d)) &
len (Line M2,iL) = width M2 )
by A3, A42, FINSEQ_1:def 3, FINSEQ_3:27, MATRIX_1:def 8;
then consider k being
Nat such that A59:
(
k in dom ((width M2) |-> d) &
j = (width M1) + k )
by A40, A42, FINSEQ_1:38;
A60:
(
dom ((width M2) |-> d) = Seg (width M2) &
dom ((width M2) |-> d) = dom (Line M2,iL) )
by A42, A58, FINSEQ_1:def 3, FINSEQ_3:31;
thus (block_diagonal <*M1,M2*>,d) * i,
j =
(<*M1,M2*> . 2) * ((iL + (len M1)) -' (len M1)),
(j -' (width M1))
by A3, A9, A10, A11, A38, A39, A41, A57, A54, Def5
.=
(<*M1,M2*> . 2) * iL,
(j -' (width M1))
by NAT_D:34
.=
(<*M1,M2*> . ((len <*M1*>) + 1)) * iL,
k
by A5, A59, NAT_D:34
.=
M2 * iL,
k
by FINSEQ_1:59
.=
(Line M2,iL) . k
by A60, A59, MATRIX_1:def 8
.=
(((width M1) |-> d) ^ (Line M2,iL)) . j
by A42, A59, A60, FINSEQ_1:def 7
;
:: thesis: verum end; hence
M * i,
j = (block_diagonal <*M1,M2*>,d) * i,
j
by A53, A3, A4, A40, MATRIX_1:def 8;
:: thesis: verum 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