let V be finite-dimensional RealUnitarySpace; ( 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 ( 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 Def1;
assume
dim V = 2
;
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
object such that A3:
u in I
by CARD_1:27, XBOOLE_0:def 1;
reconsider u =
u as
VECTOR of
V by A3;
then consider v being
object such that A4:
v in I
and A5:
not
v in {u}
;
reconsider v =
v as
VECTOR of
V by A4;
A6:
v <> u
by A5, TARSKI:def 1;
A7:
now I c= {u,v}assume
not
I c= {u,v}
;
contradictionthen consider w being
object such that A8:
w in I
and A9:
not
w in {u,v}
;
for
x being
object st
x in {u,v,w} holds
x in I
by A3, A4, A8, ENUMSET1:def 1;
then
{u,v,w} c= I
;
then A10:
card {u,v,w} <= card I
by NAT_1:43;
(
w <> u &
w <> v )
by A9, TARSKI:def 2;
then
3
<= 2
by A2, A6, A10, CARD_2:58;
hence
contradiction
;
verum end;
for
x being
object st
x in {u,v} holds
x in I
by A3, A4, TARSKI:def 2;
then
{u,v} c= I
;
then A11:
I = {u,v}
by A7;
then A12:
{u,v} is
linearly-independent
by A1, RUSUB_3:def 2;
Lin {u,v} =
UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V, the
scalar of
V #)
by A1, A11, RUSUB_3:def 2
.=
(Omega). V
by RUSUB_1:def 3
;
hence
ex
u,
v being
VECTOR of
V st
(
u <> v &
{u,v} is
linearly-independent &
(Omega). V = Lin {u,v} )
by A6, A12;
verum
end;
given u, v being VECTOR of V such that A13:
u <> v
and
A14:
{u,v} is linearly-independent
and
A15:
(Omega). V = Lin {u,v}
; dim V = 2
Lin {u,v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)
by A15, RUSUB_1:def 3;
then A16:
{u,v} is Basis of V
by A14, RUSUB_3:def 2;
card {u,v} = 2
by A13, CARD_2:57;
hence
dim V = 2
by A16, Def2; verum