The abstract of the Mizar article:

The Steinitz Theorem and the Dimension of a Real Linear Space

by

Jing-Chao Chen

Received July 1, 1997

MML identifier: RLVECT_5

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, RLSUB_1, RLVECT_2, RLVECT_3, BOOLE, ARYTM_1, FUNCT_1,
      FINSET_1, CARD_1, FINSEQ_1, RELAT_1, FUNCT_2, SEQ_1, FINSEQ_4, SUBSET_1,
      RFINSEQ, RLSUB_2, MATRLIN, TARSKI, VECTSP_9;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XREAL_0, REAL_1,
      NAT_1, RELAT_1, FUNCT_1, FUNCT_2, CARD_1, FINSET_1, FINSEQ_1, FINSEQ_3,
      FINSEQ_4, STRUCT_0, RFINSEQ, RLVECT_1, RLVECT_2, RLSUB_1, RLSUB_2,
      RLVECT_3;
 constructors REAL_1, NAT_1, FINSEQ_3, RFINSEQ, RLVECT_3, RLSUB_2, RLVECT_2,
      FINSEQ_4, PARTFUN1, XREAL_0, MEMBERED;
 clusters SUBSET_1, STRUCT_0, RELSET_1, FINSEQ_1, FINSET_1, FUNCT_2, NAT_1,
      MEMBERED, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin  :: Preliminaries

reserve V for RealLinearSpace,
        W for Subspace of V,
        x, y, y1, y2 for set,
        i, n for Nat,
        v for VECTOR of V,
        KL1, KL2 for Linear_Combination of V,
        X for Subset of V;

theorem :: RLVECT_5:1
    X is linearly-independent &
    Carrier(KL1) c= X & Carrier(KL2) c= X &
    Sum(KL1) = Sum(KL2) implies KL1 = KL2;

theorem :: RLVECT_5:2
for V being RealLinearSpace, A being Subset of V st
  A is linearly-independent
  holds ex I being Basis of V st A c= I;

theorem :: RLVECT_5:3
  for L being Linear_Combination of V,
      x being VECTOR of V holds
  x in Carrier L iff ex v st x = v & L.v <> 0;

:: More On Linear Combinations

canceled;

theorem :: RLVECT_5:5
  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);

theorem :: RLVECT_5:6
  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;

theorem :: RLVECT_5:7
  for F being FinSequence of the carrier of V st F is one-to-one
  for L being Linear_Combination of V st Carrier(L) c= rng F
    holds
   Sum(L (#) F) = Sum(L);

theorem :: RLVECT_5:8
  for L being Linear_Combination of V
  for F being FinSequence of the carrier of V
    holds
   ex K being Linear_Combination of V st
    Carrier(K) = rng F /\ Carrier(L) & L (#) F = K (#) F;

theorem :: RLVECT_5:9
  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);

theorem :: RLVECT_5:10
  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);

theorem :: RLVECT_5:11
  for L being Linear_Combination of V st Carrier(L) c= the carrier of W
  for K being Linear_Combination of W st K = L|the carrier of W
     holds
   Carrier(L) = Carrier(K) & Sum(L) = Sum(K);

theorem :: RLVECT_5:12
  for K being Linear_Combination of W
    holds
   ex L being Linear_Combination of V st Carrier(K) = Carrier(L) &
   Sum(K) = Sum(L);

theorem :: RLVECT_5:13
  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);

:: More On Linear Independence & Basis

theorem :: RLVECT_5:14
  for I being Basis of V, v being VECTOR of V holds v in Lin(I);

theorem :: RLVECT_5:15
  for A being Subset of W st A is linearly-independent
    holds
   ex B being Subset of V st B is linearly-independent & B = A;

theorem :: RLVECT_5:16
  for A being Subset of V st
   A is linearly-independent & A c= the carrier of W
     holds
    ex B being Subset of W st B is linearly-independent & B = A;

theorem :: RLVECT_5:17
  for A being Basis of W ex B being Basis of V st A c= B;

theorem :: RLVECT_5:18
  for A being Subset of V st A is linearly-independent
  for v being VECTOR of V st v in A
  for B being Subset of V st B = A \ {v}
    holds
   not v in Lin(B);

theorem :: RLVECT_5:19
  for I being Basis of V
  for A being non empty Subset of V st A misses I
  for B being Subset of V st B = I \/ A
    holds
   B is linearly-dependent;

theorem :: RLVECT_5:20
  for A being Subset of V st A c= the carrier of W
    holds
   Lin(A) is Subspace of W;

theorem :: RLVECT_5:21
  for A being Subset of V, B being Subset of W st A = B
    holds
   Lin(A) = Lin(B);

begin  :: Steinitz Theorem

:: Exchange Lemma

theorem :: RLVECT_5:22
  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});

:: Steinitz Theorem

theorem :: RLVECT_5:23
  for A, B being finite Subset of V st
   the RLSStruct 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 & the RLSStruct of V = Lin(B \/ C);

begin  :: Finite-Dimensional Vector Spaces

definition
  let V be RealLinearSpace;
  attr V is finite-dimensional means
:: RLVECT_5:def 1

    ex A being finite Subset of V st A is Basis of V;
end;

definition
  cluster strict finite-dimensional RealLinearSpace;
end;

definition
  let V be RealLinearSpace;
  redefine attr V is finite-dimensional means
:: RLVECT_5:def 2

  ex I being finite Subset of V st I is Basis of V;
end;

theorem :: RLVECT_5:24
  V is finite-dimensional implies for I being Basis of V holds I is finite;

theorem :: RLVECT_5:25
    V is finite-dimensional
    implies
   for A being Subset of V st A is linearly-independent holds A is finite;

theorem :: RLVECT_5:26
  V is finite-dimensional implies
   for A, B being Basis of V holds Card A = Card B;

theorem :: RLVECT_5:27
  (0).V is finite-dimensional;

theorem :: RLVECT_5:28
  V is finite-dimensional implies W is finite-dimensional;

definition
  let V be RealLinearSpace;
  cluster finite-dimensional strict Subspace of V;
end;

definition
  let V be finite-dimensional RealLinearSpace;
  cluster -> finite-dimensional Subspace of V;
end;

definition
  let V be finite-dimensional RealLinearSpace;
  cluster strict Subspace of V;
end;

begin  :: Dimension of a Vector Space

definition
  let V be RealLinearSpace;
  assume  V is finite-dimensional;
  func dim V -> Nat means
:: RLVECT_5:def 3

  for I being Basis of V holds it = Card I;
end;

 reserve V for finite-dimensional RealLinearSpace,
         W, W1, W2 for Subspace of V,
         u, v for VECTOR of V;

theorem :: RLVECT_5:29
  dim W <= dim V;

theorem :: RLVECT_5:30
  for A being Subset of V st A is linearly-independent
    holds
   Card A = dim Lin(A);

theorem :: RLVECT_5:31
  dim V = dim (Omega).V;

theorem :: RLVECT_5:32
    dim V = dim W iff (Omega).V = (Omega).W;

theorem :: RLVECT_5:33
  dim V = 0 iff (Omega).V = (0).V;

theorem :: RLVECT_5:34
    dim V = 1 iff ex v st v <> 0.V & (Omega).V = Lin{v};

theorem :: RLVECT_5:35
    dim V = 2 iff ex u, v st u <> v & {u, v} is linearly-independent &
   (Omega).V = Lin{u, v};

theorem :: RLVECT_5:36
  dim(W1 + W2) + dim(W1 /\ W2) = dim W1 + dim W2;

theorem :: RLVECT_5:37
    dim(W1 /\ W2) >= dim W1 + dim W2 - dim V;

theorem :: RLVECT_5:38
    V is_the_direct_sum_of W1, W2 implies dim V = dim W1 + dim W2;

theorem :: RLVECT_5:39
   n <= dim V iff ex W being strict Subspace of V st dim W = n;

definition
  let V be finite-dimensional RealLinearSpace, n be Nat;
  func n Subspaces_of V -> set means
:: RLVECT_5:def 4

  x in it iff ex W being strict Subspace of V st W = x & dim W = n;
end;

theorem :: RLVECT_5:40
    n <= dim V implies n Subspaces_of V is non empty;

theorem :: RLVECT_5:41
    dim V < n implies n Subspaces_of V = {};

theorem :: RLVECT_5:42
    n Subspaces_of W c= n Subspaces_of V;