:: The Steinitz Theorem and the Dimension of a Real Linear Space
:: by JingChao Chen
::
:: Received July 1, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users
begin
theorem
Th1
:
:: RLVECT_5:1
for
V
being
RealLinearSpace
for
KL1
,
KL2
being
Linear_Combination
of
V
for
X
being
Subset
of
V
st
X
is
linearly-independent
&
Carrier
KL1
c=
X
&
Carrier
KL2
c=
X
&
Sum
KL1
=
Sum
KL2
holds
KL1
=
KL2
proof
end;
theorem
Th2
:
:: RLVECT_5:2
for
V
being
RealLinearSpace
for
A
being
Subset
of
V
st
A
is
linearly-independent
holds
ex
I
being
Basis
of
V
st
A
c=
I
proof
end;
theorem
Th3
:
:: RLVECT_5:3
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
for
x
being
VECTOR
of
V
holds
(
x
in
Carrier
L
iff ex
v
being
VECTOR
of
V
st
(
x
=
v
&
L
.
v
<>
0
) )
proof
end;
Lm1
:
for
X
,
x
being
set
st
x
in
X
holds
(
X
\
{
x
}
)
\/
{
x
}
=
X
proof
end;
:: More On Linear Combinations
theorem
Th4
:
:: RLVECT_5:4
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
for
F
,
G
being
FinSequence
of the
carrier
of
V
for
P
being
Permutation
of
(
dom
F
)
st
G
=
F
*
P
holds
Sum
(
L
(#)
F
)
=
Sum
(
L
(#)
G
)
proof
end;
theorem
Th5
:
:: RLVECT_5:5
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
for
F
being
FinSequence
of the
carrier
of
V
st
Carrier
L
misses
rng
F
holds
Sum
(
L
(#)
F
)
=
0.
V
proof
end;
theorem
Th6
:
:: RLVECT_5:6
for
V
being
RealLinearSpace
for
F
being
FinSequence
of the
carrier
of
V
st
F
is
one-to-one
holds
for
L
being
Linear_Combination
of
V
st
Carrier
L
c=
rng
F
holds
Sum
(
L
(#)
F
)
=
Sum
L
proof
end;
theorem
Th7
:
:: RLVECT_5:7
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
for
F
being
FinSequence
of the
carrier
of
V
ex
K
being
Linear_Combination
of
V
st
(
Carrier
K
=
(
rng
F
)
/\
(
Carrier
L
)
&
L
(#)
F
=
K
(#)
F
)
proof
end;
theorem
Th8
:
:: RLVECT_5:8
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
for
A
being
Subset
of
V
for
F
being
FinSequence
of the
carrier
of
V
st
rng
F
c=
the
carrier
of
(
Lin
A
)
holds
ex
K
being
Linear_Combination
of
A
st
Sum
(
L
(#)
F
)
=
Sum
K
proof
end;
theorem
Th9
:
:: RLVECT_5:9
for
V
being
RealLinearSpace
for
L
being
Linear_Combination
of
V
for
A
being
Subset
of
V
st
Carrier
L
c=
the
carrier
of
(
Lin
A
)
holds
ex
K
being
Linear_Combination
of
A
st
Sum
L
=
Sum
K
proof
end;
theorem
Th10
:
:: RLVECT_5:10
for
V
being
RealLinearSpace
for
W
being
Subspace
of
V
for
L
being
Linear_Combination
of
V
st
Carrier
L
c=
the
carrier
of
W
holds
for
K
being
Linear_Combination
of
W
st
K
=
L
|
the
carrier
of
W
holds
(
Carrier
L
=
Carrier
K
&
Sum
L
=
Sum
K
)
proof
end;
theorem
Th11
:
:: RLVECT_5:11
for
V
being
RealLinearSpace
for
W
being
Subspace
of
V
for
K
being
Linear_Combination
of
W
ex
L
being
Linear_Combination
of
V
st
(
Carrier
K
=
Carrier
L
&
Sum
K
=
Sum
L
)
proof
end;
theorem
Th12
:
:: RLVECT_5:12
for
V
being
RealLinearSpace
for
W
being
Subspace
of
V
for
L
being
Linear_Combination
of
V
st
Carrier
L
c=
the
carrier
of
W
holds
ex
K
being
Linear_Combination
of
W
st
(
Carrier
K
=
Carrier
L
&
Sum
K
=
Sum
L
)
proof
end;
:: More On Linear Independence & Basis
theorem
Th13
:
:: RLVECT_5:13
for
V
being
RealLinearSpace
for
I
being
Basis
of
V
for
v
being
VECTOR
of
V
holds
v
in
Lin
I
proof
end;
theorem
Th14
:
:: RLVECT_5:14
for
V
being
RealLinearSpace
for
W
being
Subspace
of
V
for
A
being
Subset
of
W
st
A
is
linearly-independent
holds
A
is
linearly-independent
Subset
of
V
proof
end;
theorem
Th15
:
:: RLVECT_5:15
for
V
being
RealLinearSpace
for
W
being
Subspace
of
V
for
A
being
Subset
of
V
st
A
is
linearly-independent
&
A
c=
the
carrier
of
W
holds
A
is
linearly-independent
Subset
of
W
proof
end;
theorem
Th16
:
:: RLVECT_5:16
for
V
being
RealLinearSpace
for
W
being
Subspace
of
V
for
A
being
Basis
of
W
ex
B
being
Basis
of
V
st
A
c=
B
proof
end;
theorem
Th17
:
:: RLVECT_5:17
for
V
being
RealLinearSpace
for
A
being
Subset
of
V
st
A
is
linearly-independent
holds
for
v
being
VECTOR
of
V
st
v
in
A
holds
for
B
being
Subset
of
V
st
B
=
A
\
{
v
}
holds
not
v
in
Lin
B
proof
end;
theorem
Th18
:
:: RLVECT_5:18
for
V
being
RealLinearSpace
for
I
being
Basis
of
V
for
A
being non
empty
Subset
of
V
st
A
misses
I
holds
for
B
being
Subset
of
V
st
B
=
I
\/
A
holds
B
is
linearly-dependent
proof
end;
theorem
Th19
:
:: RLVECT_5:19
for
V
being
RealLinearSpace
for
W
being
Subspace
of
V
for
A
being
Subset
of
V
st
A
c=
the
carrier
of
W
holds
Lin
A
is
Subspace
of
W
proof
end;
theorem
Th20
:
:: RLVECT_5:20
for
V
being
RealLinearSpace
for
W
being
Subspace
of
V
for
A
being
Subset
of
V
for
B
being
Subset
of
W
st
A
=
B
holds
Lin
A
=
Lin
B
proof
end;
begin
:: Exchange Lemma
theorem
Th21
:
:: RLVECT_5:21
for
V
being
RealLinearSpace
for
A
,
B
being
finite
Subset
of
V
for
v
being
VECTOR
of
V
st
v
in
Lin
(
A
\/
B
)
& not
v
in
Lin
B
holds
ex
w
being
VECTOR
of
V
st
(
w
in
A
&
w
in
Lin
(
(
(
A
\/
B
)
\
{
w
}
)
\/
{
v
}
)
)
proof
end;
:: Steinitz Theorem
theorem
Th22
:
:: RLVECT_5:22
for
V
being
RealLinearSpace
for
A
,
B
being
finite
Subset
of
V
st
RLSStruct
(# the
carrier
of
V
, the
ZeroF
of
V
, the
U5
of
V
, the
Mult
of
V
#)
=
Lin
A
&
B
is
linearly-independent
holds
(
card
B
<=
card
A
& ex
C
being
finite
Subset
of
V
st
(
C
c=
A
&
card
C
=
(
card
A
)
-
(
card
B
)
&
RLSStruct
(# the
carrier
of
V
, the
ZeroF
of
V
, the
U5
of
V
, the
Mult
of
V
#)
=
Lin
(
B
\/
C
)
) )
proof
end;
begin
definition
let
V
be
RealLinearSpace
;
attr
V
is
finite-dimensional
means
:
Def1
:
:: RLVECT_5:def 1
ex
A
being
finite
Subset
of
V
st
A
is
Basis
of
V
;
end;
::
deftheorem
Def1
defines
finite-dimensional
RLVECT_5:def 1 :
for
V
being
RealLinearSpace
holds
(
V
is
finite-dimensional
iff ex
A
being
finite
Subset
of
V
st
A
is
Basis
of
V
);
registration
cluster
non
empty
V83
()
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
finite-dimensional
for
RLSStruct
;
existence
ex
b
1
being
RealLinearSpace
st
(
b
1
is
strict
&
b
1
is
finite-dimensional
)
proof
end;
end;
theorem
Th23
:
:: RLVECT_5:23
for
V
being
RealLinearSpace
st
V
is
finite-dimensional
holds
for
I
being
Basis
of
V
holds
I
is
finite
proof
end;
theorem
:: RLVECT_5:24
for
V
being
RealLinearSpace
st
V
is
finite-dimensional
holds
for
A
being
Subset
of
V
st
A
is
linearly-independent
holds
A
is
finite
proof
end;
theorem
Th25
:
:: RLVECT_5:25
for
V
being
RealLinearSpace
st
V
is
finite-dimensional
holds
for
A
,
B
being
Basis
of
V
holds
card
A
=
card
B
proof
end;
theorem
Th26
:
:: RLVECT_5:26
for
V
being
RealLinearSpace
holds
(0).
V
is
finite-dimensional
proof
end;
theorem
Th27
:
:: RLVECT_5:27
for
V
being
RealLinearSpace
for
W
being
Subspace
of
V
st
V
is
finite-dimensional
holds
W
is
finite-dimensional
proof
end;
registration
let
V
be
RealLinearSpace
;
cluster
non
empty
V83
()
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
finite-dimensional
for
Subspace
of
V
;
existence
ex
b
1
being
Subspace
of
V
st
(
b
1
is
finite-dimensional
&
b
1
is
strict
)
proof
end;
end;
registration
let
V
be
finite-dimensional
RealLinearSpace
;
cluster
->
finite-dimensional
for
Subspace
of
V
;
correctness
coherence
for
b
1
being
Subspace
of
V
holds
b
1
is
finite-dimensional
;
by
Th27
;
end;
registration
let
V
be
finite-dimensional
RealLinearSpace
;
cluster
non
empty
V83
()
strict
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
finite-dimensional
for
Subspace
of
V
;
existence
ex
b
1
being
Subspace
of
V
st
b
1
is
strict
proof
end;
end;
begin
definition
let
V
be
RealLinearSpace
;
assume
A1
:
V
is
finite-dimensional
;
func
dim
V
->
Element
of
NAT
means
:
Def2
:
:: RLVECT_5:def 2
for
I
being
Basis
of
V
holds
it
=
card
I
;
existence
ex
b
1
being
Element
of
NAT
st
for
I
being
Basis
of
V
holds
b
1
=
card
I
proof
end;
uniqueness
for
b
1
,
b
2
being
Element
of
NAT
st ( for
I
being
Basis
of
V
holds
b
1
=
card
I
) & ( for
I
being
Basis
of
V
holds
b
2
=
card
I
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def2
defines
dim
RLVECT_5:def 2 :
for
V
being
RealLinearSpace
st
V
is
finite-dimensional
holds
for
b
2
being
Element
of
NAT
holds
(
b
2
=
dim
V
iff for
I
being
Basis
of
V
holds
b
2
=
card
I
);
theorem
Th28
:
:: RLVECT_5:28
for
V
being
finite-dimensional
RealLinearSpace
for
W
being
Subspace
of
V
holds
dim
W
<=
dim
V
proof
end;
theorem
Th29
:
:: RLVECT_5:29
for
V
being
finite-dimensional
RealLinearSpace
for
A
being
Subset
of
V
st
A
is
linearly-independent
holds
card
A
=
dim
(
Lin
A
)
proof
end;
theorem
Th30
:
:: RLVECT_5:30
for
V
being
finite-dimensional
RealLinearSpace
holds
dim
V
=
dim
(
(Omega).
V
)
proof
end;
theorem
:: RLVECT_5:31
for
V
being
finite-dimensional
RealLinearSpace
for
W
being
Subspace
of
V
holds
(
dim
V
=
dim
W
iff
(Omega).
V
=
(Omega).
W
)
proof
end;
theorem
Th32
:
:: RLVECT_5:32
for
V
being
finite-dimensional
RealLinearSpace
holds
(
dim
V
=
0
iff
(Omega).
V
=
(0).
V
)
proof
end;
theorem
:: RLVECT_5:33
for
V
being
finite-dimensional
RealLinearSpace
holds
(
dim
V
=
1 iff ex
v
being
VECTOR
of
V
st
(
v
<>
0.
V
&
(Omega).
V
=
Lin
{
v
}
) )
proof
end;
theorem
:: RLVECT_5:34
for
V
being
finite-dimensional
RealLinearSpace
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
}
) )
proof
end;
theorem
Th35
:
:: RLVECT_5:35
for
V
being
finite-dimensional
RealLinearSpace
for
W1
,
W2
being
Subspace
of
V
holds
(
dim
(
W1
+
W2
)
)
+
(
dim
(
W1
/\
W2
)
)
=
(
dim
W1
)
+
(
dim
W2
)
proof
end;
theorem
:: RLVECT_5:36
for
V
being
finite-dimensional
RealLinearSpace
for
W1
,
W2
being
Subspace
of
V
holds
dim
(
W1
/\
W2
)
>=
(
(
dim
W1
)
+
(
dim
W2
)
)
-
(
dim
V
)
proof
end;
theorem
:: RLVECT_5:37
for
V
being
finite-dimensional
RealLinearSpace
for
W1
,
W2
being
Subspace
of
V
st
V
is_the_direct_sum_of
W1
,
W2
holds
dim
V
=
(
dim
W1
)
+
(
dim
W2
)
proof
end;
Lm2
:
for
n
being
Element
of
NAT
for
V
being
finite-dimensional
RealLinearSpace
st
n
<=
dim
V
holds
ex
W
being
strict
Subspace
of
V
st
dim
W
=
n
proof
end;
theorem
:: RLVECT_5:38
for
n
being
Element
of
NAT
for
V
being
finite-dimensional
RealLinearSpace
holds
(
n
<=
dim
V
iff ex
W
being
strict
Subspace
of
V
st
dim
W
=
n
)
by
Lm2
,
Th28
;
definition
let
V
be
finite-dimensional
RealLinearSpace
;
let
n
be
Element
of
NAT
;
func
n
Subspaces_of
V
->
set
means
:
Def3
:
:: RLVECT_5:def 3
for
x
being
set
holds
(
x
in
it
iff ex
W
being
strict
Subspace
of
V
st
(
W
=
x
&
dim
W
=
n
) );
existence
ex
b
1
being
set
st
for
x
being
set
holds
(
x
in
b
1
iff ex
W
being
strict
Subspace
of
V
st
(
W
=
x
&
dim
W
=
n
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
set
st ( for
x
being
set
holds
(
x
in
b
1
iff ex
W
being
strict
Subspace
of
V
st
(
W
=
x
&
dim
W
=
n
) ) ) & ( for
x
being
set
holds
(
x
in
b
2
iff ex
W
being
strict
Subspace
of
V
st
(
W
=
x
&
dim
W
=
n
) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def3
defines
Subspaces_of
RLVECT_5:def 3 :
for
V
being
finite-dimensional
RealLinearSpace
for
n
being
Element
of
NAT
for
b
3
being
set
holds
(
b
3
=
n
Subspaces_of
V
iff for
x
being
set
holds
(
x
in
b
3
iff ex
W
being
strict
Subspace
of
V
st
(
W
=
x
&
dim
W
=
n
) ) );
theorem
:: RLVECT_5:39
for
n
being
Element
of
NAT
for
V
being
finite-dimensional
RealLinearSpace
st
n
<=
dim
V
holds
not
n
Subspaces_of
V
is
empty
proof
end;
theorem
:: RLVECT_5:40
for
n
being
Element
of
NAT
for
V
being
finite-dimensional
RealLinearSpace
st
dim
V
<
n
holds
n
Subspaces_of
V
=
{}
proof
end;
theorem
:: RLVECT_5:41
for
n
being
Element
of
NAT
for
V
being
finite-dimensional
RealLinearSpace
for
W
being
Subspace
of
V
holds
n
Subspaces_of
W
c=
n
Subspaces_of
V
proof
end;