let F be Field; :: thesis: for V being VectSp of F st card ([#] V) = 2 holds
dim V = 1
let V be VectSp of F; :: thesis: ( card ([#] V) = 2 implies dim V = 1 )
assume A1: card ([#] V) = 2 ; :: thesis: dim V = 1
then A2: [#] V is finite ;
reconsider C = [#] V as finite set by A1;
reconsider V = V as finite-dimensional VectSp of F by A2, Th4;
ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )
proof
consider x, y being object such that
A3: x <> y and
A4: [#] V = {x,y} by A1, CARD_2:60;
per cases ( x = 0. V or y = 0. V ) by A4, TARSKI:def 2;
suppose A5: x = 0. V ; :: thesis: ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )
then reconsider x = x as Element of V ;
reconsider y = y as Element of V by A4, TARSKI:def 2;
set L = Lin {y};
take y ; :: thesis: ( y <> 0. V & (Omega). V = Lin {y} )
for v being Element of V holds
( v in (Omega). V iff v in Lin {y} )
proof
let v be Element of V; :: thesis: ( v in (Omega). V iff v in Lin {y} )
( v in (Omega). V implies v in Lin {y} ) hence ( v in (Omega). V iff v in Lin {y} ) ; :: thesis: verum
end;
hence ( y <> 0. V & (Omega). V = Lin {y} ) by A3, A5, VECTSP_4:30; :: thesis: verum
end;
suppose A8: y = 0. V ; :: thesis: ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )
reconsider x = x as Element of V by A4, TARSKI:def 2;
reconsider y = y as Element of V by A8;
set L = Lin {x};
take x ; :: thesis: ( x <> 0. V & (Omega). V = Lin {x} )
for v being Element of V holds
( v in (Omega). V iff v in Lin {x} ) hence ( x <> 0. V & (Omega). V = Lin {x} ) by A3, A8, VECTSP_4:30; :: thesis: verum
end;
end;
end;
hence dim V = 1 by VECTSP_9:30; :: thesis: verum