let K be Field; :: thesis: for A being Matrix of K st Space_of_Solutions_of A = (width A) -VectSp_over K holds

the_rank_of A = 0

let A be Matrix of K; :: thesis: ( Space_of_Solutions_of A = (width A) -VectSp_over K implies the_rank_of A = 0 )

assume A1: Space_of_Solutions_of A = (width A) -VectSp_over K ; :: thesis: the_rank_of A = 0

assume the_rank_of A <> 0 ; :: thesis: contradiction

then consider i, j being Nat such that

A2: [i,j] in Indices A and

A3: A * (i,j) <> 0. K by MATRIX13:94;

A4: j in Seg (width A) by A2, ZFMISC_1:87;

then A5: width A <> 0 ;

set L = Line ((1. (K,(width A))),j);

A6: width (1. (K,(width A))) = width A by MATRIX_0:24;

then A7: dom (Line ((1. (K,(width A))),j)) = Seg (width A) by FINSEQ_2:124;

A8: Indices (1. (K,(width A))) = [:(Seg (width A)),(Seg (width A)):] by MATRIX_0:24;

[j,j] in Indices (1. (K,(width A))) by A4, A8, ZFMISC_1:87;

then 1_ K = (1. (K,(width A))) * (j,j) by MATRIX_1:def 3

.= (Line ((1. (K,(width A))),j)) . j by A4, A6, MATRIX_0:def 7 ;

then A13: Sum (mlt ((Line ((1. (K,(width A))),j)),(Line (A,i)))) = (Line (A,i)) . j by A4, A7, A12, A9, MATRIX_3:17

.= A * (i,j) by A4, MATRIX_0:def 7 ;

A14: ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;

A15: i in dom A by A2, ZFMISC_1:87;

Line ((1. (K,(width A))),j) in (width A) -tuples_on the carrier of K by A6;

then Line ((1. (K,(width A))),j) in the carrier of (Space_of_Solutions_of A) by A1, MATRIX13:102;

then Line ((1. (K,(width A))),j) in Solutions_of (A,((len A) |-> (0. K))) by Def5, A5;

then consider f being FinSequence of K such that

A16: f = Line ((1. (K,(width A))),j) and

A17: ColVec2Mx f in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) ;

consider X being Matrix of K such that

A18: X = ColVec2Mx f and

A19: len X = width A and

width X = width (ColVec2Mx ((len A) |-> (0. K))) and

A20: A * X = ColVec2Mx ((len A) |-> (0. K)) by A17;

A21: 1 in Seg 1 ;

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

then len A <> 0 by A2, ZFMISC_1:87;

then Indices (ColVec2Mx ((len A) |-> (0. K))) = [:(Seg (len A)),(Seg 1):] by A14, MATRIX_0:23;

then A23: [i,1] in Indices (ColVec2Mx ((len A) |-> (0. K))) by A15, A22, A21, ZFMISC_1:87;

then (Line (A,i)) "*" (Col (X,1)) = (0. (K,(len A),1)) * (i,1) by A19, A20, A14, MATRIX_3:def 4

.= 0. K by A14, A23, MATRIX_3:1 ;

then 0. K = (Col (X,1)) "*" (Line (A,i)) by FVSUM_1:90

.= Sum (mlt (f,(Line (A,i)))) by A18, A19, Th26, A5 ;

hence contradiction by A3, A16, A13; :: thesis: verum

the_rank_of A = 0

let A be Matrix of K; :: thesis: ( Space_of_Solutions_of A = (width A) -VectSp_over K implies the_rank_of A = 0 )

assume A1: Space_of_Solutions_of A = (width A) -VectSp_over K ; :: thesis: the_rank_of A = 0

assume the_rank_of A <> 0 ; :: thesis: contradiction

then consider i, j being Nat such that

A2: [i,j] in Indices A and

A3: A * (i,j) <> 0. K by MATRIX13:94;

A4: j in Seg (width A) by A2, ZFMISC_1:87;

then A5: width A <> 0 ;

set L = Line ((1. (K,(width A))),j);

A6: width (1. (K,(width A))) = width A by MATRIX_0:24;

then A7: dom (Line ((1. (K,(width A))),j)) = Seg (width A) by FINSEQ_2:124;

A8: Indices (1. (K,(width A))) = [:(Seg (width A)),(Seg (width A)):] by MATRIX_0:24;

A9: now :: thesis: for k being Nat st k in dom (Line ((1. (K,(width A))),j)) & k <> j holds

0. K = (Line ((1. (K,(width A))),j)) . k

A12:
dom (Line (A,i)) = Seg (width A)
by FINSEQ_2:124;0. K = (Line ((1. (K,(width A))),j)) . k

let k be Nat; :: thesis: ( k in dom (Line ((1. (K,(width A))),j)) & k <> j implies 0. K = (Line ((1. (K,(width A))),j)) . k )

assume that

A10: k in dom (Line ((1. (K,(width A))),j)) and

A11: k <> j ; :: thesis: 0. K = (Line ((1. (K,(width A))),j)) . k

[j,k] in Indices (1. (K,(width A))) by A4, A7, A8, A10, ZFMISC_1:87;

hence 0. K = (1. (K,(width A))) * (j,k) by A11, MATRIX_1:def 3

.= (Line ((1. (K,(width A))),j)) . k by A6, A7, A10, MATRIX_0:def 7 ;

:: thesis: verum

end;assume that

A10: k in dom (Line ((1. (K,(width A))),j)) and

A11: k <> j ; :: thesis: 0. K = (Line ((1. (K,(width A))),j)) . k

[j,k] in Indices (1. (K,(width A))) by A4, A7, A8, A10, ZFMISC_1:87;

hence 0. K = (1. (K,(width A))) * (j,k) by A11, MATRIX_1:def 3

.= (Line ((1. (K,(width A))),j)) . k by A6, A7, A10, MATRIX_0:def 7 ;

:: thesis: verum

[j,j] in Indices (1. (K,(width A))) by A4, A8, ZFMISC_1:87;

then 1_ K = (1. (K,(width A))) * (j,j) by MATRIX_1:def 3

.= (Line ((1. (K,(width A))),j)) . j by A4, A6, MATRIX_0:def 7 ;

then A13: Sum (mlt ((Line ((1. (K,(width A))),j)),(Line (A,i)))) = (Line (A,i)) . j by A4, A7, A12, A9, MATRIX_3:17

.= A * (i,j) by A4, MATRIX_0:def 7 ;

A14: ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;

A15: i in dom A by A2, ZFMISC_1:87;

Line ((1. (K,(width A))),j) in (width A) -tuples_on the carrier of K by A6;

then Line ((1. (K,(width A))),j) in the carrier of (Space_of_Solutions_of A) by A1, MATRIX13:102;

then Line ((1. (K,(width A))),j) in Solutions_of (A,((len A) |-> (0. K))) by Def5, A5;

then consider f being FinSequence of K such that

A16: f = Line ((1. (K,(width A))),j) and

A17: ColVec2Mx f in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) ;

consider X being Matrix of K such that

A18: X = ColVec2Mx f and

A19: len X = width A and

width X = width (ColVec2Mx ((len A) |-> (0. K))) and

A20: A * X = ColVec2Mx ((len A) |-> (0. K)) by A17;

A21: 1 in Seg 1 ;

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

then len A <> 0 by A2, ZFMISC_1:87;

then Indices (ColVec2Mx ((len A) |-> (0. K))) = [:(Seg (len A)),(Seg 1):] by A14, MATRIX_0:23;

then A23: [i,1] in Indices (ColVec2Mx ((len A) |-> (0. K))) by A15, A22, A21, ZFMISC_1:87;

then (Line (A,i)) "*" (Col (X,1)) = (0. (K,(len A),1)) * (i,1) by A19, A20, A14, MATRIX_3:def 4

.= 0. K by A14, A23, MATRIX_3:1 ;

then 0. K = (Col (X,1)) "*" (Line (A,i)) by FVSUM_1:90

.= Sum (mlt (f,(Line (A,i)))) by A18, A19, Th26, A5 ;

hence contradiction by A3, A16, A13; :: thesis: verum