let i be Nat; for K being Field
for M being Matrix of K st Line M,i = (width M) |-> (0. K) holds
the_rank_of (DelLine M,i) = the_rank_of M
let K be Field; for M being Matrix of K st Line M,i = (width M) |-> (0. K) holds
the_rank_of (DelLine M,i) = the_rank_of M
let M be Matrix of K; ( Line M,i = (width M) |-> (0. K) implies the_rank_of (DelLine M,i) = the_rank_of M )
set D = DelLine M,i;
A1:
Indices M = [:(Seg (len M)),(Seg (width M)):]
by FINSEQ_1:def 3;
A2:
Segm M,((Seg (len M)) \ {i}),(Seg (width M)) = DelLine M,i
by Th51;
consider P, Q being finite without_zero Subset of NAT such that
A3:
[:P,Q:] c= Indices (DelLine M,i)
and
A4:
card P = card Q
and
A5:
card P = the_rank_of (DelLine M,i)
and
A6:
Det (EqSegm (DelLine M,i),P,Q) <> 0. K
by Def4;
EqSegm (DelLine M,i),P,Q = Segm (DelLine M,i),P,Q
by A4, Def3;
then A7:
the_rank_of (Segm (DelLine M,i),P,Q) = card P
by A6, Th83;
( P = {} iff Q = {} )
by A4;
then consider P2, Q2 being finite without_zero Subset of NAT such that
A8:
P2 c= (Seg (len M)) \ {i}
and
A9:
Q2 c= Seg (width M)
and
P2 = (Sgm ((Seg (len M)) \ {i})) .: P
and
Q2 = (Sgm (Seg (width M))) .: Q
and
card P2 = card P
and
card Q2 = card Q
and
A10:
Segm (DelLine M,i),P,Q = Segm M,P2,Q2
by A3, A2, Th57;
(Seg (len M)) \ {i} c= Seg (len M)
by XBOOLE_1:36;
then
P2 c= Seg (len M)
by A8, XBOOLE_1:1;
then
[:P2,Q2:] c= Indices M
by A9, A1, ZFMISC_1:119;
then A11:
the_rank_of (DelLine M,i) <= the_rank_of M
by A5, A10, A7, Th79;
consider p, q being finite without_zero Subset of NAT such that
A12:
[:p,q:] c= Indices M
and
A13:
card p = card q
and
A14:
card p = the_rank_of M
and
A15:
Det (EqSegm M,p,q) <> 0. K
by Def4;
EqSegm M,p,q = Segm M,p,q
by A13, Def3;
then A16:
the_rank_of (Segm M,p,q) = card p
by A15, Th83;
assume A17:
Line M,i = (width M) |-> (0. K)
; the_rank_of (DelLine M,i) = the_rank_of M
not i in p
proof
assume A18:
i in p
;
contradiction
then reconsider i0 =
i as non
zero Element of
NAT ;
{i} c= p
by A18, ZFMISC_1:37;
then consider q1 being
finite without_zero Subset of
NAT such that A19:
q1 c= q
and A20:
card {i} = card q1
and A21:
Det (EqSegm M,{i0},q1) <> 0. K
by A13, A15, Th65;
consider y being
set such that A22:
{y} = q1
by A20, CARD_2:60;
A23:
card {i} = 1
by CARD_1:50;
A24:
q c= Seg (width M)
by A12, A13, Th67;
y in {y}
by TARSKI:def 1;
then reconsider y =
y as non
zero Element of
NAT by A22;
y in q1
by A22, TARSKI:def 1;
then A25:
y in q
by A19;
then A26:
M * i0,
y = (Line M,i) . y
by A24, MATRIX_1:def 8;
A27:
(Line M,i) . y = 0. K
by A17, A25, A24, FINSEQ_2:71;
EqSegm M,
{i0},
q1 =
Segm M,
{i0},
{y}
by A20, A22, Def3
.=
<*<*(0. K)*>*>
by A26, A27, Th44
;
hence
contradiction
by A21, A23, MATRIX_3:36;
verum
end;
then A28:
p \ {i} = p
by ZFMISC_1:65;
p c= Seg (len M)
by A12, A13, Th67;
then A29:
p c= (Seg (len M)) \ {i}
by A28, XBOOLE_1:33;
q c= Seg (width M)
by A12, A13, Th67;
then
the_rank_of (Segm M,p,q) <= the_rank_of (DelLine M,i)
by A2, A29, Th80;
hence
the_rank_of (DelLine M,i) = the_rank_of M
by A11, A14, A16, XXREAL_0:1; verum