let K be Field; :: thesis: for R1, R2 being FinSequence_of_Square-Matrix of K st Width R1 = Len R2 holds
(block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) = block_diagonal (R1 (#) R2),(0. K)
let R1, R2 be FinSequence_of_Square-Matrix of K; :: thesis: ( Width R1 = Len R2 implies (block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) = block_diagonal (R1 (#) R2),(0. K) )
defpred S1[ Nat] means for R1, R2 being FinSequence_of_Square-Matrix of K st Width R1 = Len R2 & len R1 = $1 holds
(block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) = block_diagonal (R1 (#) R2),(0. K);
A1:
S1[ 0 ]
proof
let R1,
R2 be
FinSequence_of_Square-Matrix of
K;
:: thesis: ( Width R1 = Len R2 & len R1 = 0 implies (block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) = block_diagonal (R1 (#) R2),(0. K) )
assume A2:
(
Width R1 = Len R2 &
len R1 = 0 )
;
:: thesis: (block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) = block_diagonal (R1 (#) R2),(0. K)
set b1 =
block_diagonal R1,
(0. K);
set b2 =
block_diagonal R2,
(0. K);
set b12 =
block_diagonal (R1 (#) R2),
(0. K);
(
len R1 = len (Width R1) &
len R1 = len (Len R1) )
by FINSEQ_1:def 18;
then
(
Len R1 = {} &
Len R2 = {} &
Len R1 = Len (R1 (#) R2) )
by A2, Th73;
then
(
len (block_diagonal R1,(0. K)) = 0 &
len (block_diagonal R2,(0. K)) = 0 &
len (block_diagonal (R1 (#) R2),(0. K)) = 0 &
Sum (Width R1) = width (block_diagonal R1,(0. K)) &
Sum (Width R1) = 0 )
by Def5, Th13, RVSUM_1:102;
then
(
len ((block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K))) = 0 &
block_diagonal (R1 (#) R2),
(0. K) = {} )
by MATRIX_3:def 4;
hence
(block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) = block_diagonal (R1 (#) R2),
(0. K)
;
:: thesis: verum
end;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
:: thesis: S1[n + 1]
set n1 =
n + 1;
let R1,
R2 be
FinSequence_of_Square-Matrix of
K;
:: thesis: ( Width R1 = Len R2 & len R1 = n + 1 implies (block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) = block_diagonal (R1 (#) R2),(0. K) )
assume A5:
(
Width R1 = Len R2 &
len R1 = n + 1 )
;
:: thesis: (block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) = block_diagonal (R1 (#) R2),(0. K)
A6:
len R1 =
len (Len R2)
by A5, FINSEQ_1:def 18
.=
len R2
by FINSEQ_1:def 18
;
set R1n =
R1 | n;
set R2n =
R2 | n;
set b1n =
block_diagonal (R1 | n),
(0. K);
set b2n =
block_diagonal (R2 | n),
(0. K);
A7:
(
len (R1 | n) = n &
len (R2 | n) = n )
by A5, A6, FINSEQ_1:80, NAT_1:11;
A8:
Width (R1 | n) =
(Width R1) | n
by Th21
.=
Len (R2 | n)
by A5, Th17
;
A9:
width (block_diagonal (R1 | n),(0. K)) =
Sum (Width (R1 | n))
by Def5
.=
len (block_diagonal (R2 | n),(0. K))
by A8, Def5
;
A10:
(
n + 1
in Seg (n + 1) &
dom (Width R1) = Seg (n + 1) &
dom (Width R1) = dom (Len R2) )
by A5, FINSEQ_1:6, FINSEQ_2:144;
then A11:
width (R1 . (n + 1)) =
(Len R2) . (n + 1)
by A5, Def4
.=
len (R2 . (n + 1))
by A10, Def3
;
A12:
(
R1 = (R1 | n) ^ <*(R1 . (n + 1))*> &
R2 = (R2 | n) ^ <*(R2 . (n + 1))*> )
by A5, A6, FINSEQ_3:61;
thus (block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) =
(block_diagonal <*(block_diagonal (R1 | n),(0. K)),(R1 . (n + 1))*>,(0. K)) * (block_diagonal ((R2 | n) ^ <*(R2 . (n + 1))*>),(0. K))
by A12, Th35
.=
(block_diagonal <*(block_diagonal (R1 | n),(0. K)),(R1 . (n + 1))*>,(0. K)) * (block_diagonal <*(block_diagonal (R2 | n),(0. K)),(R2 . (n + 1))*>,(0. K))
by Th35
.=
block_diagonal (<*(block_diagonal (R1 | n),(0. K)),(R1 . (n + 1))*> (#) <*(block_diagonal (R2 | n),(0. K)),(R2 . (n + 1))*>),
(0. K)
by A9, A11, Th78
.=
block_diagonal <*((block_diagonal (R1 | n),(0. K)) * (block_diagonal (R2 | n),(0. K))),((R1 . (n + 1)) * (R2 . (n + 1)))*>,
(0. K)
by Th77
.=
block_diagonal <*(block_diagonal ((R1 | n) (#) (R2 | n)),(0. K)),((R1 . (n + 1)) * (R2 . (n + 1)))*>,
(0. K)
by A4, A7, A8
.=
block_diagonal (((R1 | n) (#) (R2 | n)) ^ <*((R1 . (n + 1)) * (R2 . (n + 1)))*>),
(0. K)
by Th35
.=
block_diagonal (((R1 | n) (#) (R2 | n)) ^ (<*(R1 . (n + 1))*> (#) <*(R2 . (n + 1))*>)),
(0. K)
by Th76
.=
block_diagonal (R1 (#) R2),
(0. K)
by A12, A7, Th74
;
:: thesis: verum
end;
A13:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A3);
assume
Width R1 = Len R2
; :: thesis: (block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) = block_diagonal (R1 (#) R2),(0. K)
hence
(block_diagonal R1,(0. K)) * (block_diagonal R2,(0. K)) = block_diagonal (R1 (#) R2),(0. K)
by A13; :: thesis: verum