Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

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

Back to top