let i, j, n be Nat; for K being Field
for M being Matrix of n,K holds Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)
let K be Field; for M being Matrix of n,K holds Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)
let M be Matrix of n,K; Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)
A1:
width M = n
by MATRIX_0:24;
A2:
len M = n
by MATRIX_0:24;
then A3:
dom M = Seg n
by FINSEQ_1:def 3;
per cases
( not i in Seg n or i in Seg n )
;
suppose A4:
not
i in Seg n
;
Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)then A5:
Seg n = (Seg n) \ {i}
by ZFMISC_1:57;
Del (
M,
i)
= M
by A3, A4, FINSEQ_3:104;
hence
Segm (
M,
((Seg n) \ {i}),
((Seg n) \ {j}))
= Deleting (
M,
i,
j)
by A2, A1, A5, Th52;
verum end; suppose A6:
i in Seg n
;
Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)set Q1 =
Seg n;
set Q =
(Seg n) \ {j};
set P =
(Seg n) \ {i};
set SS =
Segm (
M,
((Seg n) \ {i}),
(Seg n));
consider m being
Nat such that A7:
len M = m + 1
and A8:
len (Del (M,i)) = m
by A3, A6, FINSEQ_3:104;
per cases
( m = 0 or m > 0 )
;
suppose A9:
m = 0
;
Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)then
len (Deleting (M,i,j)) = 0
by A8, MATRIX_0:def 13;
then A10:
Deleting (
M,
i,
j)
= {}
;
A11:
(Seg n) \ {1} = {}
by A2, A7, A9, FINSEQ_1:2, XBOOLE_1:37;
i = 1
by A2, A6, A7, A9, FINSEQ_1:2, TARSKI:def 1;
then
len (Segm (M,((Seg n) \ {i}),((Seg n) \ {j}))) = 0
by A11, MATRIX_0:def 2;
hence
Segm (
M,
((Seg n) \ {i}),
((Seg n) \ {j}))
= Deleting (
M,
i,
j)
by A10;
verum end; suppose
m > 0
;
Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)then
n > 1
+ 0
by A2, A7, XREAL_1:8;
then A12:
n = width (DelLine (M,i))
by A2, A1, LAPLACE:4;
A13:
(Seg n) \ {j} c= Seg n
by XBOOLE_1:36;
(Seg n) \ {i} c= Seg n
by XBOOLE_1:36;
then A14:
rng (Sgm ((Seg n) \ {i})) = (Seg n) \ {i}
by FINSEQ_1:def 13;
dom (Sgm ((Seg n) \ {i})) = Seg (card ((Seg n) \ {i}))
by FINSEQ_3:40, XBOOLE_1:36;
then A15:
(Sgm ((Seg n) \ {i})) " ((Seg n) \ {i}) =
Seg (card ((Seg n) \ {i}))
by A14, RELAT_1:134
.=
Seg (len (Segm (M,((Seg n) \ {i}),(Seg n))))
by MATRIX_0:def 2
;
A16:
Segm (
M,
((Seg n) \ {i}),
(Seg n))
= Del (
M,
i)
by A2, A1, Th51;
then A17:
Deleting (
M,
i,
j)
= Segm (
(Segm (M,((Seg n) \ {i}),(Seg n))),
(Seg (len (Segm (M,((Seg n) \ {i}),(Seg n))))),
((Seg (width (Segm (M,((Seg n) \ {i}),(Seg n))))) \ {j}))
by Th52;
Sgm (Seg n) = idseq n
by FINSEQ_3:48;
then
(Sgm (Seg n)) " ((Seg n) \ {j}) = (Seg (width (Segm (M,((Seg n) \ {i}),(Seg n))))) \ {j}
by A13, A12, A16, FUNCT_2:94;
hence
Segm (
M,
((Seg n) \ {i}),
((Seg n) \ {j}))
= Deleting (
M,
i,
j)
by A13, A15, A17, Th56;
verum end; end;