let i, j, n 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_0:24;
Width <*A*> = <*(width A)*>
by Th19;
then A5:
Sum (Width <*A*>) = width A
by RVSUM_1:73;
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:73;
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:76;
A10:
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 A11:
Sum (Len (<*A*> ^ <*(block_diagonal (R,a))*>)) = (Sum (Width <*A*>)) + (width (block_diagonal (R,a)))
by A6, A10, RVSUM_1:74;
Len <*(block_diagonal (R,a))*> = <*(len (block_diagonal (R,a)))*>
by Th15;
then A12:
Sum (Len <*(block_diagonal (R,a))*>) = len (block_diagonal (R,a))
by RVSUM_1:73;
A13:
len A = n
by MATRIX_0:24;
then A14:
dom A = Seg n
by FINSEQ_1:def 3;
per cases
( n = 1 or n > 1 )
by A3, XXREAL_0:1;
suppose A15:
n = 1
;
Deleting ((block_diagonal ((<*A*> ^ R),a)),i,j) = block_diagonal ((<*(Deleting (A,i,j))*> ^ R),a)then A16:
i = 1
by A1, A14, FINSEQ_1:2, TARSKI:def 1;
A17:
j = 1
by A2, A15, FINSEQ_1:2, TARSKI:def 1;
len (Deleting (A,i,j)) =
1
-' 1
by A1, A15, LAPLACE:2
.=
0
by XREAL_1:232
;
then A18:
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 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 A13, A4, A9, A11, A12, A8, A5, A15, A16, A17, Th33, FINSEQ_1:2
.=
block_diagonal (
<*(block_diagonal (R,a))*>,
a)
by Th34
.=
block_diagonal (
(<*(Deleting (A,i,j))*> ^ <*(block_diagonal (R,a))*>),
a)
by A18, 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),a)then A19:
width A = width (DelLine (A,i))
by A13, LAPLACE:4;
thus Deleting (
(block_diagonal ((<*A*> ^ R),a)),
i,
j) =
DelCol (
(DelLine ((block_diagonal ((<*A*> ^ R),a)),i)),
j)
.=
DelCol (
(block_diagonal ((<*(DelLine (A,i))*> ^ R),a)),
j)
by A1, A19, Th41
.=
block_diagonal (
(<*(DelCol ((DelLine (A,i)),j))*> ^ R),
a)
by A2, A4, A19, Th43
.=
block_diagonal (
(<*(Deleting (A,i,j))*> ^ R),
a)
;
verum end;