let K be Field; for a, a1 being Element of K
for G being FinSequence_of_Matrix of K holds a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
let a, a1 be Element of K; for G being FinSequence_of_Matrix of K holds a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
let G be FinSequence_of_Matrix of K; a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
defpred S1[ Nat] means for a, a1 being Element of K
for G being FinSequence_of_Matrix of K st len G = $1 holds
a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1));
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let a,
a1 be
Element of
K;
for G being FinSequence_of_Matrix of K st len G = n + 1 holds
a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))let G be
FinSequence_of_Matrix of
K;
( len G = n + 1 implies a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1)) )
assume A3:
len G = n + 1
;
a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
A4:
G = (G | n) ^ <*(G . (n + 1))*>
by A3, FINSEQ_3:55;
n <= n + 1
by NAT_1:13;
then A5:
len (G | n) = n
by A3, FINSEQ_1:59;
1
in Seg 1
;
then
1
in dom <*a*>
by FINSEQ_1:def 8;
then A6:
<*a*> . 1
= <*a*> /. 1
by PARTFUN1:def 6;
A7:
<*a*> . 1
= a
by FINSEQ_1:def 8;
A8:
len <*a*> = 1
by FINSEQ_1:39;
A9:
len <*(G . (n + 1))*> = 1
by FINSEQ_1:39;
A10:
len (n |-> a) = n
by CARD_1:def 7;
(n + 1) |-> a = (n |-> a) ^ <*a*>
by FINSEQ_2:60;
hence block_diagonal (
(mlt (((len G) |-> a),G)),
(a * a1)) =
block_diagonal (
((mlt ((n |-> a),(G | n))) ^ (mlt (<*a*>,<*(G . (n + 1))*>))),
(a * a1))
by A3, A4, A5, A10, A9, A8, Th64
.=
block_diagonal (
((mlt ((n |-> a),(G | n))) ^ <*(a * (G . (n + 1)))*>),
(a * a1))
by A6, A7, Th63
.=
block_diagonal (
(<*(block_diagonal ((mlt ((n |-> a),(G | n))),(a * a1)))*> ^ <*(a * (G . (n + 1)))*>),
(a * a1))
by Th35
.=
block_diagonal (
<*(a * (block_diagonal ((G | n),a1))),(a * (G . (n + 1)))*>,
(a * a1))
by A2, A5
.=
a * (block_diagonal (<*(block_diagonal ((G | n),a1)),(G . (n + 1))*>,a1))
by Lm7
.=
a * (block_diagonal (G,a1))
by A4, Th35
;
verum
end;
A11:
S1[ 0 ]
proof
let a,
a1 be
Element of
K;
for G being FinSequence_of_Matrix of K st len G = 0 holds
a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))let G be
FinSequence_of_Matrix of
K;
( len G = 0 implies a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1)) )
assume A12:
len G = 0
;
a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
dom (mlt (((len G) |-> a),G)) = dom G
by Def9;
then
len (mlt (((len G) |-> a),G)) = len G
by FINSEQ_3:29;
then
Len (mlt (((len G) |-> a),G)) = {}
by A12;
then
len (block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))) = 0
by Def5, RVSUM_1:72;
then A13:
block_diagonal (
(mlt (((len G) |-> a),G)),
(a * a1))
= {}
;
Len G = {}
by A12;
then
len (block_diagonal (G,a1)) = 0
by Def5, RVSUM_1:72;
then
len (a * (block_diagonal (G,a1))) = 0
by MATRIX_3:def 5;
hence
a * (block_diagonal (G,a1)) = block_diagonal (
(mlt (((len G) |-> a),G)),
(a * a1))
by A13;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A11, A1);
hence
a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
; verum