:: Steinitz Theorem and Dimension of a Vector Space
::  by Mariusz \.Zynel
::
:: Received October 6, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, VECTSP_1, RLSUB_1, NAT_1, XBOOLE_0, STRUCT_0, SUBSET_1,
      RLVECT_2, FINSEQ_1, FUNCT_2, RELAT_1, CARD_3, VALUED_1, FUNCT_1,
      PARTFUN1, SUPINF_2, ORDINAL4, TARSKI, ARYTM_3, ARYTM_1, CLASSES1,
      FINSET_1, RLVECT_3, CARD_1, XXREAL_0, FINSEQ_4, RLVECT_5, RLSUB_2;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
      XCMPLX_0, RELAT_1, DOMAIN_1, STRUCT_0, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1,
      FINSET_1, FINSEQ_1, FINSEQ_3, FINSEQ_4, CLASSES1, RLVECT_1, VECTSP_1,
      VECTSP_4, VECTSP_6, VECTSP_5, VECTSP_7, MATRLIN, XXREAL_0;
 constructors FINSEQ_4, XXREAL_0, NAT_1, REALSET1, RFINSEQ, VECTSP_5, VECTSP_6,
      VECTSP_7, CLASSES1, MATRLIN, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
      FINSET_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, VECTSP_1, VECTSP_7,
      MATRLIN, CARD_1, RELSET_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve GF for Field,
  V for VectSp of GF,
  W for Subspace of V,
  x, y, y1, y2 for set,
  i, n, m for Nat;

::
::   Preliminaries
::

registration
  let S be non empty 1-sorted;
  cluster non empty for Subset of S;
end;

:: More On Linear Combinations

theorem :: VECTSP_9:1
  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 :: VECTSP_9:2
  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 :: VECTSP_9:3
  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 :: VECTSP_9:4
  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 :: VECTSP_9:5
  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 :: VECTSP_9:6
  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 :: VECTSP_9:7
  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 :: VECTSP_9:8
  for K being Linear_Combination of W ex L being
  Linear_Combination of V st Carrier(K) = Carrier(L) & Sum(K) = Sum (L);

theorem :: VECTSP_9:9
  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 :: VECTSP_9:10
  for I being Basis of V, v being Vector of V holds v in Lin(I);

registration
  let GF, V;
  cluster linearly-independent for Subset of V;
end;

theorem :: VECTSP_9:11
  for A being Subset of W st A is linearly-independent holds A is
  linearly-independent Subset of V;

theorem :: VECTSP_9:12
  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;

theorem :: VECTSP_9:13
  for A being Basis of W ex B being Basis of V st A c= B;

theorem :: VECTSP_9:14
  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 :: VECTSP_9:15
  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 :: VECTSP_9:16
  for A being Subset of V st A c= the carrier of W holds Lin(A) is
  Subspace of W;

theorem :: VECTSP_9:17
  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 :: VECTSP_9:18
  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});

::$N Steinitz Theorem
theorem :: VECTSP_9:19
  for A, B being finite Subset of V st the ModuleStr 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 ModuleStr of V = Lin(B \/ C);

begin

::
::   Finite-Dimensional Vector Spaces
::

theorem :: VECTSP_9:20
  V is finite-dimensional implies for I being Basis of V holds I is finite;

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

theorem :: VECTSP_9:22
  V is finite-dimensional implies for A, B being Basis of V holds
  card A = card B;

theorem :: VECTSP_9:23
  (0).V is finite-dimensional;

theorem :: VECTSP_9:24
  V is finite-dimensional implies W is finite-dimensional;

registration
  let GF be Field, V be VectSp of GF;
  cluster strict finite-dimensional for Subspace of V;
end;

registration
  let GF be Field, V be finite-dimensional VectSp of GF;
  cluster -> finite-dimensional for Subspace of V;
end;

registration
  let GF be Field, V be finite-dimensional VectSp of GF;
  cluster strict for Subspace of V;
end;

begin

::
::   Dimension of a Vector Space
::

definition

  let GF be Field, V be VectSp of GF;
  assume
 V is finite-dimensional;
  func dim V -> Nat means
:: VECTSP_9:def 1

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

reserve V for finite-dimensional VectSp of GF,
  W, W1, W2 for Subspace of V,
  u, v for Vector of V;

theorem :: VECTSP_9:25
  dim W <= dim V;

theorem :: VECTSP_9:26
  for A being Subset of V st A is linearly-independent holds card
  A = dim Lin(A);

theorem :: VECTSP_9:27
  dim V = dim (Omega).V;

theorem :: VECTSP_9:28
  dim V = dim W iff (Omega).V = (Omega).W;

theorem :: VECTSP_9:29
  dim V = 0 iff (Omega).V = (0).V;

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

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

theorem :: VECTSP_9:32
  dim(W1 + W2) + dim(W1 /\ W2) = dim W1 + dim W2;

theorem :: VECTSP_9:33
  dim(W1 /\ W2) >= dim W1 + dim W2 - dim V;

theorem :: VECTSP_9:34
  V is_the_direct_sum_of W1, W2 implies dim V = dim W1 + dim W2;

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

definition
  let GF be Field, V be finite-dimensional VectSp of GF, n be Nat;
  func n Subspaces_of V -> set means
:: VECTSP_9:def 2

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

theorem :: VECTSP_9:36
  n <= dim V implies n Subspaces_of V is non empty;

theorem :: VECTSP_9:37
  dim V < n implies n Subspaces_of V = {};

theorem :: VECTSP_9:38
  n Subspaces_of W c= n Subspaces_of V;