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