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 Seg (width A) holds
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (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 Seg (width A) holds
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (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 Seg (width A) holds
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)
let A be Matrix of K; for G being FinSequence_of_Matrix of K st i in Seg (width A) holds
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)
let G be FinSequence_of_Matrix of K; ( i in Seg (width A) implies DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a) )
assume A1:
i in Seg (width A)
; DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)
set iS = i + (Sum (Width G));
set bG = block_diagonal (G,a);
set Da = DelCol (A,i);
set AA = <*A*>;
set DA = <*(DelCol (A,i))*>;
set BG = <*(block_diagonal (G,a))*>;
set BGA = block_diagonal (<*(block_diagonal (G,a)),A*>,a);
set BGD = block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a);
A2:
len (DelCol (A,i)) = len A
by MATRIX_0:def 13;
len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) = Sum (Len (<*(block_diagonal (G,a))*> ^ <*A*>))
by Def5;
then A3:
len (block_diagonal (<*(block_diagonal (G,a)),A*>,a)) = (len (block_diagonal (G,a))) + (len A)
by Th16;
A4:
width (block_diagonal (G,a)) = Sum (Width G)
by Def5;
A5:
len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) = Sum (Len (<*(block_diagonal (G,a))*> ^ <*(DelCol (A,i))*>))
by Def5;
then A6:
len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) = (len (block_diagonal (G,a))) + (len (DelCol (A,i)))
by Th16;
A7:
now for j being Nat st 1 <= j & j <= len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) holds
(DelCol ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Width G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j
width A <> 0
by A1;
then
width A >= 1
by NAT_1:14;
then
(width A) -' 1
= (width A) - 1
by XREAL_1:233;
then A8:
width A = ((width A) -' 1) + 1
;
A9:
dom ((width A) |-> a) = Seg (width A)
by FINSEQ_2:124;
A10:
len ((width (block_diagonal (G,a))) |-> a) = width (block_diagonal (G,a))
by CARD_1:def 7;
reconsider Da9 =
DelCol (
A,
i) as
Matrix of
len (DelCol (A,i)),
width (DelCol (A,i)),
K by MATRIX_0:51;
let j be
Nat;
( 1 <= j & j <= len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) implies (DelCol ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Width G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j )assume that A11:
1
<= j
and A12:
j <= len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a))
;
(DelCol ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Width G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . jA13:
j in Seg (len (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)))
by A11, A12;
A14:
len (Line ((block_diagonal (G,a)),j)) = width (block_diagonal (G,a))
by MATRIX_0:def 7;
A15:
now Del ((Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j)),(i + (Sum (Width G)))) = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . jper cases
( j <= len (block_diagonal (G,a)) or j > len (block_diagonal (G,a)) )
;
suppose
j <= len (block_diagonal (G,a))
;
Del ((Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j)),(i + (Sum (Width G)))) = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . jthen A16:
j in dom (block_diagonal (G,a))
by A11, FINSEQ_3:25;
then
Line (
(block_diagonal (<*(block_diagonal (G,a)),A*>,a)),
j)
= (Line ((block_diagonal (G,a)),j)) ^ ((width A) |-> a)
by Th23;
hence Del (
(Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j)),
(i + (Sum (Width G)))) =
(Line ((block_diagonal (G,a)),j)) ^ (Del (((width A) |-> a),i))
by A1, A4, A9, A14, Th3
.=
(Line ((block_diagonal (G,a)),j)) ^ (((width A) -' 1) |-> a)
by A1, A8, Th4
.=
(Line ((block_diagonal (G,a)),j)) ^ ((width (DelCol (A,i))) |-> a)
by A1, LAPLACE:3
.=
Line (
(block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)),
j)
by A16, Th23
.=
(block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j
by A5, A13, MATRIX_0:52
;
verum end; suppose A17:
j > len (block_diagonal (G,a))
;
Del ((Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j)),(i + (Sum (Width G)))) = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . jthen reconsider jL =
j - (len (block_diagonal (G,a))) as
Element of
NAT by NAT_1:21;
jL <> 0
by A17;
then A18:
jL >= 1
by NAT_1:14;
jL + (len (block_diagonal (G,a))) <= (len (block_diagonal (G,a))) + (len A)
by A6, A12, MATRIX_0:def 13;
then A19:
jL <= len A
by XREAL_1:8;
then A20:
jL in dom (DelCol (A,i))
by A2, A18, FINSEQ_3:25;
A21:
jL in Seg (len A)
by A18, A19;
A22:
jL in dom A
by A18, A19, FINSEQ_3:25;
then A23:
Del (
(Line (A,jL)),
i) =
Da9 . jL
by MATRIX_0:def 13
.=
Line (
(DelCol (A,i)),
jL)
by A2, A21, MATRIX_0:52
;
A24:
dom (Line (A,jL)) = Seg (width A)
by FINSEQ_2:124;
Line (
(block_diagonal (<*(block_diagonal (G,a)),A*>,a)),
(jL + (len (block_diagonal (G,a)))))
= ((width (block_diagonal (G,a))) |-> a) ^ (Line (A,jL))
by A22, Th23;
hence Del (
(Line ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),j)),
(i + (Sum (Width G)))) =
((width (block_diagonal (G,a))) |-> a) ^ (Del ((Line (A,jL)),i))
by A1, A4, A10, A24, Th3
.=
Line (
(block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)),
((len (block_diagonal (G,a))) + jL))
by A20, A23, Th23
.=
(block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j
by A5, A13, MATRIX_0:52
;
verum end;
j in dom (block_diagonal (<*(block_diagonal (G,a)),A*>,a))
by A2, A6, A3, A11, A12, FINSEQ_3:25;
hence
(DelCol ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Width G))))) . j = (block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)) . j
by A15, MATRIX_0:def 13;
verum end;
A25:
block_diagonal ((G ^ <*(DelCol (A,i))*>),a) = block_diagonal (<*(block_diagonal (G,a)),(DelCol (A,i))*>,a)
by Th35;
A26:
len (DelCol ((block_diagonal (<*(block_diagonal (G,a)),A*>,a)),(i + (Sum (Width G))))) = len (block_diagonal (<*(block_diagonal (G,a)),A*>,a))
by MATRIX_0:def 13;
block_diagonal ((G ^ <*A*>),a) = block_diagonal (<*(block_diagonal (G,a)),A*>,a)
by Th35;
hence
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)
by A2, A26, A5, A3, A7, A25, Th16, FINSEQ_1:14; verum