let GF be Field; for V being finite-dimensional VectSp of GF holds
( dim V = 1 iff ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} ) )
let V be finite-dimensional VectSp of GF; ( 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 MATRLIN:def 1;
assume
dim V = 1
;
ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )then
card I = 1
by A1, Def1;
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, VECTSP_7:def 3;
then A3:
v <> 0. V
by VECTSP_7:3;
Lin {v} = ModuleStr(# the
carrier of
V, the
U5 of
V, the
ZeroF of
V, the
lmult of
V #)
by A1, A2, VECTSP_7:def 3;
hence
ex
v being
Vector of
V st
(
v <> 0. V &
(Omega). V = Lin {v} )
by A3, VECTSP_4:def 4;
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} = ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) )
by A4, VECTSP_4:def 4, VECTSP_7:3;
then A5:
{v} is Basis of V
by VECTSP_7:def 3;
card {v} = 1
by CARD_1:30;
hence
dim V = 1
by A5, Def1; verum