let K be Field; for a, a1 being Element of K
for A1, A2 being Matrix of K holds a * (block_diagonal (<*A1,A2*>,a1)) = block_diagonal (<*(a * A1),(a * A2)*>,(a * a1))
let a, a1 be Element of K; for A1, A2 being Matrix of K holds a * (block_diagonal (<*A1,A2*>,a1)) = block_diagonal (<*(a * A1),(a * A2)*>,(a * a1))
let A1, A2 be Matrix of K; a * (block_diagonal (<*A1,A2*>,a1)) = block_diagonal (<*(a * A1),(a * A2)*>,(a * a1))
set AA1 = a * A1;
set AA2 = a * A2;
set aa1 = a * a1;
set B = block_diagonal (<*A1,A2*>,a1);
A1:
width (a * A2) = width A2
by MATRIX_3:def 5;
A2:
width (a * A1) = width A1
by MATRIX_3:def 5;
then A3:
Sum (Width <*(a * A1),(a * A2)*>) = (width A1) + (width A2)
by A1, Th20;
A4:
len (block_diagonal (<*A1,A2*>,a1)) = Sum (Len <*A1,A2*>)
by Def5;
A5:
len (a * A2) = len A2
by MATRIX_3:def 5;
then A6:
dom (a * A2) = dom A2
by FINSEQ_3:29;
A7:
Sum (Width <*A1,A2*>) = (width A1) + (width A2)
by Th20;
A8:
Sum (Len <*A1,A2*>) = (len A1) + (len A2)
by Th16;
A9:
len (a * A1) = len A1
by MATRIX_3:def 5;
then A10:
dom (a * A1) = dom A1
by FINSEQ_3:29;
A11:
now for i being Nat holds
( ( i in dom (a * A1) implies Line ((a * (block_diagonal (<*A1,A2*>,a1))),i) = (Line ((a * A1),i)) ^ ((width (a * A2)) |-> (a * a1)) ) & ( i in dom (a * A2) implies Line ((a * (block_diagonal (<*A1,A2*>,a1))),(i + (len (a * A1)))) = ((width (a * A1)) |-> (a * a1)) ^ (Line ((a * A2),i)) ) )let i be
Nat;
( ( i in dom (a * A1) implies Line ((a * (block_diagonal (<*A1,A2*>,a1))),i) = (Line ((a * A1),i)) ^ ((width (a * A2)) |-> (a * a1)) ) & ( i in dom (a * A2) implies Line ((a * (block_diagonal (<*A1,A2*>,a1))),(i + (len (a * A1)))) = ((width (a * A1)) |-> (a * a1)) ^ (Line ((a * A2),i)) ) )thus
(
i in dom (a * A1) implies
Line (
(a * (block_diagonal (<*A1,A2*>,a1))),
i)
= (Line ((a * A1),i)) ^ ((width (a * A2)) |-> (a * a1)) )
( i in dom (a * A2) implies Line ((a * (block_diagonal (<*A1,A2*>,a1))),(i + (len (a * A1)))) = ((width (a * A1)) |-> (a * a1)) ^ (Line ((a * A2),i)) )proof
assume A12:
i in dom (a * A1)
;
Line ((a * (block_diagonal (<*A1,A2*>,a1))),i) = (Line ((a * A1),i)) ^ ((width (a * A2)) |-> (a * a1))
then A13:
1
<= i
by FINSEQ_3:25;
A14:
i <= len A1
by A9, A12, FINSEQ_3:25;
len A1 <= len (block_diagonal (<*A1,A2*>,a1))
by A8, A4, NAT_1:11;
then
i <= len (block_diagonal (<*A1,A2*>,a1))
by A14, XXREAL_0:2;
hence Line (
(a * (block_diagonal (<*A1,A2*>,a1))),
i) =
a * (Line ((block_diagonal (<*A1,A2*>,a1)),i))
by A13, MATRIXR1:20
.=
a * ((Line (A1,i)) ^ ((width A2) |-> a1))
by A10, A12, Th23
.=
(a * (Line (A1,i))) ^ (a * ((width A2) |-> a1))
by MATRIX15:4
.=
(Line ((a * A1),i)) ^ (a * ((width A2) |-> a1))
by A13, A14, MATRIXR1:20
.=
(Line ((a * A1),i)) ^ ((width (a * A2)) |-> (a * a1))
by A1, FVSUM_1:53
;
verum
end; thus
(
i in dom (a * A2) implies
Line (
(a * (block_diagonal (<*A1,A2*>,a1))),
(i + (len (a * A1))))
= ((width (a * A1)) |-> (a * a1)) ^ (Line ((a * A2),i)) )
verumproof
assume A15:
i in dom (a * A2)
;
Line ((a * (block_diagonal (<*A1,A2*>,a1))),(i + (len (a * A1)))) = ((width (a * A1)) |-> (a * a1)) ^ (Line ((a * A2),i))
then A16:
1
<= i
by FINSEQ_3:25;
then A17:
0 + 1
<= i + (len A1)
by XREAL_1:7;
A18:
i <= len A2
by A5, A15, FINSEQ_3:25;
then
i + (len A1) <= len (block_diagonal (<*A1,A2*>,a1))
by A8, A4, XREAL_1:7;
hence Line (
(a * (block_diagonal (<*A1,A2*>,a1))),
(i + (len (a * A1)))) =
a * (Line ((block_diagonal (<*A1,A2*>,a1)),(i + (len A1))))
by A9, A17, MATRIXR1:20
.=
a * (((width A1) |-> a1) ^ (Line (A2,i)))
by A6, A15, Th23
.=
(a * ((width A1) |-> a1)) ^ (a * (Line (A2,i)))
by MATRIX15:4
.=
((width A1) |-> (a * a1)) ^ (a * (Line (A2,i)))
by FVSUM_1:53
.=
((width (a * A1)) |-> (a * a1)) ^ (Line ((a * A2),i))
by A2, A16, A18, MATRIXR1:20
;
verum
end; end;
Sum (Len <*(a * A1),(a * A2)*>) = (len A1) + (len A2)
by A9, A5, Th16;
hence
a * (block_diagonal (<*A1,A2*>,a1)) = block_diagonal (<*(a * A1),(a * A2)*>,(a * a1))
by A8, A3, A7, A11, Th23; verum