let n be Nat; for K being Field
for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
(Delete (M,i,j)) @ = Delete ((M @),j,i)
let K be Field; for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
(Delete (M,i,j)) @ = Delete ((M @),j,i)
let M be Matrix of n,K; for i, j being Nat st i in Seg n & j in Seg n holds
(Delete (M,i,j)) @ = Delete ((M @),j,i)
let i, j be Nat; ( i in Seg n & j in Seg n implies (Delete (M,i,j)) @ = Delete ((M @),j,i) )
assume that
A1:
i in Seg n
and
A2:
j in Seg n
; (Delete (M,i,j)) @ = Delete ((M @),j,i)
n > 0
by A1;
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
set X1 = Seg n;
reconsider MT = M @ as Matrix of n,K ;
set D = Delete (M,i,j);
set n9 = n -' 1;
reconsider I = i as Element of NAT by ORDINAL1:def 12;
reconsider DT = (Delete (M,i,j)) @ as Matrix of n -' 1,K ;
set D9 = Delete (MT,j,i);
set X = Seg (n -' 1);
A3:
(n1 + 1) -' 1 = n1
by NAT_D:34;
now for k, m being Nat st [k,m] in Indices DT holds
DT * (k,m) = (Delete (MT,j,i)) * (k,m)
n -' 1
<= n
by NAT_D:35;
then A4:
Seg (n -' 1) c= Seg n
by FINSEQ_1:5;
let k,
m be
Nat;
( [k,m] in Indices DT implies DT * (b1,b2) = (Delete (MT,j,i)) * (b1,b2) )assume A5:
[k,m] in Indices DT
;
DT * (b1,b2) = (Delete (MT,j,i)) * (b1,b2)
[m,k] in Indices (Delete (M,i,j))
by A5, MATRIX_0:def 6;
then A6:
DT * (
k,
m)
= (Delete (M,i,j)) * (
m,
k)
by MATRIX_0:def 6;
reconsider k9 =
k,
m9 =
m as
Element of
NAT by ORDINAL1:def 12;
A7:
Indices DT = [:(Seg (n -' 1)),(Seg (n -' 1)):]
by MATRIX_0:24;
then A8:
k in Seg (n -' 1)
by A5, ZFMISC_1:87;
then A9:
k + 1
in Seg n
by A3, FINSEQ_1:60;
A10:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
A11:
m in Seg (n -' 1)
by A5, A7, ZFMISC_1:87;
then A12:
m + 1
in Seg n
by A3, FINSEQ_1:60;
per cases
( ( m9 < I & k9 < j ) or ( m9 < I & k9 >= j ) or ( m9 >= I & k9 < j ) or ( m9 >= I & k9 >= j ) )
;
suppose A13:
(
m9 < I &
k9 < j )
;
DT * (b1,b2) = (Delete (MT,j,i)) * (b1,b2)then A14:
(Delete (MT,j,i)) * (
k,
m)
= MT * (
k,
m)
by A1, A2, A8, A11, Th13;
A15:
[m,k] in Indices M
by A8, A11, A4, A10, ZFMISC_1:87;
(Delete (M,i,j)) * (
m,
k)
= M * (
m,
k)
by A1, A2, A8, A11, A13, Th13;
hence
DT * (
k,
m)
= (Delete (MT,j,i)) * (
k,
m)
by A6, A15, A14, MATRIX_0:def 6;
verum end; suppose A16:
(
m9 < I &
k9 >= j )
;
DT * (b1,b2) = (Delete (MT,j,i)) * (b1,b2)then A17:
(Delete (MT,j,i)) * (
k,
m)
= MT * (
(k + 1),
m)
by A1, A2, A8, A11, Th13;
A18:
[m,(k + 1)] in Indices M
by A11, A4, A9, A10, ZFMISC_1:87;
(Delete (M,i,j)) * (
m,
k)
= M * (
m,
(k + 1))
by A1, A2, A8, A11, A16, Th13;
hence
DT * (
k,
m)
= (Delete (MT,j,i)) * (
k,
m)
by A6, A18, A17, MATRIX_0:def 6;
verum end; suppose A19:
(
m9 >= I &
k9 < j )
;
DT * (b1,b2) = (Delete (MT,j,i)) * (b1,b2)then A20:
(Delete (MT,j,i)) * (
k,
m)
= MT * (
k,
(m + 1))
by A1, A2, A8, A11, Th13;
A21:
[(m + 1),k] in Indices M
by A8, A4, A12, A10, ZFMISC_1:87;
(Delete (M,i,j)) * (
m,
k)
= M * (
(m + 1),
k)
by A1, A2, A8, A11, A19, Th13;
hence
DT * (
k,
m)
= (Delete (MT,j,i)) * (
k,
m)
by A6, A21, A20, MATRIX_0:def 6;
verum end; suppose A22:
(
m9 >= I &
k9 >= j )
;
DT * (b1,b2) = (Delete (MT,j,i)) * (b1,b2)then A23:
(Delete (MT,j,i)) * (
k,
m)
= MT * (
(k + 1),
(m + 1))
by A1, A2, A8, A11, Th13;
A24:
[(m + 1),(k + 1)] in Indices M
by A9, A12, A10, ZFMISC_1:87;
(Delete (M,i,j)) * (
m,
k)
= M * (
(m + 1),
(k + 1))
by A1, A2, A8, A11, A22, Th13;
hence
DT * (
k,
m)
= (Delete (MT,j,i)) * (
k,
m)
by A6, A24, A23, MATRIX_0:def 6;
verum end; end;
hence
(Delete (M,i,j)) @ = Delete ((M @),j,i)
by MATRIX_0:27; verum