let K be Field; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))

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

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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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 )
;

end;

suppose A4:
card N = 0
; :: thesis: the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))

the_rank_of A = 0

end;proof

hence
the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))
by A4, MATRIX13:77; :: thesis: verum
A5:
N = {}
by A4;

assume the_rank_of A <> 0 ; :: thesis: 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; :: thesis: verum

end;assume the_rank_of A <> 0 ; :: thesis: 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; :: thesis: verum

suppose A10:
card N > 0
; :: thesis: 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;

.= 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 ; :: thesis: verum

end;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 :: thesis: for i being Nat st i in (dom (A @)) \ N holds

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

thus the_rank_of A =
the_rank_of (A @)
by MATRIX13:84
Line ((A @),i) = (width (A @)) |-> (0. K)

let i be Nat; :: thesis: ( i in (dom (A @)) \ N implies Line ((A @),i) = (width (A @)) |-> (0. K) )

assume A19: i in (dom (A @)) \ N ; :: thesis: 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 ;

:: thesis: verum

end;assume A19: i in (dom (A @)) \ N ; :: thesis: 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 ;

:: thesis: verum

.= 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 ; :: thesis: verum