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
set ;
:: 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 x' =
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
len A = 0
;
:: thesis: x in Solutions_of A,((len A) |-> (0. K))then A5:
(
Solutions_of A,
(ColVec2Mx ((len A) |-> (0. K))) = {{} } &
width A = 0 )
by A4, Th51, MATRIX_1:def 4;
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:112
;
then A6:
x = <*> the
carrier of
K
by A3, TARSKI:def 1;
A7:
{} in Solutions_of A,
(ColVec2Mx ((len A) |-> (0. K)))
by A5, TARSKI:def 1;
then consider f being
FinSequence of
K such that A8:
(
{} = ColVec2Mx f &
len f = width A )
by Th58;
f = x
by A5, A6, A8;
hence
x in Solutions_of A,
((len A) |-> (0. K))
by A7, A8;
:: thesis: verum end;
end;
then the carrier of ((width A) -VectSp_over K) =
Solutions_of A,((len A) |-> (0. K))
by XBOOLE_0:def 10
.=
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:39; :: thesis: verum