let K be Field; :: thesis: for A being Matrix of K

for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ) holds

the_rank_of A = the_rank_of (Segm (A,N,(Seg (width A))))

let A be Matrix of K; :: thesis: for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ) holds

the_rank_of A = the_rank_of (Segm (A,N,(Seg (width A))))

let N be finite without_zero Subset of NAT; :: thesis: ( N c= dom A & ( for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ) implies the_rank_of A = the_rank_of (Segm (A,N,(Seg (width A)))) )

assume that

A1: N c= dom A and

A2: for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ; :: thesis: the_rank_of A = the_rank_of (Segm (A,N,(Seg (width A))))

set w = width A;

set l = len A;

reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;

set S = Segm (A9,N,(Seg (width A9)));

consider U being finite Subset of ((width A) -VectSp_over K) such that

A3: U is linearly-independent and

A4: U c= lines A9 and

A5: card U = the_rank_of A9 by MATRIX13:123;

A6: U c= lines (Segm (A9,N,(Seg (width A9))))

hence the_rank_of A = the_rank_of (Segm (A,N,(Seg (width A)))) by A3, A5, A6, A15, MATRIX13:123; :: thesis: verum

for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ) holds

the_rank_of A = the_rank_of (Segm (A,N,(Seg (width A))))

let A be Matrix of K; :: thesis: for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ) holds

the_rank_of A = the_rank_of (Segm (A,N,(Seg (width A))))

let N be finite without_zero Subset of NAT; :: thesis: ( N c= dom A & ( for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ) implies the_rank_of A = the_rank_of (Segm (A,N,(Seg (width A)))) )

assume that

A1: N c= dom A and

A2: for i being Nat st i in (dom A) \ N holds

Line (A,i) = (width A) |-> (0. K) ; :: thesis: the_rank_of A = the_rank_of (Segm (A,N,(Seg (width A))))

set w = width A;

set l = len A;

reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;

set S = Segm (A9,N,(Seg (width A9)));

consider U being finite Subset of ((width A) -VectSp_over K) such that

A3: U is linearly-independent and

A4: U c= lines A9 and

A5: card U = the_rank_of A9 by MATRIX13:123;

A6: U c= lines (Segm (A9,N,(Seg (width A9))))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in U or x in lines (Segm (A9,N,(Seg (width A9)))) )

assume A7: x in U ; :: thesis: x in lines (Segm (A9,N,(Seg (width A9))))

consider Ni being Nat such that

A8: Ni in Seg (len A) and

A9: x = Line (A9,Ni) by A4, A7, MATRIX13:103;

A10: dom A = Seg (len A) by FINSEQ_1:def 3;

A11: Ni in N

then consider i being object such that

A12: i in dom (Sgm N) and

A13: (Sgm N) . i = Ni by A11, FUNCT_1:def 3;

reconsider i = i as Element of NAT by A12;

A14: dom (Sgm N) = Seg (card N) by A1, A10, FINSEQ_3:40;

then Line ((Segm (A9,N,(Seg (width A9)))),i) = x by A9, A12, A13, MATRIX13:48;

hence x in lines (Segm (A9,N,(Seg (width A9)))) by A12, A14, MATRIX13:103; :: thesis: verum

end;assume A7: x in U ; :: thesis: x in lines (Segm (A9,N,(Seg (width A9))))

consider Ni being Nat such that

A8: Ni in Seg (len A) and

A9: x = Line (A9,Ni) by A4, A7, MATRIX13:103;

A10: dom A = Seg (len A) by FINSEQ_1:def 3;

A11: Ni in N

proof

rng (Sgm N) = N
by A1, A10, FINSEQ_1:def 13;
assume
not Ni in N
; :: thesis: contradiction

then Ni in (dom A) \ N by A8, A10, XBOOLE_0:def 5;

then x = (width A) |-> (0. K) by A2, A9

.= 0. ((width A) -VectSp_over K) by MATRIX13:102 ;

hence contradiction by A3, A7, VECTSP_7:2; :: thesis: verum

end;then Ni in (dom A) \ N by A8, A10, XBOOLE_0:def 5;

then x = (width A) |-> (0. K) by A2, A9

.= 0. ((width A) -VectSp_over K) by MATRIX13:102 ;

hence contradiction by A3, A7, VECTSP_7:2; :: thesis: verum

then consider i being object such that

A12: i in dom (Sgm N) and

A13: (Sgm N) . i = Ni by A11, FUNCT_1:def 3;

reconsider i = i as Element of NAT by A12;

A14: dom (Sgm N) = Seg (card N) by A1, A10, FINSEQ_3:40;

then Line ((Segm (A9,N,(Seg (width A9)))),i) = x by A9, A12, A13, MATRIX13:48;

hence x in lines (Segm (A9,N,(Seg (width A9)))) by A12, A14, MATRIX13:103; :: thesis: verum

A15: now :: thesis: for W being finite Subset of ((width A) -VectSp_over K) st W is linearly-independent & W c= lines (Segm (A9,N,(Seg (width A9)))) holds

card W <= the_rank_of A9

width A = card (Seg (width A))
by FINSEQ_1:57;card W <= the_rank_of A9

let W be finite Subset of ((width A) -VectSp_over K); :: thesis: ( W is linearly-independent & W c= lines (Segm (A9,N,(Seg (width A9)))) implies card W <= the_rank_of A9 )

assume that

A16: W is linearly-independent and

A17: W c= lines (Segm (A9,N,(Seg (width A9)))) ; :: thesis: card W <= the_rank_of A9

dom A = Seg (len A) by FINSEQ_1:def 3;

then lines (Segm (A9,N,(Seg (width A9)))) c= lines A9 by A1, MATRIX13:118;

then W c= lines A9 by A17;

hence card W <= the_rank_of A9 by A16, MATRIX13:123; :: thesis: verum

end;assume that

A16: W is linearly-independent and

A17: W c= lines (Segm (A9,N,(Seg (width A9)))) ; :: thesis: card W <= the_rank_of A9

dom A = Seg (len A) by FINSEQ_1:def 3;

then lines (Segm (A9,N,(Seg (width A9)))) c= lines A9 by A1, MATRIX13:118;

then W c= lines A9 by A17;

hence card W <= the_rank_of A9 by A16, MATRIX13:123; :: thesis: verum

hence the_rank_of A = the_rank_of (Segm (A,N,(Seg (width A)))) by A3, A5, A6, A15, MATRIX13:123; :: thesis: verum