let GF be Field; :: thesis: for V being finite-dimensional VectSp of GF holds
( dim V = 2 iff ex u, v being Vector of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )
let V be finite-dimensional VectSp of GF; :: thesis: ( dim V = 2 iff ex u, v being Vector of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )
hereby :: thesis: ( ex u, v being Vector of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) implies dim V = 2 )
consider I being
finite Subset of
V such that A1:
I is
Basis of
V
by MATRLIN:def 3;
assume
dim V = 2
;
:: thesis: ex u, v being Vector of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} )then A2:
card I = 2
by A1, Def2;
then consider u being
set such that A3:
u in I
by CARD_1:47, XBOOLE_0:def 1;
reconsider u =
u as
Vector of
V by A3;
then consider v being
set such that A4:
(
v in I & not
v in {u} )
by TARSKI:def 3;
reconsider v =
v as
Vector of
V by A4;
A5:
v <> u
by A4, TARSKI:def 1;
for
x being
set st
x in {u,v} holds
x in I
by A3, A4, TARSKI:def 2;
then A6:
{u,v} c= I
by TARSKI:def 3;
now assume
not
I c= {u,v}
;
:: thesis: contradictionthen consider w being
set such that A7:
(
w in I & not
w in {u,v} )
by TARSKI:def 3;
A8:
(
w <> u &
w <> v )
by A7, TARSKI:def 2;
for
x being
set st
x in {u,v,w} holds
x in I
by A3, A4, A7, ENUMSET1:def 1;
then
{u,v,w} c= I
by TARSKI:def 3;
then
card {u,v,w} <= card I
by NAT_1:44;
then
3
<= 2
by A2, A5, A8, CARD_2:77;
hence
contradiction
;
:: thesis: verum end; then A9:
I = {u,v}
by A6, XBOOLE_0:def 10;
then A10:
Lin {u,v} =
VectSpStr(# the
carrier of
V,the
U5 of
V,the
U2 of
V,the
lmult of
V #)
by A1, VECTSP_7:def 3
.=
(Omega). V
by VECTSP_4:def 4
;
{u,v} is
linearly-independent
by A1, A9, VECTSP_7:def 3;
hence
ex
u,
v being
Vector of
V st
(
u <> v &
{u,v} is
linearly-independent &
(Omega). V = Lin {u,v} )
by A5, A10;
:: thesis: verum
end;
given u, v being Vector of V such that A11:
u <> v
and
A12:
{u,v} is linearly-independent
and
A13:
(Omega). V = Lin {u,v}
; :: thesis: dim V = 2
Lin {u,v} = VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #)
by A13, VECTSP_4:def 4;
then
( {u,v} is Basis of V & card {u,v} = 2 )
by A11, A12, CARD_2:76, VECTSP_7:def 3;
hence
dim V = 2
by Def2; :: thesis: verum