The abstract of the Mizar article:

Subspaces of Real Linear Space Generated by One, Two, or Three Vectors and Their Cosets

by

Wojciech A. Trybulec

Received February 24, 1993

MML identifier: RLVECT_4

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, RLSUB_1, FUNCT_1, RLVECT_2, FUNCT_2, ARYTM_1, BOOLE,
      FINSEQ_1, RELAT_1, SEQ_1, RLVECT_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, FINSEQ_1, FUNCT_1, FUNCT_2,
      REAL_1, STRUCT_0, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3, FRAENKEL;
 constructors REAL_1, RLVECT_2, RLVECT_3, FINSEQ_4, MEMBERED, XBOOLE_0;
 clusters STRUCT_0, RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve x for set;
reserve a,b,c,d,e,r1,r2,r3,r4,r5,r6 for Real;
reserve V for RealLinearSpace;
reserve u,v,v1,v2,v3,w,w1,w2,w3 for VECTOR of V;
reserve W,W1,W2 for Subspace of V;

scheme LambdaSep3{D, R() -> non empty set,
                  A1, A2, A3() -> Element of D(),
                  B1, B2, B3() -> Element of R(),
                  F(set) -> Element of R()}:
 ex f being Function of D(),R() st
  f.A1() = B1() & f.A2() = B2() & f.A3() = B3() &
   for C being Element of D() st C <> A1() & C <> A2() & C <> A3() holds
    f.C = F(C) provided
  A1() <> A2() and
  A1() <> A3() and
  A2() <> A3();

scheme LinCEx1{V() -> RealLinearSpace, v() -> VECTOR of V(), a() -> Real}:
 ex l being Linear_Combination of {v()} st l.v() = a();

scheme LinCEx2{V() -> RealLinearSpace, v1, v2() -> VECTOR of V(),
               a, b() -> Real}:
 ex l being Linear_Combination of {v1(),v2()} st l.v1() = a() & l.v2() = b()
  provided
  v1() <> v2();

scheme LinCEx3{V() -> RealLinearSpace, v1, v2, v3() -> VECTOR of V(),
               a, b, c() -> Real}:
 ex l being Linear_Combination of {v1(),v2(),v3()} st
  l.v1() = a() & l.v2() = b() & l.v3() = c() provided
  v1() <> v2() and
  v1() <> v3() and
  v2() <> v3();

theorem :: RLVECT_4:1
   v + w - v = w & w + v - v = w & v - v + w = w & w - v + v = w &
 v + (w - v) = w & w + (v - v) = w & v - (v - w) = w;

theorem :: RLVECT_4:2
 v + u - w = v - w + u;

:: RLVECT_1:37 extended

canceled;

theorem :: RLVECT_4:4
   v1 - w = v2 - w implies v1 = v2;

:: Composition of RLVECT_1:38 and RLVECT_1:39

canceled;

theorem :: RLVECT_4:6
 - (a * v) = (- a) * v;

theorem :: RLVECT_4:7
   W1 is Subspace of W2 implies v + W1 c= v + W2;

theorem :: RLVECT_4:8
   u in v + W implies v + W = u + W;

theorem :: RLVECT_4:9
 for l being Linear_Combination of {u,v,w} st
  u <> v & u <> w & v <> w holds Sum(l) = l.u * u + l.v * v + l.w * w;

theorem :: RLVECT_4:10
 u <> v & u <> w & v <> w & {u,v,w} is linearly-independent iff
  for a,b,c st a * u + b * v + c * w = 0.V holds a = 0 & b = 0 & c = 0;

theorem :: RLVECT_4:11
 x in Lin{v} iff ex a st x = a * v;

theorem :: RLVECT_4:12
   v in Lin{v};

theorem :: RLVECT_4:13
   x in v + Lin{w} iff ex a st x = v + a * w;

theorem :: RLVECT_4:14
 x in Lin{w1,w2} iff ex a,b st x = a * w1 + b * w2;

theorem :: RLVECT_4:15
   w1 in Lin{w1,w2} & w2 in Lin{w1,w2};

theorem :: RLVECT_4:16
   x in v + Lin{w1,w2} iff ex a,b st x = v + a * w1 + b * w2;

theorem :: RLVECT_4:17
 x in Lin{v1,v2,v3} iff ex a,b,c st x = a * v1 + b * v2 + c * v3;

theorem :: RLVECT_4:18
   w1 in Lin{w1,w2,w3} & w2 in Lin{w1,w2,w3} & w3 in Lin{w1,w2,w3};

theorem :: RLVECT_4:19
   x in v + Lin{w1,w2,w3} iff ex a,b,c st x = v + a * w1 + b * w2 + c * w3;

theorem :: RLVECT_4:20
   {u,v} is linearly-independent & u <> v implies
  {u,v - u} is linearly-independent;

theorem :: RLVECT_4:21
   {u,v} is linearly-independent & u <> v implies
  {u,v + u} is linearly-independent;

theorem :: RLVECT_4:22
 {u,v} is linearly-independent & u <> v & a <> 0 implies
  {u,a * v} is linearly-independent;

theorem :: RLVECT_4:23
   {u,v} is linearly-independent & u <> v implies
  {u,- v} is linearly-independent;

theorem :: RLVECT_4:24
 a <> b implies {a * v,b * v} is linearly-dependent;

theorem :: RLVECT_4:25
   a <> 1 implies {v,a * v} is linearly-dependent;

theorem :: RLVECT_4:26
   {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
  {u,w,v - u} is linearly-independent;

theorem :: RLVECT_4:27
   {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
  {u,w - u,v - u} is linearly-independent;

theorem :: RLVECT_4:28
   {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
  {u,w,v + u} is linearly-independent;

theorem :: RLVECT_4:29
   {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
  {u,w + u,v + u} is linearly-independent;

theorem :: RLVECT_4:30
 {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 implies
  {u,w,a * v} is linearly-independent;

theorem :: RLVECT_4:31
 {u,w,v} is linearly-independent &
  u <> v & u <> w & v <> w & a <> 0 & b <> 0 implies
   {u,a * w,b * v} is linearly-independent;

theorem :: RLVECT_4:32
   {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
  {u,w,- v} is linearly-independent;

theorem :: RLVECT_4:33
   {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies
  {u,- w,- v} is linearly-independent;

theorem :: RLVECT_4:34
 a <> b implies {a * v,b * v,w} is linearly-dependent;

theorem :: RLVECT_4:35
   a <> 1 implies {v,a * v,w} is linearly-dependent;

theorem :: RLVECT_4:36
   v in Lin{w} & v <> 0.V implies Lin{v} = Lin{w};

theorem :: RLVECT_4:37
   v1 <> v2 & {v1,v2} is linearly-independent &
  v1 in Lin{w1,w2} & v2 in Lin{w1,w2} implies
   Lin{w1,w2} = Lin{v1,v2} & {w1,w2} is linearly-independent & w1 <> w2;

theorem :: RLVECT_4:38
   w <> 0.V & {v,w} is linearly-dependent implies ex a st v = a * w;

theorem :: RLVECT_4:39
   v <> w & {v,w} is linearly-independent & {u,v,w} is linearly-dependent
implies
  ex a,b st u = a * v + b * w;