The abstract of the Mizar article:

Basis of Real Linear Space

by

Wojciech A. Trybulec

Received July 10, 1990

MML identifier: RLVECT_3

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2, FINSEQ_1, FUNCT_1, ORDERS_1,
      SEQ_1, RELAT_1, FINSEQ_4, BOOLE, FUNCT_2, ARYTM_1, TARSKI, CARD_1,
      ZFMISC_1, RLVECT_3, HAHNBAN;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, FINSEQ_1, RELAT_1,
      ORDINAL1, FUNCT_1, FUNCT_2, STRUCT_0, RLVECT_1, FINSEQ_4, FRAENKEL,
      FINSET_1, REAL_1, RLSUB_1, ORDERS_1, RLSUB_2, RLVECT_2, CARD_1, NAT_1;
 constructors NAT_1, REAL_1, ORDERS_1, RLSUB_2, RLVECT_2, FINSEQ_4, MEMBERED,
      PARTFUN1, XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2, RELSET_1,
      STRUCT_0, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve x,y,X,Y,Z for set;
reserve a,b for Real;
reserve k,n for Nat;
reserve V for RealLinearSpace;
reserve W1,W2,W3 for Subspace of V;
reserve v,v1,v2,u for VECTOR of V;
reserve A,B,C for Subset of V;
reserve T for finite Subset of V;
reserve L,L1,L2 for Linear_Combination of V;
reserve l for Linear_Combination of A;
reserve F,G,H for FinSequence of the carrier of V;
reserve f,g for Function of the carrier of V, REAL;
reserve p,q,r for FinSequence;
reserve M for non empty set;
reserve CF for Choice_Function of M;

theorem :: RLVECT_3:1
 Sum(L1 + L2) = Sum(L1) + Sum(L2);

theorem :: RLVECT_3:2
 Sum(a * L) = a * Sum(L);

theorem :: RLVECT_3:3
 Sum(- L) = - Sum(L);

theorem :: RLVECT_3:4
 Sum(L1 - L2) = Sum(L1) - Sum(L2);

definition let V; let A;
 attr A is linearly-independent means
:: RLVECT_3:def 1
   for l st Sum(l) = 0.V holds Carrier(l) = {};
 antonym A is linearly-dependent;
end;

canceled;

theorem :: RLVECT_3:6
   A c= B & B is linearly-independent implies A is linearly-independent;

theorem :: RLVECT_3:7
 A is linearly-independent implies not 0.V in A;

theorem :: RLVECT_3:8
 {}(the carrier of V) is linearly-independent;

theorem :: RLVECT_3:9
 {v} is linearly-independent iff v <> 0.V;

theorem :: RLVECT_3:10
   {0.V} is linearly-dependent;

theorem :: RLVECT_3:11
 {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V;

theorem :: RLVECT_3:12
   {v,0.V} is linearly-dependent & {0.V,v} is linearly-dependent;

theorem :: RLVECT_3:13
 v1 <> v2 & {v1,v2} is linearly-independent iff
  v2 <> 0.V & for a holds v1 <> a * v2;

theorem :: RLVECT_3:14
   v1 <> v2 & {v1,v2} is linearly-independent iff
  for a,b st a * v1 + b * v2 = 0.V holds a = 0 & b = 0;

definition let V; let A;
 func Lin(A) -> strict Subspace of V means
:: RLVECT_3:def 2
   the carrier of it = {Sum(l) : not contradiction};
end;

canceled 2;

theorem :: RLVECT_3:17
 x in Lin(A) iff ex l st x = Sum(l);

theorem :: RLVECT_3:18
 x in A implies x in Lin(A);

reserve l0 for Linear_Combination of {}(the carrier of V);

theorem :: RLVECT_3:19
   Lin({}(the carrier of V)) = (0).V;

theorem :: RLVECT_3:20
   Lin(A) = (0).V implies A = {} or A = {0.V};

theorem :: RLVECT_3:21
 for W being strict Subspace of V holds
 A = the carrier of W implies Lin(A) = W;

theorem :: RLVECT_3:22
   for V being strict RealLinearSpace,A being Subset of V holds
  A = the carrier of V implies Lin(A) = V;

theorem :: RLVECT_3:23
 A c= B implies Lin(A) is Subspace of Lin(B);

theorem :: RLVECT_3:24
  for V being strict RealLinearSpace,A,B being Subset of V holds
 Lin(A) = V & A c= B implies Lin(B) = V;

theorem :: RLVECT_3:25
   Lin(A \/ B) = Lin(A) + Lin(B);

theorem :: RLVECT_3:26
   Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B);

theorem :: RLVECT_3:27
 A is linearly-independent implies
  ex B st A c= B & B is linearly-independent & Lin(B) = the RLSStruct of V;

theorem :: RLVECT_3:28
 Lin(A) = V implies
  ex B st B c= A & B is linearly-independent & Lin(B) = V;

definition let V be RealLinearSpace;
 mode Basis of V -> Subset of V means
:: RLVECT_3:def 3
   it is linearly-independent & Lin(it) = the RLSStruct of V;
end;

reserve I for Basis of V;

canceled 3;

theorem :: RLVECT_3:32
  for V being strict RealLinearSpace,A being Subset of V holds
 A is linearly-independent implies ex I being Basis of V st A c= I;

theorem :: RLVECT_3:33
   Lin(A) = V implies ex I st I c= A;

::
::  Auxiliary theorems.
::

theorem :: RLVECT_3:34
   Z <> {} & Z is finite &
  (for X,Y st X in Z & Y in Z holds X c= Y or Y c= X) implies union Z in Z;

theorem :: RLVECT_3:35
   not {} in M implies dom CF = M & rng CF c= union M;

theorem :: RLVECT_3:36
   x in (0).V iff x = 0.V;

theorem :: RLVECT_3:37
   W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3;

theorem :: RLVECT_3:38
   W1 is Subspace of W2 & W1 is Subspace of W3 implies
  W1 is Subspace of W2 /\ W3;

theorem :: RLVECT_3:39
   W1 is Subspace of W3 & W2 is Subspace of W3 implies
  W1 + W2 is Subspace of W3;

theorem :: RLVECT_3:40
   W1 is Subspace of W2 implies W1 is Subspace of W2 + W3;

theorem :: RLVECT_3:41
   f (#) (F ^ G) = (f (#) F) ^ (f (#) G);