let i be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: 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:104;
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:5;
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 :: thesis: for j being Nat st 1 <= j & j <= m + (len (block_diagonal (G,a))) holds
(Del ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = (block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)) . j
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: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; :: thesis: ( 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
A16: 1 <= j and
A17: j <= m + (len (block_diagonal (G,a))) ; :: thesis: (Del ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = (block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)) . j
A18: 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 (<*A,(block_diagonal (G,a))*>,a)) by A12, A17, XREAL_1:7;
then A20: j + 1 in Seg (len (block_diagonal (<*A,(block_diagonal (G,a))*>,a))) by A19;
now :: thesis: (Del ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = (block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)) . j
per cases ( j < i or j >= i ) ;
suppose A21: j < i ; :: thesis: (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:1;
then A22: j < len A by A21, XXREAL_0:2;
then A23: j <= m by A4, NAT_1:13;
then A24: j in dom (DelLine (A,i)) by A5, A16, FINSEQ_3:25;
A25: j in dom A by A16, A22, FINSEQ_3:25;
A26: j in Seg m by A16, A23;
j in Seg (len A) by A16, A22;
then A27: Line (A9,j) = A . j by MATRIX_0:52
.= da9 . j by A21, FINSEQ_3:110
.= Line ((DelLine (A,i)),j) by A5, A26, MATRIX_0:52 ;
thus (Del ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = (block_diagonal (<*A,(block_diagonal (G,a))*>,a)) . j by A21, FINSEQ_3:110
.= Line ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),j) by A7, A18, A15, MATRIX_0:52
.= (Line ((DelLine (A,i)),j)) ^ ((width (block_diagonal (G,a))) |-> a) by A25, A27, Th23
.= Line ((block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)),j) by A24, Th23
.= (block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)) . j by A5, A10, A13, A18, MATRIX_0:52 ; :: thesis: verum
end;
suppose A28: j >= i ; :: thesis: (Del ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = (block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)) . j
then A29: (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, A17, FINSEQ_3:111
.= Line ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),(j + 1)) by A7, A20, MATRIX_0:52 ;
now :: thesis: (Del ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = Line ((block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)),j)
per cases ( j + 1 <= len A or j + 1 > len A ) ;
suppose A30: j + 1 <= len A ; :: thesis: (Del ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = Line ((block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)),j)
then A31: j + 1 in dom A by A19, FINSEQ_3:25;
A32: j <= m by A4, A30, XREAL_1:8;
then A33: j in Seg m by A16;
A34: j in dom (DelLine (A,i)) by A5, A16, A32, FINSEQ_3:25;
j + 1 in Seg (len A) by A19, A30;
then Line (A9,(j + 1)) = A . (j + 1) by MATRIX_0:52
.= da9 . j by A1, A4, A28, A32, FINSEQ_3:111
.= Line ((DelLine (A,i)),j) by A5, A33, MATRIX_0:52 ;
hence (Del ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = (Line ((DelLine (A,i)),j)) ^ ((width (block_diagonal (G,a))) |-> a) by A29, A31, Th23
.= Line ((block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)),j) by A34, Th23 ;
:: thesis: verum
end;
suppose A35: j + 1 > len A ; :: thesis: (Del ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = Line ((block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)),j)
then reconsider jL = (j + 1) - (len A) as Element of NAT by NAT_1:21;
jL <> 0 by A35;
then A36: jL >= 1 by NAT_1:14;
jL + (len A) <= (len (block_diagonal (G,a))) + (len A) by A8, A12, A17, XREAL_1:7;
then jL <= len (block_diagonal (G,a)) by XREAL_1:8;
then A37: jL in dom (block_diagonal (G,a)) by A36, FINSEQ_3:25;
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 A29
.= ((width (DelLine (A,i))) |-> a) ^ (Line ((block_diagonal (G,a)),jL)) by A2, A37, Th23
.= Line ((block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)),(jL + (len (DelLine (A,i))))) by A37, Th23
.= Line ((block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)),j) by A4, A5 ; :: thesis: verum
end;
end;
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, A18, MATRIX_0:52; :: thesis: verum
end;
end;
end;
hence (Del ((block_diagonal (<*A,(block_diagonal (G,a))*>,a)),i)) . j = (block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a)) . j ; :: thesis: verum
end;
A38: block_diagonal ((<*(DelLine (A,i))*> ^ G),a) = block_diagonal (<*(DelLine (A,i)),(block_diagonal (G,a))*>,a) by Th36;
A39: 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:109;
hence DelLine ((block_diagonal ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelLine (A,i))*> ^ G),a) by A11, A39, A38, A14; :: thesis: verum