let V be finite-dimensional RealUnitarySpace; for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
let W be Subspace of V; ( dim V = dim W iff (Omega). V = (Omega). W )
consider A being finite Subset of V such that
A1:
A is Basis of V
by Def1;
hereby ( (Omega). V = (Omega). W implies dim V = dim W )
set A = the
Basis of
W;
consider B being
Basis of
V such that A2:
the
Basis of
W c= B
by RUSUB_3:24;
the
carrier of
W c= the
carrier of
V
by RUSUB_1:def 1;
then reconsider A9 = the
Basis of
W as
finite Subset of
V by Th3, XBOOLE_1:1;
reconsider B9 =
B as
finite Subset of
V by Th3;
assume
dim V = dim W
;
(Omega). V = (Omega). Wthen A3:
card the
Basis of
W =
dim V
by Def2
.=
card B
by Def2
;
reconsider B =
B as
Subset of
V ;
reconsider A = the
Basis of
W as
Subset of
W ;
(Omega). V =
UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V, the
scalar of
V #)
by RUSUB_1:def 3
.=
Lin B
by RUSUB_3:def 2
.=
Lin A
by A4, RUSUB_3:28
.=
UNITSTR(# the
carrier of
W, the
ZeroF of
W, the
addF of
W, the
Mult of
W, the
scalar of
W #)
by RUSUB_3:def 2
.=
(Omega). W
by RUSUB_1:def 3
;
hence
(Omega). V = (Omega). W
;
verum
end;
consider B being finite Subset of W such that
A5:
B is Basis of W
by Def1;
A6:
A is linearly-independent
by A1, RUSUB_3:def 2;
assume
(Omega). V = (Omega). W
; dim V = dim W
then UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) =
(Omega). W
by RUSUB_1:def 3
.=
UNITSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the scalar of W #)
by RUSUB_1:def 3
;
then A7: Lin A =
UNITSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the scalar of W #)
by A1, RUSUB_3:def 2
.=
Lin B
by A5, RUSUB_3:def 2
;
A8:
B is linearly-independent
by A5, RUSUB_3:def 2;
reconsider B = B as Subset of W ;
reconsider A = A as Subset of V ;
dim V =
card A
by A1, Def2
.=
dim (Lin B)
by A6, A7, Th9
.=
card B
by A8, Th9
.=
dim W
by A5, Def2
;
hence
dim V = dim W
; verum