let i be Nat; for K being Field
for a being Element of K
for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in dom A & width A = width (DelLine A,i) holds
DelLine (block_diagonal (<*A*> ^ G),a),i = block_diagonal (<*(DelLine A,i)*> ^ G),a
let K be Field; for a being Element of K
for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in dom A & width A = width (DelLine A,i) holds
DelLine (block_diagonal (<*A*> ^ G),a),i = block_diagonal (<*(DelLine A,i)*> ^ G),a
let a be Element of K; for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in dom A & width A = width (DelLine A,i) holds
DelLine (block_diagonal (<*A*> ^ G),a),i = block_diagonal (<*(DelLine A,i)*> ^ G),a
let A be Matrix of K; for G being FinSequence_of_Matrix of K st i in dom A & width A = width (DelLine A,i) holds
DelLine (block_diagonal (<*A*> ^ G),a),i = block_diagonal (<*(DelLine A,i)*> ^ G),a
let G be FinSequence_of_Matrix of K; ( i in dom A & width A = width (DelLine A,i) implies DelLine (block_diagonal (<*A*> ^ G),a),i = block_diagonal (<*(DelLine A,i)*> ^ G),a )
assume that
A1:
i in dom A
and
A2:
width A = width (DelLine A,i)
; DelLine (block_diagonal (<*A*> ^ G),a),i = block_diagonal (<*(DelLine A,i)*> ^ G),a
A3:
i in Seg (len A)
by A1, FINSEQ_1:def 3;
set da = DelLine A,i;
consider m being Nat such that
A4:
len A = m + 1
and
A5:
len (DelLine A,i) = m
by A1, FINSEQ_3:113;
set bG = block_diagonal G,a;
set DA = <*(DelLine A,i)*>;
set AA = <*A*>;
set BG = <*(block_diagonal G,a)*>;
set bAG = block_diagonal <*A,(block_diagonal G,a)*>,a;
set bdAG = block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a;
A6:
Seg (len (block_diagonal <*A,(block_diagonal G,a)*>,a)) = dom (block_diagonal <*A,(block_diagonal G,a)*>,a)
by FINSEQ_1:def 3;
A7:
len (block_diagonal <*A,(block_diagonal G,a)*>,a) = Sum (Len (<*A*> ^ <*(block_diagonal G,a)*>))
by Def5;
then A8:
len (block_diagonal <*A,(block_diagonal G,a)*>,a) = (len A) + (len (block_diagonal G,a))
by Th16;
then
len (block_diagonal <*A,(block_diagonal G,a)*>,a) >= len A
by NAT_1:11;
then A9:
Seg (len A) c= Seg (len (block_diagonal <*A,(block_diagonal G,a)*>,a))
by FINSEQ_1:7;
A10:
len (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a) = Sum (Len (<*(DelLine A,i)*> ^ <*(block_diagonal G,a)*>))
by Def5;
then A11:
len (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a) = m + (len (block_diagonal G,a))
by A5, Th16;
A12:
len (block_diagonal <*A,(block_diagonal G,a)*>,a) = (m + (len (block_diagonal G,a))) + 1
by A4, A8;
A13:
len (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a) = (len (DelLine A,i)) + (len (block_diagonal G,a))
by A10, Th16;
A14:
now
m + (len (block_diagonal G,a)) <= len (block_diagonal <*A,(block_diagonal G,a)*>,a)
by A12, NAT_1:11;
then A15:
Seg (m + (len (block_diagonal G,a))) c= Seg (len (block_diagonal <*A,(block_diagonal G,a)*>,a))
by FINSEQ_1:7;
reconsider da9 =
DelLine A,
i as
Matrix of
len (DelLine A,i),
width (DelLine A,i),
K by MATRIX_2:7;
A16:
i in NAT
by ORDINAL1:def 13;
reconsider A9 =
A as
Matrix of
len A,
width A,
K by MATRIX_2:7;
let j be
Nat;
( 1 <= j & j <= m + (len (block_diagonal G,a)) implies (Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j = (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a) . j )assume that A17:
1
<= j
and A18:
j <= m + (len (block_diagonal G,a))
;
(Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j = (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a) . jA19:
j in Seg (m + (len (block_diagonal G,a)))
by A17, A18, FINSEQ_1:3;
A20:
1
<= 1
+ j
by NAT_1:11;
A21:
j in NAT
by ORDINAL1:def 13;
j + 1
<= len (block_diagonal <*A,(block_diagonal G,a)*>,a)
by A12, A18, XREAL_1:9;
then A22:
j + 1
in Seg (len (block_diagonal <*A,(block_diagonal G,a)*>,a))
by A20;
now per cases
( j < i or j >= i )
;
suppose A23:
j < i
;
(Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j = (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a) . j
i <= len A
by A3, FINSEQ_1:3;
then A24:
j < len A
by A23, XXREAL_0:2;
then A25:
j <= m
by A4, NAT_1:13;
then A26:
j in dom (DelLine A,i)
by A5, A17, FINSEQ_3:27;
A27:
j in dom A
by A17, A24, FINSEQ_3:27;
then A28:
j in Seg m
by A17, A25;
j in Seg (len A)
by A17, A24, FINSEQ_1:3;
then A29:
Line A9,
j =
A . j
by MATRIX_2:10
.=
da9 . j
by A4, A5, A21, A16, A23, FINSEQ_3:119
.=
Line (DelLine A,i),
j
by A5, A28, MATRIX_2:10
;
thus (Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j =
(block_diagonal <*A,(block_diagonal G,a)*>,a) . j
by A12, A21, A16, A23, FINSEQ_3:119
.=
Line (block_diagonal <*A,(block_diagonal G,a)*>,a),
j
by A7, A19, A15, MATRIX_2:10
.=
(Line (DelLine A,i),j) ^ ((width (block_diagonal G,a)) |-> a)
by A27, A29, Th23
.=
Line (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a),
j
by A26, Th23
.=
(block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a) . j
by A5, A10, A13, A19, MATRIX_2:10
;
verum end; suppose A30:
j >= i
;
(Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j = (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a) . jthen A31:
(Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j =
(block_diagonal <*A,(block_diagonal G,a)*>,a) . (j + 1)
by A12, A9, A3, A6, A18, A19, FINSEQ_3:120
.=
Line (block_diagonal <*A,(block_diagonal G,a)*>,a),
(j + 1)
by A7, A22, MATRIX_2:10
;
now per cases
( j + 1 <= len A or j + 1 > len A )
;
suppose A32:
j + 1
<= len A
;
(Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j = Line (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a),jthen A33:
j + 1
in dom A
by A20, FINSEQ_3:27;
A34:
j <= m
by A4, A32, XREAL_1:10;
then A35:
j in Seg m
by A17, FINSEQ_1:3;
A36:
j in dom (DelLine A,i)
by A5, A17, A34, FINSEQ_3:27;
j + 1
in Seg (len A)
by A20, A32;
then Line A9,
(j + 1) =
A . (j + 1)
by MATRIX_2:10
.=
da9 . j
by A1, A4, A5, A21, A30, A34, FINSEQ_3:120
.=
Line (DelLine A,i),
j
by A5, A35, MATRIX_2:10
;
hence (Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j =
(Line (DelLine A,i),j) ^ ((width (block_diagonal G,a)) |-> a)
by A31, A33, Th23
.=
Line (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a),
j
by A36, Th23
;
verum end; suppose A37:
j + 1
> len A
;
(Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j = Line (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a),jthen reconsider jL =
(j + 1) - (len A) as
Element of
NAT by NAT_1:21;
jL <> 0
by A37;
then A38:
jL >= 1
by NAT_1:14;
jL + (len A) <= (len (block_diagonal G,a)) + (len A)
by A8, A12, A18, XREAL_1:9;
then
jL <= len (block_diagonal G,a)
by XREAL_1:10;
then A39:
jL in dom (block_diagonal G,a)
by A38, FINSEQ_3:27;
thus (Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j =
Line (block_diagonal <*A,(block_diagonal G,a)*>,a),
(jL + (len A))
by A31
.=
((width (DelLine A,i)) |-> a) ^ (Line (block_diagonal G,a),jL)
by A2, A39, Th23
.=
Line (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a),
(jL + (len (DelLine A,i)))
by A39, Th23
.=
Line (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a),
j
by A4, A5
;
verum end; hence
(Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j = (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a) . j
by A5, A10, A13, A19, MATRIX_2:10;
verum end; hence
(Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) . j = (block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a) . j
;
verum end;
A40:
block_diagonal (<*(DelLine A,i)*> ^ G),a = block_diagonal <*(DelLine A,i),(block_diagonal G,a)*>,a
by Th36;
A41:
block_diagonal (<*A*> ^ G),a = block_diagonal <*A,(block_diagonal G,a)*>,a
by Th36;
len (Del (block_diagonal <*A,(block_diagonal G,a)*>,a),i) = m + (len (block_diagonal G,a))
by A12, A9, A3, A6, FINSEQ_3:118;
hence
DelLine (block_diagonal (<*A*> ^ G),a),i = block_diagonal (<*(DelLine A,i)*> ^ G),a
by A11, A41, A40, A14, FINSEQ_1:18; verum