:: Steinitz Theorem and Dimension of a Vector Space
:: by Mariusz \.Zynel
::
:: Received October 6, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users
begin
::
:: Preliminaries
::
registration
let
S
be non
empty
1-sorted
;
cluster
non
empty
for
Element
of
K27
( the
carrier
of
S
);
existence
not for
b
1
being
Subset
of
S
holds
b
1
is
empty
proof
end;
end;
Lm1
:
for
X
,
x
being
set
st
x
in
X
holds
(
X
\
{
x
}
)
\/
{
x
}
=
X
proof
end;
:: More On Linear Combinations
theorem
Th1
:
:: VECTSP_9:1
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th2
:
:: VECTSP_9:2
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th3
:
:: VECTSP_9:3
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th4
:
:: VECTSP_9:4
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th5
:
:: VECTSP_9:5
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th6
:
:: VECTSP_9:6
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th7
:
:: VECTSP_9:7
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th8
:
:: VECTSP_9:8
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th9
:
:: VECTSP_9:9
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th10
:
:: VECTSP_9:10
for
GF
being
Field
for
V
being
VectSp
of
GF
for
I
being
Basis
of
V
for
v
being
Vector
of
V
holds
v
in
Lin
I
proof
end;
registration
let
GF
be
Field
;
let
V
be
VectSp
of
GF
;
cluster
linearly-independent
for
Element
of
K27
( the
carrier
of
V
);
existence
ex
b
1
being
Subset
of
V
st
b
1
is
linearly-independent
proof
end;
end;
theorem
Th11
:
:: VECTSP_9:11
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th12
:
:: VECTSP_9:12
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th13
:
:: VECTSP_9:13
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th14
:
:: VECTSP_9:14
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th15
:
:: VECTSP_9:15
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th16
:
:: VECTSP_9:16
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th17
:
:: VECTSP_9:17
for
GF
being
Field
for
V
being
VectSp
of
GF
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
::
:: Steinitz Theorem
::
:: Exchange Lemma
theorem
Th18
:
:: VECTSP_9:18
for
GF
being
Field
for
V
being
VectSp
of
GF
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
Th19
:
:: VECTSP_9:19
for
GF
being
Field
for
V
being
VectSp
of
GF
for
A
,
B
being
finite
Subset
of
V
st
VectSpStr
(# the
carrier
of
V
, the
U5
of
V
, the
ZeroF
of
V
, the
lmult
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
)
&
VectSpStr
(# the
carrier
of
V
, the
U5
of
V
, the
ZeroF
of
V
, the
lmult
of
V
#)
=
Lin
(
B
\/
C
)
) )
proof
end;
begin
::
:: Finite-Dimensional Vector Spaces
::
theorem
Th20
:
:: VECTSP_9:20
for
GF
being
Field
for
V
being
VectSp
of
GF
st
V
is
finite-dimensional
holds
for
I
being
Basis
of
V
holds
I
is
finite
proof
end;
theorem
:: VECTSP_9:21
for
GF
being
Field
for
V
being
VectSp
of
GF
st
V
is
finite-dimensional
holds
for
A
being
Subset
of
V
st
A
is
linearly-independent
holds
A
is
finite
proof
end;
theorem
Th22
:
:: VECTSP_9:22
for
GF
being
Field
for
V
being
VectSp
of
GF
st
V
is
finite-dimensional
holds
for
A
,
B
being
Basis
of
V
holds
card
A
=
card
B
proof
end;
theorem
Th23
:
:: VECTSP_9:23
for
GF
being
Field
for
V
being
VectSp
of
GF
holds
(0).
V
is
finite-dimensional
proof
end;
theorem
Th24
:
:: VECTSP_9:24
for
GF
being
Field
for
V
being
VectSp
of
GF
for
W
being
Subspace
of
V
st
V
is
finite-dimensional
holds
W
is
finite-dimensional
proof
end;
registration
let
GF
be
Field
;
let
V
be
VectSp
of
GF
;
cluster
non
empty
V72
()
strict
V109
(
GF
)
V110
(
GF
)
V111
(
GF
)
V112
(
GF
)
V116
()
V117
()
V118
()
finite-dimensional
for
Subspace
of
V
;
existence
ex
b
1
being
Subspace
of
V
st
(
b
1
is
strict
&
b
1
is
finite-dimensional
)
proof
end;
end;
registration
let
GF
be
Field
;
let
V
be
finite-dimensional
VectSp
of
GF
;
cluster
->
finite-dimensional
for
Subspace
of
V
;
correctness
coherence
for
b
1
being
Subspace
of
V
holds
b
1
is
finite-dimensional
;
by
Th24
;
end;
registration
let
GF
be
Field
;
let
V
be
finite-dimensional
VectSp
of
GF
;
cluster
non
empty
V72
()
strict
V109
(
GF
)
V110
(
GF
)
V111
(
GF
)
V112
(
GF
)
V116
()
V117
()
V118
()
finite-dimensional
for
Subspace
of
V
;
existence
ex
b
1
being
Subspace
of
V
st
b
1
is
strict
proof
end;
end;
begin
::
:: Dimension of a Vector Space
::
definition
let
GF
be
Field
;
let
V
be
VectSp
of
GF
;
assume
A1
:
V
is
finite-dimensional
;
func
dim
V
->
Nat
means
:
Def1
:
:: VECTSP_9:def 1
for
I
being
Basis
of
V
holds
it
=
card
I
;
existence
ex
b
1
being
Nat
st
for
I
being
Basis
of
V
holds
b
1
=
card
I
proof
end;
uniqueness
for
b
1
,
b
2
being
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
Def1
defines
dim
VECTSP_9:def 1 :
for
GF
being
Field
for
V
being
VectSp
of
GF
st
V
is
finite-dimensional
holds
for
b
3
being
Nat
holds
(
b
3
=
dim
V
iff for
I
being
Basis
of
V
holds
b
3
=
card
I
);
theorem
Th25
:
:: VECTSP_9:25
for
GF
being
Field
for
V
being
finite-dimensional
VectSp
of
GF
for
W
being
Subspace
of
V
holds
dim
W
<=
dim
V
proof
end;
theorem
Th26
:
:: VECTSP_9:26
for
GF
being
Field
for
V
being
finite-dimensional
VectSp
of
GF
for
A
being
Subset
of
V
st
A
is
linearly-independent
holds
card
A
=
dim
(
Lin
A
)
proof
end;
theorem
Th27
:
:: VECTSP_9:27
for
GF
being
Field
for
V
being
finite-dimensional
VectSp
of
GF
holds
dim
V
=
dim
(
(Omega).
V
)
proof
end;
theorem
:: VECTSP_9:28
for
GF
being
Field
for
V
being
finite-dimensional
VectSp
of
GF
for
W
being
Subspace
of
V
holds
(
dim
V
=
dim
W
iff
(Omega).
V
=
(Omega).
W
)
proof
end;
theorem
Th29
:
:: VECTSP_9:29
for
GF
being
Field
for
V
being
finite-dimensional
VectSp
of
GF
holds
(
dim
V
=
0
iff
(Omega).
V
=
(0).
V
)
proof
end;
theorem
:: VECTSP_9:30
for
GF
being
Field
for
V
being
finite-dimensional
VectSp
of
GF
holds
(
dim
V
=
1 iff ex
v
being
Vector
of
V
st
(
v
<>
0.
V
&
(Omega).
V
=
Lin
{
v
}
) )
proof
end;
theorem
:: VECTSP_9:31
for
GF
being
Field
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
}
) )
proof
end;
theorem
Th32
:
:: VECTSP_9:32
for
GF
being
Field
for
V
being
finite-dimensional
VectSp
of
GF
for
W1
,
W2
being
Subspace
of
V
holds
(
dim
(
W1
+
W2
)
)
+
(
dim
(
W1
/\
W2
)
)
=
(
dim
W1
)
+
(
dim
W2
)
proof
end;
theorem
:: VECTSP_9:33
for
GF
being
Field
for
V
being
finite-dimensional
VectSp
of
GF
for
W1
,
W2
being
Subspace
of
V
holds
dim
(
W1
/\
W2
)
>=
(
(
dim
W1
)
+
(
dim
W2
)
)
-
(
dim
V
)
proof
end;
theorem
:: VECTSP_9:34
for
GF
being
Field
for
V
being
finite-dimensional
VectSp
of
GF
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
GF
being
Field
for
n
being
Nat
for
V
being
finite-dimensional
VectSp
of
GF
st
n
<=
dim
V
holds
ex
W
being
strict
Subspace
of
V
st
dim
W
=
n
proof
end;
theorem
:: VECTSP_9:35
for
GF
being
Field
for
n
being
Nat
for
V
being
finite-dimensional
VectSp
of
GF
holds
(
n
<=
dim
V
iff ex
W
being
strict
Subspace
of
V
st
dim
W
=
n
)
by
Lm2
,
Th25
;
definition
let
GF
be
Field
;
let
V
be
finite-dimensional
VectSp
of
GF
;
let
n
be
Nat
;
func
n
Subspaces_of
V
->
set
means
:
Def2
:
:: VECTSP_9:def 2
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
Def2
defines
Subspaces_of
VECTSP_9:def 2 :
for
GF
being
Field
for
V
being
finite-dimensional
VectSp
of
GF
for
n
being
Nat
for
b
4
being
set
holds
(
b
4
=
n
Subspaces_of
V
iff for
x
being
set
holds
(
x
in
b
4
iff ex
W
being
strict
Subspace
of
V
st
(
W
=
x
&
dim
W
=
n
) ) );
theorem
:: VECTSP_9:36
for
GF
being
Field
for
n
being
Nat
for
V
being
finite-dimensional
VectSp
of
GF
st
n
<=
dim
V
holds
not
n
Subspaces_of
V
is
empty
proof
end;
theorem
:: VECTSP_9:37
for
GF
being
Field
for
n
being
Nat
for
V
being
finite-dimensional
VectSp
of
GF
st
dim
V
<
n
holds
n
Subspaces_of
V
=
{}
proof
end;
theorem
:: VECTSP_9:38
for
GF
being
Field
for
n
being
Nat
for
V
being
finite-dimensional
VectSp
of
GF
for
W
being
Subspace
of
V
holds
n
Subspaces_of
W
c=
n
Subspaces_of
V
proof
end;
:: Preliminaries
::