let K be Field; :: thesis: 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; :: thesis: 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; :: thesis: 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:
S1[ 0 ]
proof
let a,
a1 be
Element of
K;
:: thesis: 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;
:: thesis: ( len G = 0 implies a * (block_diagonal G,a1) = block_diagonal (mlt ((len G) |-> a),G),(a * a1) )
assume A2:
len G = 0
;
:: thesis: 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 (Len G) = len G &
len (Len (mlt ((len G) |-> a),G)) = len (mlt ((len G) |-> a),G) &
len (mlt ((len G) |-> a),G) = len G )
by FINSEQ_1:def 18, FINSEQ_3:31;
then
(
Len G = {} &
Len (mlt ((len G) |-> a),G) = {} )
by A2;
then
(
len (block_diagonal G,a1) = 0 &
len (block_diagonal (mlt ((len G) |-> a),G),(a * a1)) = 0 )
by Def5, RVSUM_1:102;
then
(
len (a * (block_diagonal G,a1)) = 0 &
block_diagonal (mlt ((len G) |-> a),G),
(a * a1) = {} )
by MATRIX_3:def 5;
hence
a * (block_diagonal G,a1) = block_diagonal (mlt ((len G) |-> a),G),
(a * a1)
;
:: 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 a,
a1 be
Element of
K;
:: thesis: 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;
:: thesis: ( len G = n + 1 implies a * (block_diagonal G,a1) = block_diagonal (mlt ((len G) |-> a),G),(a * a1) )
assume A5:
len G = n + 1
;
:: thesis: a * (block_diagonal G,a1) = block_diagonal (mlt ((len G) |-> a),G),(a * a1)
set M =
mlt ((len G) |-> a),
G;
1
in Seg 1
;
then
1
in dom <*a*>
by FINSEQ_1:def 8;
then A6:
(
<*a*> . 1
= <*a*> /. 1 &
<*a*> . 1
= a )
by FINSEQ_1:def 8, PARTFUN1:def 8;
n <= n + 1
by NAT_1:13;
then A7:
(
G = (G | n) ^ <*(G . (n + 1))*> &
(n + 1) |-> a = (n |-> a) ^ <*a*> &
len (G | n) = n &
len (n |-> a) = n &
len <*(G . (n + 1))*> = 1 &
len <*a*> = 1 )
by A5, FINSEQ_1:56, FINSEQ_1:80, FINSEQ_1:def 18, FINSEQ_2:74, FINSEQ_3:61;
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 A5, Th64
.=
block_diagonal ((mlt (n |-> a),(G | n)) ^ <*(a * (G . (n + 1)))*>),
(a * a1)
by Th63, A6
.=
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 A4, A7
.=
a * (block_diagonal <*(block_diagonal (G | n),a1),(G . (n + 1))*>,a1)
by Lm7
.=
a * (block_diagonal G,a1)
by A7, Th35
;
:: thesis: verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A3);
hence
a * (block_diagonal G,a1) = block_diagonal (mlt ((len G) |-> a),G),(a * a1)
; :: thesis: verum