Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

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

by
Wojciech A. Trybulec

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;
```