let K be Field; :: thesis: for A being Matrix of K st ( width A = 0 implies len A = 0 ) & the_rank_of A = 0 holds
Space_of_Solutions_of A = (width A) -VectSp_over K
let A be Matrix of K; :: thesis: ( ( width A = 0 implies len A = 0 ) & the_rank_of A = 0 implies Space_of_Solutions_of A = (width A) -VectSp_over K )
assume that
A1: ( width A = 0 implies len A = 0 ) and
A2: the_rank_of A = 0 ; :: thesis: Space_of_Solutions_of A = (width A) -VectSp_over K
set L = (len A) |-> (0. K);
the carrier of ((width A) -VectSp_over K) c= Solutions_of (A,((len A) |-> (0. K)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of ((width A) -VectSp_over K) or x in Solutions_of (A,((len A) |-> (0. K))) )
assume A3: x in the carrier of ((width A) -VectSp_over K) ; :: thesis: x in Solutions_of (A,((len A) |-> (0. K)))
reconsider x9 = x as Element of (width A) -tuples_on the carrier of K by A3, MATRIX13:102;
A4: ( A = 0. (K,(len A),(width A)) & ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) ) by A2, Th32, MATRIX13:95;
per cases ( len A = 0 or len A > 0 ) ;
suppose A5: len A = 0 ; :: thesis: x in Solutions_of (A,((len A) |-> (0. K)))
then Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) = {{}} by A4, Th51;
then A6: {} in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) by TARSKI:def 1;
then consider f being FinSequence of K such that
A7: {} = ColVec2Mx f and
A8: len f = width A by Th58;
width A = 0 by A5, MATRIX_0:def 3;
then the carrier of ((width A) -VectSp_over K) = 0 -tuples_on the carrier of K by MATRIX13:102
.= {(<*> the carrier of K)} by FINSEQ_2:94 ;
then x = <*> the carrier of K by A3, TARSKI:def 1;
then f = x by A5, A8, MATRIX_0:def 3;
hence x in Solutions_of (A,((len A) |-> (0. K))) by A6, A7; :: thesis: verum
end;
suppose A9: len A > 0 ; :: thesis: x in Solutions_of (A,((len A) |-> (0. K)))
A10: len x9 = width A by CARD_1:def 7;
Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) = { X where X is Matrix of width A,1,K : verum } by A1, A4, A9, Th54;
then ColVec2Mx x9 in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) by A10;
hence x in Solutions_of (A,((len A) |-> (0. K))) ; :: thesis: verum
end;
end;
end;
then the carrier of ((width A) -VectSp_over K) = Solutions_of (A,((len A) |-> (0. K)))
.= the carrier of (Space_of_Solutions_of A) by A1, Def5 ;
hence Space_of_Solutions_of A = (width A) -VectSp_over K by VECTSP_4:31; :: thesis: verum