let V be finite-dimensional RealUnitarySpace; :: thesis: for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
let W be Subspace of V; :: thesis: ( dim V = dim W iff (Omega). V = (Omega). W )
hereby :: thesis: ( (Omega). V = (Omega). W implies dim V = dim W )
assume A1:
dim V = dim W
;
:: thesis: (Omega). V = (Omega). Wconsider A being
Basis of
W;
consider B being
Basis of
V such that A2:
A c= B
by RUSUB_3:24;
A3:
card A =
dim V
by A1, Def3
.=
card B
by Def3
;
(
A c= the
carrier of
W & the
carrier of
W c= the
carrier of
V )
by RUSUB_1:def 1;
then reconsider A' =
A as
finite Subset of
V by Th3, XBOOLE_1:1;
reconsider B' =
B as
finite Subset of
V by Th3;
reconsider A =
A as
Subset of
W ;
reconsider B =
B as
Subset of
V ;
(Omega). V =
UNITSTR(# the
carrier of
V,the
U2 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
U2 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
;
:: thesis: verum
end;
assume
(Omega). V = (Omega). W
; :: thesis: dim V = dim W
then A5: UNITSTR(# the carrier of V,the U2 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 U2 of W,the addF of W,the Mult of W,the scalar of W #)
by RUSUB_1:def 3
;
consider A being finite Subset of V such that
A6:
A is Basis of V
by Def1;
consider B being finite Subset of W such that
A7:
B is Basis of W
by Def1;
A8:
A is linearly-independent
by A6, RUSUB_3:def 2;
A9:
B is linearly-independent
by A7, RUSUB_3:def 2;
A10: Lin A =
UNITSTR(# the carrier of W,the U2 of W,the addF of W,the Mult of W,the scalar of W #)
by A5, A6, RUSUB_3:def 2
.=
Lin B
by A7, RUSUB_3:def 2
;
reconsider A = A as Subset of V ;
reconsider B = B as Subset of W ;
dim V =
card A
by A6, Def3
.=
dim (Lin B)
by A8, A10, Th9
.=
card B
by A9, Th9
.=
dim W
by A7, Def3
;
hence
dim V = dim W
; :: thesis: verum