let n, i, j be Nat; 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; 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; 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; 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; ( 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 that
A1:
i in dom A
and
A2:
j in Seg n
; Deleting (block_diagonal (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),a
n <> 0
by A2;
then A3:
n >= 1
by NAT_1:14;
set AA = <*A*>;
set b = block_diagonal R,a;
set B = <*(block_diagonal R,a)*>;
set LAR = Sum (Len (<*A*> ^ R));
set LAB = Sum (Len (<*A*> ^ <*(block_diagonal R,a)*>));
A4:
width A = n
by MATRIX_1:25;
Width <*A*> = <*(width A)*>
by Th19;
then A5:
Sum (Width <*A*>) = width A
by RVSUM_1:103;
A6:
Width <*(block_diagonal R,a)*> = <*(width (block_diagonal R,a))*>
by Th19;
A7:
Len <*A*> = <*(len A)*>
by Th15;
then A8:
Sum (Len <*A*>) = len A
by RVSUM_1:103;
Len (<*A*> ^ <*(block_diagonal R,a)*>) = (Len <*A*>) ^ (Len <*(block_diagonal R,a)*>)
by Th14;
then A9:
Sum (Len (<*A*> ^ <*(block_diagonal R,a)*>)) = (len A) + (Sum (Len <*(block_diagonal R,a)*>))
by A7, RVSUM_1:106;
Len (<*A*> ^ R) = (Len <*A*>) ^ (Len R)
by Th14;
then A10:
Sum (Len (<*A*> ^ R)) = (len A) + (Sum (Len R))
by A7, RVSUM_1:106;
A11:
Len (<*A*> ^ <*(block_diagonal R,a)*>) = Width (<*A*> ^ <*(block_diagonal R,a)*>)
by Th46;
Width (<*A*> ^ <*(block_diagonal R,a)*>) = (Width <*A*>) ^ (Width <*(block_diagonal R,a)*>)
by Th18;
then A12:
Sum (Len (<*A*> ^ <*(block_diagonal R,a)*>)) = (Sum (Width <*A*>)) + (width (block_diagonal R,a))
by A6, A11, RVSUM_1:104;
A13:
len (block_diagonal R,a) = Sum (Len R)
by Def5;
Len <*(block_diagonal R,a)*> = <*(len (block_diagonal R,a))*>
by Th15;
then A14:
Sum (Len <*(block_diagonal R,a)*>) = len (block_diagonal R,a)
by RVSUM_1:103;
A15:
len A = n
by MATRIX_1:25;
then A16:
dom A = Seg n
by FINSEQ_1:def 3;
per cases
( n = 1 or n > 1 )
by A3, XXREAL_0:1;
suppose A17:
n = 1
;
Deleting (block_diagonal (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),athen A18:
i = 1
by A1, A16, FINSEQ_1:4, TARSKI:def 1;
A19:
j = 1
by A2, A17, FINSEQ_1:4, TARSKI:def 1;
len (Deleting A,i,j) =
1
-' 1
by A1, A17, LAPLACE:2
.=
0
by XREAL_1:234
;
then A20:
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 A13, A10, A9, A14, 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 A15, A4, A9, A12, A14, A8, A5, A17, A18, A19, Th33, FINSEQ_1:4
.=
block_diagonal <*(block_diagonal R,a)*>,
a
by Th34
.=
block_diagonal (<*(Deleting A,i,j)*> ^ <*(block_diagonal R,a)*>),
a
by A20, Th40
.=
block_diagonal (<*(Deleting A,i,j)*> ^ R),
a
by Th36
;
verum end; suppose
n > 1
;
Deleting (block_diagonal (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),athen A21:
width A = width (DelLine A,i)
by A15, 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, A21, Th41
.=
block_diagonal (<*(DelCol (DelLine A,i),j)*> ^ R),
a
by A2, A4, A21, Th43
.=
block_diagonal (<*(Deleting A,i,j)*> ^ R),
a
by MATRIX_2:def 8
;
verum end;