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 ((R ^ <*A*>),a)),(i + (Sum (Len R))),(j + (Sum (Len R)))) = block_diagonal ((R ^ <*(Deleting (A,i,j))*>),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 ((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; 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; 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; ( 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 that
A1:
i in dom A
and
A2:
j in Seg n
; Deleting ((block_diagonal ((R ^ <*A*>),a)),(i + (Sum (Len R))),(j + (Sum (Len R)))) = block_diagonal ((R ^ <*(Deleting (A,i,j))*>),a)
n <> 0
by A2;
then A3:
n >= 1
by NAT_1:14;
set jS = j + (Sum (Len R));
set iS = i + (Sum (Len R));
set AA = <*A*>;
set b = block_diagonal (R,a);
set B = <*(block_diagonal (R,a))*>;
set LRA = Sum (Len (R ^ <*A*>));
set LBA = Sum (Len (<*(block_diagonal (R,a))*> ^ <*A*>));
A4:
width A = n
by MATRIX_0:24;
A5:
Len R = Width R
by Th46;
A6:
len A = n
by MATRIX_0:24;
then A7:
dom A = Seg n
by FINSEQ_1:def 3;
A8:
Width <*A*> = <*(width A)*>
by Th19;
A9:
len (block_diagonal (R,a)) = Sum (Len R)
by Def5;
A10:
Len (<*(block_diagonal (R,a))*> ^ <*A*>) = Width (<*(block_diagonal (R,a))*> ^ <*A*>)
by Th46;
A11:
Len <*A*> = <*(len A)*>
by Th15;
then A12:
Sum (Len <*A*>) = len A
by RVSUM_1:73;
Len (<*(block_diagonal (R,a))*> ^ <*A*>) = (Len <*(block_diagonal (R,a))*>) ^ (Len <*A*>)
by Th14;
then A13:
Sum (Len (<*(block_diagonal (R,a))*> ^ <*A*>)) = (len A) + (Sum (Len <*(block_diagonal (R,a))*>))
by A11, RVSUM_1:74;
A14:
Width <*(block_diagonal (R,a))*> = <*(width (block_diagonal (R,a)))*>
by Th19;
then A15:
Sum (Width <*(block_diagonal (R,a))*>) = width (block_diagonal (R,a))
by RVSUM_1:73;
Width (<*(block_diagonal (R,a))*> ^ <*A*>) = (Width <*(block_diagonal (R,a))*>) ^ (Width <*A*>)
by Th18;
then A16:
Sum (Len (<*(block_diagonal (R,a))*> ^ <*A*>)) = (Sum (Width <*A*>)) + (width (block_diagonal (R,a)))
by A14, A10, RVSUM_1:76;
Len <*(block_diagonal (R,a))*> = <*(len (block_diagonal (R,a)))*>
by Th15;
then A17:
Sum (Len <*(block_diagonal (R,a))*>) = len (block_diagonal (R,a))
by RVSUM_1:73;
per cases
( n = 1 or n > 1 )
by A3, XXREAL_0:1;
suppose A18:
n = 1
;
Deleting ((block_diagonal ((R ^ <*A*>),a)),(i + (Sum (Len R))),(j + (Sum (Len R)))) = block_diagonal ((R ^ <*(Deleting (A,i,j))*>),a)then A19:
i = 1
by A1, A7, FINSEQ_1:2, TARSKI:def 1;
A20:
j = 1
by A2, A18, FINSEQ_1:2, TARSKI:def 1;
len (Deleting (A,i,j)) =
1
-' 1
by A1, A18, LAPLACE:2
.=
0
by XREAL_1:232
;
then A21:
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 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 A6, A9, A13, A17, A18, A19, FINSEQ_1:10
.=
Segm (
(block_diagonal ((<*(block_diagonal (R,a))*> ^ <*A*>),a)),
(Seg (Sum (Len <*(block_diagonal (R,a))*>))),
(Seg (Sum (Width <*(block_diagonal (R,a))*>))))
by A6, A4, A9, A11, A8, A13, A16, A17, A12, A15, A18, A20, FINSEQ_1:10
.=
block_diagonal (
R,
a)
by A17, A15, Th32
.=
block_diagonal (
<*(block_diagonal (R,a))*>,
a)
by Th34
.=
block_diagonal (
(<*(block_diagonal (R,a))*> ^ <*(Deleting (A,i,j))*>),
a)
by A21, Th40
.=
block_diagonal (
(R ^ <*(Deleting (A,i,j))*>),
a)
by Th35
;
verum end; suppose
n > 1
;
Deleting ((block_diagonal ((R ^ <*A*>),a)),(i + (Sum (Len R))),(j + (Sum (Len R)))) = block_diagonal ((R ^ <*(Deleting (A,i,j))*>),a)then A22:
width A = width (DelLine (A,i))
by A6, 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))))
.=
DelCol (
(block_diagonal ((R ^ <*(DelLine (A,i))*>),a)),
(j + (Sum (Len R))))
by A1, A22, Th42
.=
block_diagonal (
(R ^ <*(DelCol ((DelLine (A,i)),j))*>),
a)
by A2, A4, A5, A22, Th44
.=
block_diagonal (
(R ^ <*(Deleting (A,i,j))*>),
a)
;
verum end;