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 ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),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 ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),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 ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),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 ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),a)
let G be FinSequence_of_Matrix of K; ( i in dom A & width A = width (DelLine (A,i)) implies DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),a) )
assume that
A1:
i in dom A
and
A2:
width A = width (DelLine (A,i))
; DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),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:104;
set Si = (Sum (Len G)) + i;
set bG = block_diagonal (G,a);
set DA = <*(DelLine (A,i))*>;
set AA = <*A*>;
set BG = <*(block_diagonal (G,a))*>;
set bGA = block_diagonal (<*(block_diagonal (G,a)),A*>,a);
set bGdA = block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a);
A6:
Seg (len (block_diagonal (<*(block_diagonal (G,a)),A*>,a))) = dom (block_diagonal (<*(block_diagonal (G,a)),A*>,a))
by FINSEQ_1:def 3;
A7:
len (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) = Sum (Len (<*(block_diagonal (G,a))*> ^ <*(DelLine (A,i))*>))
by Def5;
then A8:
len (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) = m + (len (block_diagonal (G,a)))
by A5, Th16;
A9:
len (block_diagonal (G,a)) = Sum (Len G)
by Def5;
A10:
len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) = Sum (Len (<*(block_diagonal (G,a))*> ^ <*A*>))
by Def5;
then A11:
len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) = (len A) + (len (block_diagonal (G,a)))
by Th16;
then A12:
len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) = (m + (len (block_diagonal (G,a)))) + 1
by A4;
A13:
len (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) = (len (DelLine (A,i))) + (len (block_diagonal (G,a)))
by A7, Th16;
A14:
now for j being Nat st 1 <= j & j <= m + (len (block_diagonal (G,a))) holds
(Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Len G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j
m + (len (block_diagonal (G,a))) <= len (block_diagonal (<*(block_diagonal (G,a)),A*>,a))
by A12, NAT_1:11;
then A15:
Seg (m + (len (block_diagonal (G,a)))) c= Seg (len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)))
by FINSEQ_1:5;
reconsider da9 =
DelLine (
A,
i) as
Matrix of
len (DelLine (A,i)),
width (DelLine (A,i)),
K by MATRIX_0:51;
reconsider A9 =
A as
Matrix of
len A,
width A,
K by MATRIX_0:51;
let j be
Nat;
( 1 <= j & j <= m + (len (block_diagonal (G,a))) implies (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Len G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j )assume that A16:
1
<= j
and A17:
j <= m + (len (block_diagonal (G,a)))
;
(Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Len G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . jA18:
j in Seg (m + (len (block_diagonal (G,a))))
by A16, A17;
A19:
1
<= 1
+ j
by NAT_1:11;
j + 1
<= len (block_diagonal (<*(block_diagonal (G,a)),A*>,a))
by A12, A17, XREAL_1:7;
then A20:
j + 1
in Seg (len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)))
by A19;
now (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . jper cases
( j <= len (block_diagonal (G,a)) or j > len (block_diagonal (G,a)) )
;
suppose A21:
j <= len (block_diagonal (G,a))
;
(Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . jthen A22:
j in dom (block_diagonal (G,a))
by A16, FINSEQ_3:25;
0 < i
by A3;
then
j + 0 < (len (block_diagonal (G,a))) + i
by A21, XREAL_1:8;
then
j < (Sum (Len G)) + i
by Def5;
hence (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j =
(block_diagonal (<*(block_diagonal (G,a)),A*>,a)) . j
by FINSEQ_3:110
.=
Line (
(block_diagonal (<*(block_diagonal (G,a)),A*>,a)),
j)
by A10, A18, A15, MATRIX_0:52
.=
(Line ((block_diagonal (G,a)),j)) ^ ((width (DelLine (A,i))) |-> a)
by A2, A22, Th23
.=
Line (
(block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),
j)
by A22, Th23
.=
(block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j
by A5, A7, A13, A18, MATRIX_0:52
;
verum end; suppose A23:
j > len (block_diagonal (G,a))
;
(Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . jthen reconsider jL =
j - (len (block_diagonal (G,a))) as
Element of
NAT by NAT_1:21;
A24:
0 + 1
<= jL + 1
by NAT_1:13;
jL + (len (block_diagonal (G,a))) <= m + (len (block_diagonal (G,a)))
by A17;
then A25:
jL <= m
by XREAL_1:8;
then A26:
jL + 1
<= len A
by A4, XREAL_1:7;
then A27:
jL + 1
in dom A
by A24, FINSEQ_3:25;
jL <> 0
by A23;
then A28:
1
<= jL
by NAT_1:14;
then A29:
jL in dom (DelLine (A,i))
by A5, A25, FINSEQ_3:25;
A30:
jL + 1
in Seg (len A)
by A24, A26;
A31:
jL in Seg (len (DelLine (A,i)))
by A5, A28, A25;
A32:
jL <= len A
by A4, A25, NAT_1:13;
then A33:
jL in Seg (len A)
by A28;
A34:
jL in dom A
by A28, A32, FINSEQ_3:25;
now (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = Line ((block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),(jL + (len (block_diagonal (G,a)))))per cases
( j < (Sum (Len G)) + i or j >= (Sum (Len G)) + i )
;
suppose A35:
j < (Sum (Len G)) + i
;
(Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = Line ((block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),(jL + (len (block_diagonal (G,a)))))then
jL + (len (block_diagonal (G,a))) < i + (len (block_diagonal (G,a)))
by Def5;
then A36:
jL < i
by XREAL_1:7;
A37:
Line (
A,
jL) =
A9 . jL
by A33, MATRIX_0:52
.=
da9 . jL
by A36, FINSEQ_3:110
.=
Line (
(DelLine (A,i)),
jL)
by A31, MATRIX_0:52
;
thus (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j =
(block_diagonal (<*(block_diagonal (G,a)),A*>,a)) . j
by A35, FINSEQ_3:110
.=
Line (
(block_diagonal (<*(block_diagonal (G,a)),A*>,a)),
(jL + (len (block_diagonal (G,a)))))
by A10, A18, A15, MATRIX_0:52
.=
((width (block_diagonal (G,a))) |-> a) ^ (Line ((DelLine (A,i)),jL))
by A34, A37, Th23
.=
Line (
(block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),
(jL + (len (block_diagonal (G,a)))))
by A29, Th23
;
verum end; suppose A38:
j >= (Sum (Len G)) + i
;
(Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = Line ((block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),(jL + (len (block_diagonal (G,a)))))then
jL + (len (block_diagonal (G,a))) >= i + (len (block_diagonal (G,a)))
by Def5;
then A39:
jL >= i
by XREAL_1:8;
A40:
Line (
A,
(1 + jL)) =
A9 . (1 + jL)
by A30, MATRIX_0:52
.=
da9 . jL
by A1, A4, A25, A39, FINSEQ_3:111
.=
Line (
(DelLine (A,i)),
jL)
by A31, MATRIX_0:52
;
thus (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j =
(block_diagonal (<*(block_diagonal (G,a)),A*>,a)) . (j + 1)
by A9, A11, A12, A3, A6, A17, A38, FINSEQ_1:60, FINSEQ_3:111
.=
Line (
(block_diagonal (<*(block_diagonal (G,a)),A*>,a)),
((jL + 1) + (len (block_diagonal (G,a)))))
by A10, A20, MATRIX_0:52
.=
((width (block_diagonal (G,a))) |-> a) ^ (Line ((DelLine (A,i)),jL))
by A27, A40, Th23
.=
Line (
(block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)),
(jL + (len (block_diagonal (G,a)))))
by A29, Th23
;
verum end; hence
(Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j
by A5, A7, A13, A18, MATRIX_0:52;
verum end; hence
(Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Len G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)) . j
;
verum end;
A41:
block_diagonal ((G ^ <*(DelLine (A,i))*>),a) = block_diagonal (<*(block_diagonal (G,a)),(DelLine (A,i))*>,a)
by Th35;
A42:
block_diagonal ((G ^ <*A*>),a) = block_diagonal (<*(block_diagonal (G,a)),A*>,a)
by Th35;
len (Del ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),((Sum (Len G)) + i))) = m + (len (block_diagonal (G,a)))
by A9, A11, A12, A3, A6, FINSEQ_1:60, FINSEQ_3:109;
hence
DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),a)
by A8, A42, A41, A14; verum