let n, i, j be Nat; :: thesis: for K being Field
for a being Element of K
for R being FinSequence_of_Square-Matrix of K
for A being Matrix of n,K st i in dom A & j in Seg n holds
Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a
let K be Field; :: thesis: for a being Element of K
for R being FinSequence_of_Square-Matrix of K
for A being Matrix of n,K st i in dom A & j in Seg n holds
Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a
let a be Element of K; :: thesis: for R being FinSequence_of_Square-Matrix of K
for A being Matrix of n,K st i in dom A & j in Seg n holds
Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a
let R be FinSequence_of_Square-Matrix of K; :: thesis: for A being Matrix of n,K st i in dom A & j in Seg n holds
Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a
let A be Matrix of n,K; :: thesis: ( i in dom A & j in Seg n implies Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a )
assume A1:
( i in dom A & j in Seg n )
; :: thesis: Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),a
set b = block_diagonal R,a;
set B = <*(block_diagonal R,a)*>;
set AA = <*A*>;
set LRA = Sum (Len (R ^ <*A*>));
set LBA = Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>));
set iS = i + (Sum (Len R));
set jS = j + (Sum (Len R));
A2:
( len A = n & width A = n )
by MATRIX_1:25;
then A3:
( n >= 1 & dom A = Seg n )
by A1, FINSEQ_1:4, FINSEQ_1:def 3, NAT_1:14;
A4:
Len R = Width R
by Th46;
A5:
len (block_diagonal R,a) = Sum (Len R)
by Def5;
A6:
( Len (R ^ <*A*>) = (Len R) ^ (Len <*A*>) & Len (<*(block_diagonal R,a)*> ^ <*A*>) = (Len <*(block_diagonal R,a)*>) ^ (Len <*A*>) & Len <*A*> = <*(len A)*> & Len <*(block_diagonal R,a)*> = <*(len (block_diagonal R,a))*> & Width (<*(block_diagonal R,a)*> ^ <*A*>) = (Width <*(block_diagonal R,a)*>) ^ (Width <*A*>) & Width <*A*> = <*(width A)*> & Width <*(block_diagonal R,a)*> = <*(width (block_diagonal R,a))*> & Len (<*(block_diagonal R,a)*> ^ <*A*>) = Width (<*(block_diagonal R,a)*> ^ <*A*>) )
by Th14, Th15, Th18, Th19, Th46;
then A7:
( Sum (Len (R ^ <*A*>)) = (len A) + (Sum (Len R)) & Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>)) = (len A) + (Sum (Len <*(block_diagonal R,a)*>)) & Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>)) = (Sum (Width <*A*>)) + (width (block_diagonal R,a)) & Sum (Len <*(block_diagonal R,a)*>) = len (block_diagonal R,a) & Sum (Len <*A*>) = len A & Sum (Width <*(block_diagonal R,a)*>) = width (block_diagonal R,a) )
by RVSUM_1:103, RVSUM_1:104, RVSUM_1:106;
per cases
( n = 1 or n > 1 )
by A3, XXREAL_0:1;
suppose A8:
n = 1
;
:: thesis: Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),athen A9:
(
i = 1 &
j = 1 )
by A1, A3, FINSEQ_1:4, TARSKI:def 1;
len (Deleting A,i,j) =
1
-' 1
by A1, A8, LAPLACE:2
.=
0
by XREAL_1:234
;
then A10:
Deleting A,
i,
j = {}
;
thus Deleting (block_diagonal (R ^ <*A*>),a),
(i + (Sum (Len R))),
(j + (Sum (Len R))) =
Deleting (block_diagonal (<*(block_diagonal R,a)*> ^ <*A*>),a),
(i + (Sum (Len R))),
(j + (Sum (Len R)))
by A5, A7, Th35
.=
Segm (block_diagonal (<*(block_diagonal R,a)*> ^ <*A*>),a),
((Seg (Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>)))) \ {(i + (Sum (Len R)))}),
((Seg (Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>)))) \ {(j + (Sum (Len R)))})
by MATRIX13:58
.=
Segm (block_diagonal (<*(block_diagonal R,a)*> ^ <*A*>),a),
(Seg (Sum (Len <*(block_diagonal R,a)*>))),
((Seg (Sum (Len (<*(block_diagonal R,a)*> ^ <*A*>)))) \ {(j + (Sum (Len R)))})
by A2, A5, A7, A8, A9, FINSEQ_1:12
.=
Segm (block_diagonal (<*(block_diagonal R,a)*> ^ <*A*>),a),
(Seg (Sum (Len <*(block_diagonal R,a)*>))),
(Seg (Sum (Width <*(block_diagonal R,a)*>)))
by A2, A5, A6, A7, A8, A9, FINSEQ_1:12
.=
block_diagonal R,
a
by Th32, A7
.=
block_diagonal <*(block_diagonal R,a)*>,
a
by Th34
.=
block_diagonal (<*(block_diagonal R,a)*> ^ <*(Deleting A,i,j)*>),
a
by A10, Th40
.=
block_diagonal (R ^ <*(Deleting A,i,j)*>),
a
by Th35
;
:: thesis: verum end; suppose
n > 1
;
:: thesis: Deleting (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R))),(j + (Sum (Len R))) = block_diagonal (R ^ <*(Deleting A,i,j)*>),athen A11:
width A = width (DelLine A,i)
by A2, LAPLACE:4;
thus Deleting (block_diagonal (R ^ <*A*>),a),
(i + (Sum (Len R))),
(j + (Sum (Len R))) =
DelCol (DelLine (block_diagonal (R ^ <*A*>),a),(i + (Sum (Len R)))),
(j + (Sum (Len R)))
by MATRIX_2:def 8
.=
DelCol (block_diagonal (R ^ <*(DelLine A,i)*>),a),
(j + (Sum (Len R)))
by A1, A11, Th42
.=
block_diagonal (R ^ <*(DelCol (DelLine A,i),j)*>),
a
by A4, A1, A2, A11, Th44
.=
block_diagonal (R ^ <*(Deleting A,i,j)*>),
a
by MATRIX_2:def 8
;
:: thesis: verum end;