let GF be Field; for V being finite-dimensional VectSp of finite-dimensional holds
( dim V = 1 iff ex v being Vector of st
( v <> 0. V & (Omega). V = Lin {v} ) )
let V be finite-dimensional VectSp of finite-dimensional ; ( dim V = 1 iff ex v being Vector of st
( v <> 0. V & (Omega). V = Lin {v} ) )
hereby ( ex v being Vector of st
( v <> 0. V & (Omega). V = Lin {v} ) implies dim V = 1 )
consider I being
finite Subset of
such that A1:
I is
Basis of
V
by MATRLIN:def 3;
assume
dim V = 1
;
ex v being Vector of st
( v <> 0. V & (Omega). V = Lin {v} )then
card I = 1
by A1, Def2;
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} is
linearly-independent
by A1, A2, VECTSP_7:def 3;
then A3:
v <> 0. V
by VECTSP_7:5;
Lin {v} = VectSpStr(# the
carrier of
V,the
U5 of
V,the
U2 of
V,the
lmult of
V #)
by A1, A2, VECTSP_7:def 3;
hence
ex
v being
Vector of st
(
v <> 0. V &
(Omega). V = Lin {v} )
by A3, VECTSP_4:def 4;
verum
end;
given v being Vector of such that A4:
( v <> 0. V & (Omega). V = Lin {v} )
; dim V = 1
( {v} is linearly-independent & Lin {v} = VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) )
by A4, VECTSP_4:def 4, VECTSP_7:5;
then A5:
{v} is Basis of V
by VECTSP_7:def 3;
card {v} = 1
by CARD_1:50;
hence
dim V = 1
by A5, Def2; verum