let K be Field; for A being Matrix of K
for N being finite without_zero Subset of NAT st N c= Seg (width A) & ( for i being Nat st i in (Seg (width A)) \ N holds
Col (A,i) = (len A) |-> (0. K) ) holds
the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))
let A be Matrix of K; for N being finite without_zero Subset of NAT st N c= Seg (width A) & ( for i being Nat st i in (Seg (width A)) \ N holds
Col (A,i) = (len A) |-> (0. K) ) holds
the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))
let N be finite without_zero Subset of NAT; ( N c= Seg (width A) & ( for i being Nat st i in (Seg (width A)) \ N holds
Col (A,i) = (len A) |-> (0. K) ) implies the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N)) )
assume that
A1:
N c= Seg (width A)
and
A2:
for i being Nat st i in (Seg (width A)) \ N holds
Col (A,i) = (len A) |-> (0. K)
; the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))
A3:
dom A = Seg (len A)
by FINSEQ_1:def 3;
per cases
( card N = 0 or card N > 0 )
;
suppose A4:
card N = 0
;
the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))
the_rank_of A = 0
proof
A5:
N = {}
by A4;
assume
the_rank_of A <> 0
;
contradiction
then consider i,
j being
Nat such that A6:
[i,j] in Indices A
and A7:
A * (
i,
j)
<> 0. K
by MATRIX13:94;
A8:
j in Seg (width A)
by A6, ZFMISC_1:87;
A9:
i in dom A
by A6, ZFMISC_1:87;
then 0. K =
((len A) |-> (0. K)) . i
by A3, FINSEQ_2:57
.=
(Col (A,j)) . i
by A2, A8, A5
.=
A * (
i,
j)
by A9, MATRIX_0:def 8
;
hence
contradiction
by A7;
verum
end; hence
the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))
by A4, MATRIX13:77;
verum end; suppose A10:
card N > 0
;
the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))then
N <> {}
;
then
Seg (width A) <> {}
by A1, XBOOLE_1:3;
then A11:
width A <> 0
;
then A12:
len A <> 0
by MATRIX_0:def 3;
set AT =
A @ ;
A13:
[:(dom A),N:] c= Indices A
by A1, ZFMISC_1:95;
A14:
width (A @) = len A
by A11, MATRIX_0:54;
A15:
len (A @) = width A
by A11, MATRIX_0:54;
then A16:
N c= dom (A @)
by A1, FINSEQ_1:def 3;
A17:
dom (A @) = Seg (len (A @))
by FINSEQ_1:def 3;
A18:
now for i being Nat st i in (dom (A @)) \ N holds
Line ((A @),i) = (width (A @)) |-> (0. K)let i be
Nat;
( i in (dom (A @)) \ N implies Line ((A @),i) = (width (A @)) |-> (0. K) )assume A19:
i in (dom (A @)) \ N
;
Line ((A @),i) = (width (A @)) |-> (0. K)
i in dom (A @)
by A19, XBOOLE_0:def 5;
hence Line (
(A @),
i) =
Col (
A,
i)
by A15, A17, MATRIX_0:59
.=
(width (A @)) |-> (0. K)
by A2, A15, A14, A17, A19
;
verum end; thus the_rank_of A =
the_rank_of (A @)
by MATRIX13:84
.=
the_rank_of (Segm ((A @),N,(Seg (len A))))
by A14, A16, A18, Th11
.=
the_rank_of ((Segm (A,(Seg (len A)),N)) @)
by A3, A10, A12, A13, MATRIX13:61
.=
the_rank_of (Segm (A,(Seg (len A)),N))
by MATRIX13:84
;
verum end; end;