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 (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),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 (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),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 (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),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 (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),a
let A be Matrix of n,K; :: thesis: ( i in dom A & j in Seg n implies Deleting (block_diagonal (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),a )
assume A1:
( i in dom A & j in Seg n )
; :: thesis: Deleting (block_diagonal (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),a
set b = block_diagonal R,a;
set B = <*(block_diagonal R,a)*>;
set AA = <*A*>;
set LAR = Sum (Len (<*A*> ^ R));
set LAB = Sum (Len (<*A*> ^ <*(block_diagonal R,a)*>));
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 (block_diagonal R,a) = Sum (Len R)
by Def5;
( Len (<*A*> ^ R) = (Len <*A*>) ^ (Len R) & Len (<*A*> ^ <*(block_diagonal R,a)*>) = (Len <*A*>) ^ (Len <*(block_diagonal R,a)*>) & Len <*A*> = <*(len A)*> & Len <*(block_diagonal R,a)*> = <*(len (block_diagonal R,a))*> & Width (<*A*> ^ <*(block_diagonal R,a)*>) = (Width <*A*>) ^ (Width <*(block_diagonal R,a)*>) & Width <*A*> = <*(width A)*> & Width <*(block_diagonal R,a)*> = <*(width (block_diagonal R,a))*> & Len (<*A*> ^ <*(block_diagonal R,a)*>) = Width (<*A*> ^ <*(block_diagonal R,a)*>) )
by Th14, Th15, Th18, Th19, Th46;
then A5:
( Sum (Len (<*A*> ^ R)) = (len A) + (Sum (Len R)) & Sum (Len (<*A*> ^ <*(block_diagonal R,a)*>)) = (len A) + (Sum (Len <*(block_diagonal R,a)*>)) & Sum (Len (<*A*> ^ <*(block_diagonal R,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 <*A*>) = width A )
by RVSUM_1:103, RVSUM_1:104, RVSUM_1:106;
per cases
( n = 1 or n > 1 )
by A3, XXREAL_0:1;
suppose A6:
n = 1
;
:: thesis: Deleting (block_diagonal (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),athen A7:
(
i = 1 &
j = 1 )
by A1, A3, FINSEQ_1:4, TARSKI:def 1;
len (Deleting A,i,j) =
1
-' 1
by A1, A6, LAPLACE:2
.=
0
by XREAL_1:234
;
then A8:
Deleting A,
i,
j = {}
;
thus Deleting (block_diagonal (<*A*> ^ R),a),
i,
j =
Deleting (block_diagonal (<*A*> ^ <*(block_diagonal R,a)*>),a),
i,
j
by A4, A5, Th36
.=
Segm (block_diagonal (<*A*> ^ <*(block_diagonal R,a)*>),a),
((Seg (Sum (Len (<*A*> ^ <*(block_diagonal R,a)*>)))) \ {i}),
((Seg (Sum (Len (<*A*> ^ <*(block_diagonal R,a)*>)))) \ {j})
by MATRIX13:58
.=
block_diagonal R,
a
by Th33, A6, A2, A5, A7, FINSEQ_1:4
.=
block_diagonal <*(block_diagonal R,a)*>,
a
by Th34
.=
block_diagonal (<*(Deleting A,i,j)*> ^ <*(block_diagonal R,a)*>),
a
by A8, Th40
.=
block_diagonal (<*(Deleting A,i,j)*> ^ R),
a
by Th36
;
:: thesis: verum end; suppose
n > 1
;
:: thesis: Deleting (block_diagonal (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),athen A9:
width A = width (DelLine A,i)
by A2, LAPLACE:4;
thus Deleting (block_diagonal (<*A*> ^ R),a),
i,
j =
DelCol (DelLine (block_diagonal (<*A*> ^ R),a),i),
j
by MATRIX_2:def 8
.=
DelCol (block_diagonal (<*(DelLine A,i)*> ^ R),a),
j
by A1, A9, Th41
.=
block_diagonal (<*(DelCol (DelLine A,i),j)*> ^ R),
a
by A1, A2, A9, Th43
.=
block_diagonal (<*(Deleting A,i,j)*> ^ R),
a
by MATRIX_2:def 8
;
:: thesis: verum end;