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 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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)
; :: thesis: DelCol (block_diagonal (G ^ <*A*>),a),(i + (Sum (Width G))) = block_diagonal (G ^ <*(DelCol A,i)*>),a
set AA = <*A*>;
set Da = DelCol A,i;
set DA = <*(DelCol A,i)*>;
set bG = block_diagonal G,a;
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;
set iS = i + (Sum (Width G));
A2:
( len (DelCol A,i) = len A & 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_2:def 6;
A3:
( len (block_diagonal <*(block_diagonal G,a),A*>,a) = Sum (Len (<*(block_diagonal G,a)*> ^ <*A*>)) & len (block_diagonal <*(block_diagonal G,a),(DelCol A,i)*>,a) = Sum (Len (<*(block_diagonal G,a)*> ^ <*(DelCol A,i)*>)) & width (block_diagonal G,a) = Sum (Width G) )
by Def5;
then A4:
( len (block_diagonal <*(block_diagonal G,a),(DelCol A,i)*>,a) = (len (block_diagonal G,a)) + (len (DelCol A,i)) & len (block_diagonal <*(block_diagonal G,a),A*>,a) = (len (block_diagonal G,a)) + (len A) )
by Th16;
A5:
now let j be
Nat;
:: thesis: ( 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 A6:
( 1
<= j &
j <= len (block_diagonal <*(block_diagonal G,a),(DelCol A,i)*>,a) )
;
:: thesis: (DelCol (block_diagonal <*(block_diagonal G,a),A*>,a),(i + (Sum (Width G)))) . j = (block_diagonal <*(block_diagonal G,a),(DelCol A,i)*>,a) . jA7:
(
j in dom (block_diagonal <*(block_diagonal G,a),A*>,a) &
j in Seg (len (block_diagonal <*(block_diagonal G,a),(DelCol A,i)*>,a)) )
by A4, A2, A6, FINSEQ_1:3, FINSEQ_3:27;
reconsider Da' =
DelCol A,
i as
Matrix of
len (DelCol A,i),
width (DelCol A,i),
K by MATRIX_2:7;
A8:
(
dom ((width A) |-> a) = Seg (width A) &
len ((width (block_diagonal G,a)) |-> a) = width (block_diagonal G,a) )
by FINSEQ_1:def 18, FINSEQ_2:144;
A9:
len (Line (block_diagonal G,a),j) = width (block_diagonal G,a)
by MATRIX_1:def 8;
(width A) -' 1
= (width A) - 1
by A1, FINSEQ_1:4, NAT_1:14, XREAL_1:235;
then A10:
width A = ((width A) -' 1) + 1
;
now per cases
( j <= len (block_diagonal G,a) or j > len (block_diagonal G,a) )
;
suppose
j <= len (block_diagonal G,a)
;
:: thesis: 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 A11:
j in dom (block_diagonal G,a)
by A6, FINSEQ_3:27;
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 Th3, A3, A1, A8, A9
.=
(Line (block_diagonal G,a),j) ^ (((width A) -' 1) |-> a)
by A1, A10, 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 A11, Th23
.=
(block_diagonal <*(block_diagonal G,a),(DelCol A,i)*>,a) . j
by A3, A7, MATRIX_2:10
;
:: thesis: verum end; suppose A12:
j > len (block_diagonal G,a)
;
:: thesis: 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;
A13:
dom (Line A,jL) = Seg (width A)
by FINSEQ_2:144;
jL <> 0
by A12;
then A14:
jL >= 1
by NAT_1:14;
jL + (len (block_diagonal G,a)) <= (len (block_diagonal G,a)) + (len A)
by A6, A4, MATRIX_2:def 6;
then
jL <= len A
by XREAL_1:10;
then A15:
(
jL in dom A &
jL in Seg (len A) &
jL in dom (DelCol A,i) )
by A2, A14, FINSEQ_3:27;
then A16:
Del (Line A,jL),
i =
Da' . jL
by MATRIX_2:def 6
.=
Line (DelCol A,i),
jL
by A2, A15, MATRIX_2:10
;
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 Th23, A15;
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 A13, Th3, A3, A1, A8
.=
Line (block_diagonal <*(block_diagonal G,a),(DelCol A,i)*>,a),
((len (block_diagonal G,a)) + jL)
by A15, A16, Th23
.=
(block_diagonal <*(block_diagonal G,a),(DelCol A,i)*>,a) . j
by A3, A7, MATRIX_2:10
;
:: thesis: verum end; 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 A7, MATRIX_2:def 6;
:: thesis: verum end;
( block_diagonal (G ^ <*A*>),a = block_diagonal <*(block_diagonal G,a),A*>,a & block_diagonal (G ^ <*(DelCol A,i)*>),a = block_diagonal <*(block_diagonal G,a),(DelCol A,i)*>,a )
by Th35;
hence
DelCol (block_diagonal (G ^ <*A*>),a),(i + (Sum (Width G))) = block_diagonal (G ^ <*(DelCol A,i)*>),a
by A5, A2, A4, FINSEQ_1:18; :: thesis: verum