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;
then
[:P2,Q2:] c= Indices M
by A9, A1, ZFMISC_1:96;
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:31;
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
object such that A22:
{y} = q1
by A20, CARD_2:42;
A23:
card {i} = 1
by CARD_1:30;
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_0:def 7;
A27:
(Line (M,i)) . y = 0. K
by A17, A25, A24, FINSEQ_2:57;
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:34;
verum
end;
then A28:
p \ {i} = p
by ZFMISC_1:57;
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