let V be finite-dimensional RealUnitarySpace; ( dim V = 1 iff ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) )
hereby ( ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) implies dim V = 1 )
consider I being
finite Subset of
V such that A1:
I is
Basis of
V
by Def1;
assume
dim V = 1
;
ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} )then
card I = 1
by A1, Def3;
then consider v being
set such that A2:
I = {v}
by CARD_2:60;
v in I
by A2, TARSKI:def 1;
then reconsider v =
v as
VECTOR of
V ;
{v} is
linearly-independent
by A1, A2, RUSUB_3:def 2;
then A3:
v <> 0. V
by RLVECT_3:9;
Lin {v} = UNITSTR(# the
carrier of
V,the
ZeroF of
V,the
addF of
V,the
Mult of
V,the
scalar of
V #)
by A1, A2, RUSUB_3:def 2;
hence
ex
v being
VECTOR of
V st
(
v <> 0. V &
(Omega). V = Lin {v} )
by A3, RUSUB_1:def 3;
verum
end;
given v being VECTOR of V such that A4:
( v <> 0. V & (Omega). V = Lin {v} )
; dim V = 1
( {v} is linearly-independent & Lin {v} = UNITSTR(# the carrier of V,the ZeroF of V,the addF of V,the Mult of V,the scalar of V #) )
by A4, RLVECT_3:9, RUSUB_1:def 3;
then A5:
{v} is Basis of V
by RUSUB_3:def 2;
card {v} = 1
by CARD_1:50;
hence
dim V = 1
by A5, Def3; verum