:: Subspaces of Real Linear Space Generated by One, Two, or Three Vectors :: and Their Cosets :: by Wojciech A. Trybulec :: :: Received February 24, 1993 :: Copyright (c) 1993-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 REAL_1, RLVECT_1, RLSUB_1, XBOOLE_0, SUBSET_1, FUNCT_1, RLVECT_2, CARD_1, STRUCT_0, NUMBERS, FUNCT_2, TARSKI, ARYTM_3, ARYTM_1, SUPINF_2, RELAT_1, CARD_3, FINSEQ_1, VALUED_1, RLVECT_3; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FINSEQ_1, FUNCT_1, FUNCT_2, XCMPLX_0, XREAL_0, REAL_1, DOMAIN_1, FINSEQ_4, STRUCT_0, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3; constructors DOMAIN_1, REAL_1, FINSEQ_4, RLVECT_2, RLVECT_3, RELSET_1; registrations RELSET_1, FINSET_1, NUMBERS, STRUCT_0, ORDINAL1, XREAL_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 :: RLVECT_4:sch 1 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(); 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; :: RLVECT_1:37 extended theorem :: RLVECT_4:2 v1 - w = v2 - w implies v1 = v2; :: Composition of RLVECT_1:38 and RLVECT_1:39 theorem :: RLVECT_4:3 - (a * v) = (- a) * v; theorem :: RLVECT_4:4 W1 is Subspace of W2 implies v + W1 c= v + W2; theorem :: RLVECT_4:5 u in v + W implies v + W = u + W; theorem :: RLVECT_4:6 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:7 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:8 x in Lin{v} iff ex a st x = a * v; theorem :: RLVECT_4:9 v in Lin{v}; theorem :: RLVECT_4:10 x in v + Lin{w} iff ex a st x = v + a * w; theorem :: RLVECT_4:11 x in Lin{w1,w2} iff ex a,b st x = a * w1 + b * w2; theorem :: RLVECT_4:12 w1 in Lin{w1,w2} & w2 in Lin{w1,w2}; theorem :: RLVECT_4:13 x in v + Lin{w1,w2} iff ex a,b st x = v + a * w1 + b * w2; theorem :: RLVECT_4:14 x in Lin{v1,v2,v3} iff ex a,b,c st x = a * v1 + b * v2 + c * v3; theorem :: RLVECT_4:15 w1 in Lin{w1,w2,w3} & w2 in Lin{w1,w2,w3} & w3 in Lin{w1,w2,w3}; theorem :: RLVECT_4:16 x in v + Lin{w1,w2,w3} iff ex a,b,c st x = v + a * w1 + b * w2 + c * w3; theorem :: RLVECT_4:17 {u,v} is linearly-independent & u <> v implies {u,v - u} is linearly-independent; theorem :: RLVECT_4:18 {u,v} is linearly-independent & u <> v implies {u,v + u} is linearly-independent; theorem :: RLVECT_4:19 {u,v} is linearly-independent & u <> v & a <> 0 implies {u,a * v } is linearly-independent; theorem :: RLVECT_4:20 {u,v} is linearly-independent & u <> v implies {u,- v} is linearly-independent; theorem :: RLVECT_4:21 a <> b implies {a * v,b * v} is linearly-dependent; theorem :: RLVECT_4:22 a <> 1 implies {v,a * v} is linearly-dependent; theorem :: RLVECT_4:23 {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u, w,v - u} is linearly-independent; theorem :: RLVECT_4:24 {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u, w - u,v - u} is linearly-independent; theorem :: RLVECT_4:25 {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u, w,v + u} is linearly-independent; theorem :: RLVECT_4:26 {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u, w + u,v + u} is linearly-independent; theorem :: RLVECT_4:27 {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:28 {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:29 {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u, w,- v} is linearly-independent; theorem :: RLVECT_4:30 {u,w,v} is linearly-independent & u <> v & u <> w & v <> w implies {u, - w,- v} is linearly-independent; theorem :: RLVECT_4:31 a <> b implies {a * v,b * v,w} is linearly-dependent; theorem :: RLVECT_4:32 a <> 1 implies {v,a * v,w} is linearly-dependent; theorem :: RLVECT_4:33 v in Lin{w} & v <> 0.V implies Lin{v} = Lin{w}; theorem :: RLVECT_4:34 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:35 w <> 0.V & {v,w} is linearly-dependent implies ex a st v = a * w; theorem :: RLVECT_4:36 v <> w & {v,w} is linearly-independent & {u,v,w} is linearly-dependent implies ex a,b st u = a * v + b * w; theorem :: RLVECT_4:37 for V be RealLinearSpace, v be VECTOR of V, a be Real ex l being Linear_Combination of {v} st l.v = a; theorem :: RLVECT_4:38 for V be RealLinearSpace, v1, v2 be VECTOR of V, a, b be Real st v1 <> v2 ex l being Linear_Combination of {v1,v2} st l.v1 = a & l.v2 = b; theorem :: RLVECT_4:39 for V be RealLinearSpace, v1, v2, v3 be VECTOR of V, a, b, c be Real st v1 <> v2 & v1 <> v3 & v2 <> v3 ex l being Linear_Combination of {v1,v2,v3} st l.v1 = a & l.v2 = b & l.v3 = c;