let K be Field; for a1, a2 being Element of K
for A1, A2, B1, B2 being Matrix of K st len A1 = len B1 & len A2 = len B2 & width A1 = width B1 & width A2 = width B2 holds
(block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))
let a1, a2 be Element of K; for A1, A2, B1, B2 being Matrix of K st len A1 = len B1 & len A2 = len B2 & width A1 = width B1 & width A2 = width B2 holds
(block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))
let A1, A2, B1, B2 be Matrix of K; ( len A1 = len B1 & len A2 = len B2 & width A1 = width B1 & width A2 = width B2 implies (block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)) )
assume that
A1:
len A1 = len B1
and
A2:
len A2 = len B2
and
A3:
width A1 = width B1
and
A4:
width A2 = width B2
; (block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))
set b12 = <*B1,B2*>;
set a12 = <*A1,A2*>;
set AB2 = A2 + B2;
set AB1 = A1 + B1;
set ab = <*A1,A2*> (+) <*B1,B2*>;
set bA = block_diagonal (<*A1,A2*>,a1);
set bB = block_diagonal (<*B1,B2*>,a2);
set bAB = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2));
A5:
len ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) = len (block_diagonal (<*A1,A2*>,a1))
by MATRIX_3:def 3;
width ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) = width (block_diagonal (<*A1,A2*>,a1))
by MATRIX_3:def 3;
then reconsider bAbB = (block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) as Matrix of len (block_diagonal (<*A1,A2*>,a1)), width (block_diagonal (<*A1,A2*>,a1)),K by A5, MATRIX_0:51;
A6:
len (A1 + B1) = len A1
by MATRIX_3:def 3;
A7:
len (block_diagonal (<*A1,A2*>,a1)) = Sum (Len <*A1,A2*>)
by Def5;
A8:
Sum (Len <*A1,A2*>) = (len A1) + (len A2)
by Th16;
A9:
len (A2 + B2) = len A2
by MATRIX_3:def 3;
A10:
Sum (Width <*B1,B2*>) = (width B1) + (width B2)
by Th20;
A11:
len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) = Sum (Len (<*A1,A2*> (+) <*B1,B2*>))
by Def5;
A12:
width (block_diagonal (<*B1,B2*>,a2)) = Sum (Width <*B1,B2*>)
by Def5;
A13:
width (block_diagonal (<*A1,A2*>,a1)) = Sum (Width <*A1,A2*>)
by Def5;
A14:
width (A2 + B2) = width A2
by MATRIX_3:def 3;
A15:
width (A1 + B1) = width A1
by MATRIX_3:def 3;
A16:
Len (<*A1,A2*> (+) <*B1,B2*>) = Len <*A1,A2*>
by Th66;
A17:
<*A1,A2*> (+) <*B1,B2*> = <*(A1 + B1),(A2 + B2)*>
by Th70;
now for i being Nat st 1 <= i & i <= len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) holds
(block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) . iA18:
dom (block_diagonal (<*A1,A2*>,a1)) = Seg (len (block_diagonal (<*A1,A2*>,a1)))
by FINSEQ_1:def 3;
let i be
Nat;
( 1 <= i & i <= len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) implies (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) . i )assume that A19:
1
<= i
and A20:
i <= len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)))
;
(block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) . iA21:
i in Seg (len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))))
by A19, A20;
then A22:
(block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = Line (
(block_diagonal (<*(A1 + B1),(A2 + B2)*>,(a1 + a2))),
i)
by A17, A11, MATRIX_0:52;
A23:
bAbB . i = Line (
((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))),
i)
by A16, A7, A11, A21, MATRIX_0:52;
A24:
dom (A1 ^ A2) = Seg (len (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))))
by A8, A16, A11, FINSEQ_1:def 7;
now (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = bAbB . iper cases
( i in dom A1 or ex n being Nat st
( n in dom A2 & i = (len A1) + n ) )
by A21, A24, FINSEQ_1:25;
suppose A25:
i in dom A1
;
(block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = bAbB . iA26:
len (Line (B1,i)) = width B1
by CARD_1:def 7;
A27:
dom A1 = dom B1
by A1, FINSEQ_3:29;
A28:
len (Line (A1,i)) = width A1
by CARD_1:def 7;
dom A1 = dom (A1 + B1)
by A6, FINSEQ_3:29;
hence (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i =
(Line ((A1 + B1),i)) ^ ((width (A2 + B2)) |-> (a1 + a2))
by A22, A25, Th23
.=
((Line (A1,i)) + (Line (B1,i))) ^ ((width (A2 + B2)) |-> (a1 + a2))
by A3, A25, Lm8
.=
((Line (A1,i)) + (Line (B1,i))) ^ (((width (A2 + B2)) |-> a1) + ((width (A2 + B2)) |-> a2))
by FVSUM_1:20
.=
((Line (A1,i)) ^ ((width A2) |-> a1)) + ((Line (B1,i)) ^ ((width B2) |-> a2))
by A3, A4, A14, A28, A26, Th1
.=
(Line ((block_diagonal (<*A1,A2*>,a1)),i)) + ((Line (B1,i)) ^ ((width B2) |-> a2))
by A25, Th23
.=
(Line ((block_diagonal (<*A1,A2*>,a1)),i)) + (Line ((block_diagonal (<*B1,B2*>,a2)),i))
by A25, A27, Th23
.=
bAbB . i
by A3, A4, A10, A16, A7, A13, A12, A11, A21, A18, A23, Lm8, Th20
;
verum end; suppose A29:
ex
n being
Nat st
(
n in dom A2 &
i = (len A1) + n )
;
(block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = bAbB . iA30:
len ((width (A1 + B1)) |-> a1) = width (A1 + B1)
by CARD_1:def 7;
A31:
dom A2 = dom B2
by A2, FINSEQ_3:29;
A32:
len ((width (A1 + B1)) |-> a2) = width (A1 + B1)
by CARD_1:def 7;
consider n being
Nat such that A33:
n in dom A2
and A34:
i = (len A1) + n
by A29;
dom A2 = dom (A2 + B2)
by A9, FINSEQ_3:29;
hence (block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i =
((width (A1 + B1)) |-> (a1 + a2)) ^ (Line ((A2 + B2),n))
by A6, A22, A33, A34, Th23
.=
((width (A1 + B1)) |-> (a1 + a2)) ^ ((Line (A2,n)) + (Line (B2,n)))
by A4, A33, Lm8
.=
(((width (A1 + B1)) |-> a1) + ((width (A1 + B1)) |-> a2)) ^ ((Line (A2,n)) + (Line (B2,n)))
by FVSUM_1:20
.=
(((width (A1 + B1)) |-> a1) ^ (Line (A2,n))) + (((width (A1 + B1)) |-> a2) ^ (Line (B2,n)))
by A30, A32, Th1
.=
(Line ((block_diagonal (<*A1,A2*>,a1)),i)) + (((width B1) |-> a2) ^ (Line (B2,n)))
by A3, A15, A33, A34, Th23
.=
(Line ((block_diagonal (<*A1,A2*>,a1)),i)) + (Line ((block_diagonal (<*B1,B2*>,a2)),i))
by A1, A33, A34, A31, Th23
.=
bAbB . i
by A3, A4, A10, A16, A7, A13, A12, A11, A21, A18, A23, Lm8, Th20
;
verum end; hence
(block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))) . i = ((block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2))) . i
;
verum end;
hence
(block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))
by A16, A7, A11, A5; verum