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, Def2;
then consider v being
object such that A2:
I = {v}
by CARD_2:42;
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:8;
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:8, RUSUB_1:def 3;
then A5:
{v} is Basis of V
by RUSUB_3:def 2;
card {v} = 1
by CARD_1:30;
hence
dim V = 1
by A5, Def2; verum