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;
( Sum (Len <*M1,M2*>) = 0 implies Sum (Width <*M1,M2*>) = 0 )
by Th13;
then A1:
( len M = Sum (Len <*M1,M2*>) & width M = Sum (Width <*M1,M2*>) )
by MATRIX13:1;
A2:
( Sum (Len <*M1,M2*>) = (len M1) + (len M2) & Sum (Width <*M1,M2*>) = (width M1) + (width M2) )
by Th16, Th20;
then
( width M1 <= width M & len M1 <= len M )
by A1, NAT_1:12;
then A3:
( Seg (width M1) c= Seg (width M) & Seg (len M1) c= Seg (len M) & Seg (len M) = dom M & Seg (len M1) = dom M1 & dom M2 = Seg (len M2) )
by FINSEQ_1:7, FINSEQ_1:def 3;
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
assume A4:
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 CMi =
Col M,
(i + (width M1));
set CM1 =
Col M1,
i;
set CM2 =
Col M2,
i;
set L1 =
(len M1) |-> d;
set L2 =
(len M2) |-> d;
A5:
(
len (Col M,i) = len M &
len (Col M,(i + (width M1))) = len M &
len (Col M1,i) = len M1 &
len (Col M2,i) = len M2 &
len ((len M1) |-> d) = len M1 &
len ((len M2) |-> d) = len M2 )
by FINSEQ_1:def 18;
then A6:
(
dom (Col M1,i) = dom M1 &
dom (Col M2,i) = dom M2 &
dom ((len M1) |-> d) = dom M1 &
dom ((len M2) |-> d) = dom M2 &
dom ((width M1) |-> d) = Seg (width M1) &
dom ((width M2) |-> d) = Seg (width M2) &
dom ((len M2) |-> d) = Seg (len M2) &
dom ((len M1) |-> d) = Seg (len M1) )
by FINSEQ_2:144, 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 A7:
i in Seg (width M1)
;
:: thesis: Col M,i = (Col M1,i) ^ ((len M2) |-> d)
A8:
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 A9:
( 1
<= j &
j <= len (Col M,i) )
;
:: thesis: ((Col M1,i) ^ ((len M2) |-> d)) . j = (Col M,i) . jA10:
dom (Line M1,j) = Seg (width M1)
by FINSEQ_2:144;
A11:
(
j in dom ((Col M1,i) ^ ((len M2) |-> d)) &
j in dom M )
by A8, A9, A2, A1, A5, FINSEQ_3:27;
then A12:
(Col M,i) . j = (Line M,j) . i
by A7, A3, GOBOARD1:17;
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 A11, FINSEQ_1:38;
suppose A13:
j in dom (Col M1,i)
;
:: thesis: (Col M,i) . j = ((Col M1,i) ^ ((len M2) |-> d)) . jhence (Col M,i) . j =
((Line M1,j) ^ ((width M2) |-> d)) . i
by A6, A4, A12, Th23
.=
(Line M1,j) . i
by A7, A10, FINSEQ_1:def 7
.=
(Col M1,i) . j
by A7, A6, A13, GOBOARD1:17
.=
((Col M1,i) ^ ((len M2) |-> d)) . j
by A13, 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)) . jthen consider k being
Nat such that A14:
(
k in dom ((len M2) |-> d) &
j = (len (Col M1,i)) + k )
;
thus (Col M,i) . j =
(((width M1) |-> d) ^ (Line M2,k)) . i
by A5, A6, A4, A12, A14, Th23
.=
((width M1) |-> d) . i
by A7, A6, FINSEQ_1:def 7
.=
d
by A7, FINSEQ_2:71
.=
((len M2) |-> d) . k
by A14, A6, FINSEQ_2:71
.=
((Col M1,i) ^ ((len M2) |-> d)) . j
by A14, FINSEQ_1:def 7
;
:: thesis: verum 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 A8, A2, A1, A5, FINSEQ_1:18;
:: thesis: verum
end;
assume A15:
i in Seg (width M2)
;
:: thesis: Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i)
A16:
len (((len M1) |-> d) ^ (Col M2,i)) = (len ((len M1) |-> d)) + (len (Col M2,i))
by FINSEQ_1:35;
now 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 A17:
( 1
<= j &
j <= len (Col M,(i + (width M1))) )
;
:: thesis: (((len M1) |-> d) ^ (Col M2,i)) . j = (Col M,(i + (width M1))) . jA18:
i + (width M1) in Seg (width M)
by A1, A2, A15, FINSEQ_1:81;
A19:
(
len (Line M1,j) = width M1 &
len ((width M1) |-> d) = width M1 )
by FINSEQ_1:def 18, MATRIX_1:def 8;
A20:
(
j in dom (((len M1) |-> d) ^ (Col M2,i)) &
j in dom M )
by A16, A17, A2, A1, A5, FINSEQ_3:27;
then A21:
(Col M,(i + (width M1))) . j = (Line M,j) . (i + (width M1))
by A18, GOBOARD1:17;
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 A20, FINSEQ_1:38;
suppose A22:
j in dom ((len M1) |-> d)
;
:: thesis: (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 A6, A4, A21, Th23
.=
((width M2) |-> d) . i
by A19, A15, A6, FINSEQ_1:def 7
.=
d
by A15, FINSEQ_2:71
.=
((len M1) |-> d) . j
by A22, A6, FINSEQ_2:71
.=
(((len M1) |-> d) ^ (Col M2,i)) . j
by A22, 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)) . jthen consider k being
Nat such that A23:
(
k in dom (Col M2,i) &
j = (len ((len M1) |-> d)) + k )
;
A24:
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 A5, A6, A4, A21, A23, Th23
.=
(Line M2,k) . i
by A24, A19, A15, FINSEQ_1:def 7
.=
(Col M2,i) . k
by A15, A6, A23, GOBOARD1:17
.=
(((len M1) |-> d) ^ (Col M2,i)) . j
by A23, FINSEQ_1:def 7
;
:: thesis: verum 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 A16, A2, A1, A5, FINSEQ_1:18;
:: thesis: verum
end;
assume A25:
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
now 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;
set W1 =
(width M1) |-> d;
set W2 =
(width M2) |-> d;
A26:
(
len (Line M,i) = width M &
len (Line M,(i + (len M1))) = width M &
len (Line M1,i) = width M1 &
len (Line M2,i) = width M2 &
len ((width M1) |-> d) = width M1 &
len ((width M2) |-> d) = width M2 )
by FINSEQ_1:def 18;
then A27:
(
dom (Line M,i) = Seg (width M) &
dom (Line M1,i) = Seg (width M1) &
dom (Line M2,i) = Seg (width M2) &
dom ((width M2) |-> d) = Seg (width M2) &
dom ((width M1) |-> d) = 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 A28:
i in dom M1
;
:: thesis: Line M,i = (Line M1,i) ^ ((width M2) |-> d)
A29:
len ((Line M1,i) ^ ((width M2) |-> d)) = (len (Line M1,i)) + (len ((width M2) |-> d))
by FINSEQ_1:35;
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 A30:
( 1
<= j &
j <= len (Line M,i) )
;
:: thesis: (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . jA31:
(
j in Seg (width M) &
j in dom ((Line M1,i) ^ ((width M2) |-> d)) )
by A1, A2, A26, A27, A29, A30, FINSEQ_3:27;
then A32:
(Line M,i) . j = (Col M,j) . i
by A3, A28, GOBOARD1:17;
A33:
(
dom (Col M1,j) = Seg (len M1) &
dom ((len M1) |-> d) = Seg (len M1) )
by FINSEQ_2:144;
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 A31, FINSEQ_1:38;
suppose A34:
j in dom (Line M1,i)
;
:: thesis: (Line M,i) . j = ((Line M1,i) ^ ((width M2) |-> d)) . jhence (Line M,i) . j =
((Col M1,j) ^ ((len M2) |-> d)) . i
by A25, A27, A32
.=
(Col M1,j) . i
by A28, A3, A33, FINSEQ_1:def 7
.=
(Line M1,i) . j
by A28, A27, A34, GOBOARD1:17
.=
((Line M1,i) ^ ((width M2) |-> d)) . j
by A34, 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)) . jthen consider n being
Nat such that A35:
(
n in dom ((width M2) |-> d) &
j = (len (Line M1,i)) + n )
;
thus (Line M,i) . j =
(((len M1) |-> d) ^ (Col M2,n)) . i
by A25, A27, A32, A26, A35
.=
((len M1) |-> d) . i
by A28, A3, A33, FINSEQ_1:def 7
.=
d
by A28, A3, FINSEQ_2:71
.=
((width M2) |-> d) . n
by A27, A35, FINSEQ_2:71
.=
((Line M1,i) ^ ((width M2) |-> d)) . j
by A35, 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 A29, A2, A1, A26, 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
assume A36:
i in dom M2
;
:: thesis: Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i)
A37:
len (((width M1) |-> d) ^ (Line M2,i)) = (len ((width M1) |-> d)) + (len (Line M2,i))
by FINSEQ_1:35;
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 A38:
( 1
<= j &
j <= len (Line M,(i + (len M1))) )
;
:: thesis: (Line M,(i + (len M1))) . j = (((width M1) |-> d) ^ (Line M2,i)) . j
dom M2 = Seg (len M2)
by FINSEQ_1:def 3;
then A39:
i + (len M1) in Seg (len M)
by A36, A1, A2, FINSEQ_1:81;
A40:
(
j in Seg (width M) &
j in dom (((width M1) |-> d) ^ (Line M2,i)) )
by A1, A2, A26, A27, A37, A38, FINSEQ_3:27;
then A41:
(Line M,(i + (len M1))) . j = (Col M,j) . (i + (len M1))
by A3, A39, GOBOARD1:17;
A42:
(
len (Col M1,j) = len M1 &
dom ((len M2) |-> d) = Seg (len M2) &
len ((len M1) |-> d) = len M1 )
by FINSEQ_1:def 18, FINSEQ_2:144;
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 A40, FINSEQ_1:38;
suppose A43:
j in dom ((width M1) |-> d)
;
:: thesis: (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 A25, A27, A41
.=
((len M2) |-> d) . i
by A36, A42, A3, FINSEQ_1:def 7
.=
d
by A36, A3, FINSEQ_2:71
.=
((width M1) |-> d) . j
by A43, A27, FINSEQ_2:71
.=
(((width M1) |-> d) ^ (Line M2,i)) . j
by A43, 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)) . jthen consider n being
Nat such that A44:
(
n in dom (Line M2,i) &
j = (len ((width M1) |-> d)) + n )
;
A45:
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 A25, A26, A27, A41, A44
.=
(Col M2,n) . i
by A45, A42, A36, A3, FINSEQ_1:def 7
.=
(Line M2,i) . n
by A36, A27, A44, GOBOARD1:17
.=
(((width M1) |-> d) ^ (Line M2,i)) . j
by A44, 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 A37, A2, A1, A26, FINSEQ_1:18;
:: thesis: verum
end; end;
hence
M = block_diagonal <*M1,M2*>,d
by Th23; :: thesis: verum