:: Vectors in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 24, 1989
:: Copyright (c) 1990-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 NUMBERS, ALGSTR_0, STRUCT_0, SUBSET_1, BINOP_1, FUNCT_1,
ZFMISC_1, XBOOLE_0, RELAT_1, REAL_1, ARYTM_3, SUPINF_2, FUNCT_5, MCART_1,
ARYTM_1, CARD_1, FINSEQ_1, ORDINAL4, CARD_3, TARSKI, XXREAL_0, FUNCOP_1,
NAT_1, VALUED_0, RLVECT_1, PARTFUN1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1,
FUNCOP_1, REAL_1, FINSEQ_1, NAT_1, FUNCT_3, FUNCT_5, FINSEQ_4, STRUCT_0,
ALGSTR_0;
constructors BINOP_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, FINSEQ_1, FUNCT_3,
FUNCT_5, ALGSTR_0, REALSET1, RELSET_1, FINSEQ_4, VALUED_0, XREAL_0;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
STRUCT_0, ALGSTR_0, FINSEQ_1, CARD_1, RELAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
definition
struct (addLoopStr) RLSStruct (# carrier -> set,
ZeroF -> Element of the carrier,
addF -> BinOp of the carrier,
Mult -> Function of [:REAL, the carrier :], the carrier #);
end;
registration
cluster non empty for RLSStruct;
end;
reserve V for non empty RLSStruct;
reserve x,y,y1 for set;
definition
let V be RLSStruct;
mode VECTOR of V is Element of V;
end;
theorem :: RLVECT_1:1
for V being non empty 1-sorted, v being Element of V holds v in V;
:: Definitons of functions on the Elements of the carrier of
:: Real Linear Space structure, i.e. zero element, addition of two
:: elements, and multiplication of the element by a real number.
reserve v for VECTOR of V;
reserve a,b for Real;
definition
let V,v;
let a be Real;
func a * v -> Element of V equals
:: RLVECT_1:def 1
(the Mult of V).(a,v);
end;
:: Definitional theorems of zero element, addition, multiplication.
theorem :: RLVECT_1:2
for V being non empty addMagma, v,w being Element of V holds
v + w = (the addF of V).(v,w);
registration
let ZS be non empty set, O be Element of ZS, F be BinOp of ZS, G be Function
of [:REAL,ZS:],ZS;
cluster RLSStruct (# ZS,O,F,G #) -> non empty;
end;
definition
let IT be addMagma;
attr IT is Abelian means
:: RLVECT_1:def 2
for v,w being Element of IT holds v + w = w + v;
attr IT is add-associative means
:: RLVECT_1:def 3
for u,v,w being Element of IT holds (u + v) + w = u + (v + w);
end;
definition
let IT be addLoopStr;
attr IT is right_zeroed means
:: RLVECT_1:def 4
for v being Element of IT holds v + 0.IT = v;
end;
definition
let IT be non empty RLSStruct;
attr IT is vector-distributive means
:: RLVECT_1:def 5
for a for v,w being VECTOR of IT holds a * (v + w) = a * v + a * w;
attr IT is scalar-distributive means
:: RLVECT_1:def 6
for a,b for v being VECTOR of IT holds (a + b) * v = a * v + b * v;
attr IT is scalar-associative means
:: RLVECT_1:def 7
for a,b for v being VECTOR of IT holds (a * b) * v = a * (b * v);
attr IT is scalar-unital means
:: RLVECT_1:def 8
for v being VECTOR of IT holds 1 * v = v;
end;
definition
func Trivial-RLSStruct -> strict RLSStruct equals
:: RLVECT_1:def 9
RLSStruct(#{0},op0,op2,pr2(REAL,{0})#);
end;
registration
cluster Trivial-RLSStruct -> 1-element;
end;
registration
cluster strict Abelian add-associative non empty for addMagma;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
non empty for addLoopStr;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
scalar-distributive vector-distributive scalar-associative scalar-unital
for non empty RLSStruct;
end;
definition
mode RealLinearSpace is Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
non empty RLSStruct;
end;
definition
let V be Abelian addMagma, v,w be Element of V;
redefine func v + w;
commutativity;
end;
theorem :: RLVECT_1:3
for V being add-associative right_zeroed right_complementable
addLoopStr holds V is right_add-cancelable;
theorem :: RLVECT_1:4
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v being Element of V holds v + 0.V = v & 0.V + v = v;
registration
let V be add-associative right_zeroed right_complementable
non empty addLoopStr;
let v1 be zero Element of V;
let v2 be Element of V;
reduce v1 + v2 to v2;
reduce v2 + v1 to v2;
end;
:: Definitions of reverse element to the vector and of
:: subtraction of vectors.
definition
let V be non empty addLoopStr;
let v be Element of V;
assume
V is add-associative right_zeroed right_complementable;
redefine func - v means
:: RLVECT_1:def 10
v + it = 0.V;
end;
definition
let V be addLoopStr;
let v,w be Element of V;
redefine func v - w equals
:: RLVECT_1:def 11
v + (- w);
end;
:: Definitional theorems of reverse element and substraction.
theorem :: RLVECT_1:5
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v being Element of V holds v + -v = 0.V & -v + v = 0.V;
theorem :: RLVECT_1:6
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds v + w = 0.V implies v = - w;
theorem :: RLVECT_1:7
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v,u being Element of V ex w being Element of V st v + w = u;
theorem :: RLVECT_1:8
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, w,u,v1,v2 being Element of V st
w + v1 = w + v2 or v1 + w = v2 + w holds v1 = v2;
theorem :: RLVECT_1:9
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds
v + w = v or w + v = v implies w = 0.V;
theorem :: RLVECT_1:10
for V being add-associative right_zeroed right_complementable
scalar-distributive scalar-unital vector-distributive non empty RLSStruct,
v being Element of V holds
a = 0 or v = 0.V implies a * v = 0.V;
registration
let V be add-associative right_zeroed right_complementable
scalar-distributive scalar-unital vector-distributive non empty RLSStruct;
let v be zero Element of V;
let r be Real;
reduce r * v to v;
end;
theorem :: RLVECT_1:11
for V being add-associative right_zeroed right_complementable
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
a * v = 0.V implies a = 0 or v = 0.V;
theorem :: RLVECT_1:12
for V being add-associative right_zeroed right_complementable
non empty addLoopStr holds - 0.V = 0.V;
registration
let V be add-associative right_zeroed right_complementable
non empty addLoopStr;
let v be zero Element of V;
reduce - v to v;
end;
registration
let V be add-associative right_zeroed right_complementable
non empty addLoopStr;
let v1 be Element of V;
let v2 be zero Element of V;
reduce v1 - v2 to v1;
end;
theorem :: RLVECT_1:13
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v being Element of V holds v - 0.V = v;
theorem :: RLVECT_1:14
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v being Element of V holds 0.V - v = - v;
theorem :: RLVECT_1:15
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v being Element of V holds v - v = 0.V;
theorem :: RLVECT_1:16
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-unital vector-distributive non empty RLSStruct,
v being Element of V holds
- v = (- 1) * v;
registration
let V be add-associative right_zeroed right_complementable
non empty addLoopStr;
let v be Element of V;
reduce --v to v;
end;
theorem :: RLVECT_1:17
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v being Element of V holds --v = v;
theorem :: RLVECT_1:18
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds - v = - w implies v = w;
theorem :: RLVECT_1:19
for V being add-associative right_zeroed right_complementable
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
v = - v implies v = 0.V;
theorem :: RLVECT_1:20
for V being add-associative right_zeroed right_complementable
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
v + v = 0.V implies v = 0.V;
theorem :: RLVECT_1:21
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds v - w = 0.V implies v = w;
theorem :: RLVECT_1:22
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, u,v being Element of V
ex w being Element of V st v - w = u;
theorem :: RLVECT_1:23
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, w,v1,v2 being Element of V st
w - v1 = w - v2 holds v1 = v2;
theorem :: RLVECT_1:24
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
a * (- v) = (- a) * v;
theorem :: RLVECT_1:25
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
a * (- v) = - (a * v);
theorem :: RLVECT_1:26
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
(- a) * (- v) = a * v;
theorem :: RLVECT_1:27
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
v - (u + w) = (v - w) - u;
theorem :: RLVECT_1:28
for V being add-associative non empty addLoopStr,
v,u,w being Element of V holds (v + u) - w = v + (u - w);
theorem :: RLVECT_1:29
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds v - (u - w) = (v -u) + w
;
theorem :: RLVECT_1:30
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds - (v + w) = (- w) - v;
theorem :: RLVECT_1:31
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v,w being Element of V holds - (v + w) = -w + -v;
theorem :: RLVECT_1:32
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds (- v) - w = (- w) - v;
theorem :: RLVECT_1:33
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v,w being Element of V holds - (v - w) = w + (- v);
theorem :: RLVECT_1:34
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v,w being Element of V holds
a * (v - w) = a * v - a * w;
theorem :: RLVECT_1:35
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
(a - b) * v = a * v - b * v;
theorem :: RLVECT_1:36
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v,w being Element of V holds
a <> 0 & a * v = a * w implies v = w;
theorem :: RLVECT_1:37
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
v <> 0.V & a * v = b * v implies a = b;
:: Definition of the sum of the finite sequence of vectors.
reserve V for non empty addLoopStr;
reserve F for FinSequence-like PartFunc of NAT,V;
reserve f,f9,g for sequence of V;
reserve v,u for Element of V;
reserve j,k,n for Nat;
definition
let V; let F be (the carrier of V)-valued FinSequence;
func Sum(F) -> Element of V means
:: RLVECT_1:def 12
ex f st it = f.(len F) & f.0 = 0.V
& for j being Nat,v st j < len F & v = F.(j + 1) holds f.(j + 1) = f.j + v;
end;
theorem :: RLVECT_1:38
for F,G being FinSequence of V holds
len F = len G + 1 & G = F | (dom G) & v = F.(len F) implies
Sum(F) = Sum(G) + v;
reserve V for RealLinearSpace;
reserve v for VECTOR of V;
reserve F,G,H,I for FinSequence of V;
theorem :: RLVECT_1:39
len F = len G & (for k,v st k in dom F & v = G.k holds F.k = a * v)
implies Sum(F) = a * Sum(G);
theorem :: RLVECT_1:40
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, F,G being FinSequence of V st len F = len G &
(for k for v being Element of V st k in dom F & v = G.k holds F.k = - v)
holds Sum(F) = - Sum(G);
theorem :: RLVECT_1:41
for V being add-associative right_zeroed non empty addLoopStr,
F,G being FinSequence of V holds Sum(F ^ G) = Sum(F) + Sum(G);
reserve V for add-associative right_zeroed right_complementable non empty
addLoopStr;
reserve F for FinSequence of V;
reserve v,v1,v2,u,w for Element of V;
reserve j,k for Nat;
theorem :: RLVECT_1:42
for V being Abelian add-associative right_zeroed non empty addLoopStr,
F,G being FinSequence of V st rng F = rng G & F is one-to-one
& G is one-to-one holds Sum(F) = Sum(G);
theorem :: RLVECT_1:43
for V being non empty addLoopStr holds Sum(<*>(the carrier of V)) = 0.V;
theorem :: RLVECT_1:44
for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v being Element of V holds Sum<* v *> = v;
theorem :: RLVECT_1:45
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,u being Element of V holds Sum<* v,u *> = v + u;
theorem :: RLVECT_1:46
for V being add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
Sum<* v,u,w *> = v + u + w;
theorem :: RLVECT_1:47
for V being RealLinearSpace, a being Real holds
a * Sum(<*>(the carrier of V)) = 0.V;
theorem :: RLVECT_1:48
for V being RealLinearSpace, a being Real, v,u being VECTOR of V holds
a * Sum<* v,u *> = a * v + a * u;
theorem :: RLVECT_1:49
for V being RealLinearSpace, a being Real, v,u,w being VECTOR of V
holds a * Sum<* v,u,w *> = a * v + a * u + a * w;
theorem :: RLVECT_1:50
- Sum(<*>(the carrier of V)) = 0.V;
theorem :: RLVECT_1:51
- Sum<* v *> = - v;
theorem :: RLVECT_1:52
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u being Element of V holds - Sum<* v,u *> = (- v) - u;
theorem :: RLVECT_1:53
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
- Sum<* v,u,w *> = ((- v) - u) - w;
theorem :: RLVECT_1:54
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds
Sum<* v,w *> = Sum<* w,v*>;
theorem :: RLVECT_1:55
Sum<* v,w *> = Sum<* v *> + Sum<* w *>;
::$CT
theorem :: RLVECT_1:57
Sum<* 0.V,v *> = v & Sum<* v,0.V *> = v;
theorem :: RLVECT_1:58
Sum<* v,- v *> = 0.V & Sum<* - v,v *> = 0.V;
theorem :: RLVECT_1:59
Sum<* v,- w *> = v - w;
theorem :: RLVECT_1:60
Sum<* - v,- w *> = - (w + v);
theorem :: RLVECT_1:61
for V being RealLinearSpace, v being VECTOR of V holds Sum<* v,v *> = 2 * v;
theorem :: RLVECT_1:62
for V being RealLinearSpace, v being VECTOR of V holds
Sum<* - v,- v*> = (- 2) * v;
theorem :: RLVECT_1:63
Sum<* u,v,w *> = Sum<* u *> + Sum<* v *> + Sum<* w *>;
theorem :: RLVECT_1:64
Sum<* u,v,w *> = Sum<* u,v *> + w;
theorem :: RLVECT_1:65
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
Sum<* u,v,w *> = Sum<* v,w *> + u;
theorem :: RLVECT_1:66
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u,w being Element of V holds
Sum <* u,v,w *> = Sum<* u,w *> + v;
theorem :: RLVECT_1:67
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u,w being Element of V holds
Sum <* u,v,w *> = Sum<* u,w,v *>;
theorem :: RLVECT_1:68
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u,w being Element of V holds
Sum <* u,v,w *> = Sum<* v,u,w *>;
theorem :: RLVECT_1:69
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u,w being Element of V holds
Sum <* u,v,w *> = Sum<* v,w,u *>;
theorem :: RLVECT_1:70
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
Sum<* u,v,w *> = Sum<* w,v,u *>;
::$CT
theorem :: RLVECT_1:72
Sum<* 0.V,0.V,v *> = v & Sum<* 0.V,v,0.V *> = v & Sum<* v,0.V,0.V *> = v;
theorem :: RLVECT_1:73
Sum<*0.V,u,v*> = u + v & Sum<*u,v,0.V*> = u + v & Sum<*u,0.V,v*> = u + v;
theorem :: RLVECT_1:74
for V being RealLinearSpace, v being VECTOR of V holds Sum<* v,v,v *> = 3 * v
;
theorem :: RLVECT_1:75
len F = 0 implies Sum(F) = 0.V;
theorem :: RLVECT_1:76
len F = 1 implies Sum(F) = F.1;
theorem :: RLVECT_1:77
len F = 2 & v1 = F.1 & v2 = F.2 implies Sum(F) = v1 + v2;
theorem :: RLVECT_1:78
len F = 3 & v1 = F.1 & v2 = F.2 & v = F.3 implies Sum(F) = v1 + v2 + v;
begin :: from REALSET2, 2007.02.24, A.T
definition
let L be non empty addLoopStr;
attr L is zeroed means
:: RLVECT_1:def 13
for a being Element of L holds a+0.L = a & 0.L+a = a;
end;
registration
cluster zeroed -> right_zeroed for non empty addLoopStr;
end;
registration
cluster Abelian right_zeroed -> zeroed for non empty addLoopStr;
cluster Abelian right_complementable -> left_complementable for non empty
addLoopStr;
end;
:: missing, 2009.02.14, A.T.
theorem :: RLVECT_1:79
for V being add-associative right_zeroed right_complementable Abelian
scalar-distributive scalar-associative scalar-unital vector-distributive
non empty RLSStruct,
v being Element of V holds
(- a) * v = - a * v;
begin :: VECTSP_3
reserve x,y for set,
k,n for Element of NAT;
theorem :: RLVECT_1:80
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr holds - Sum(<*>(the carrier of V)) = 0.V;
theorem :: RLVECT_1:81
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u being Element of V holds - Sum<* v,u *> = (- v) - u
;
theorem :: RLVECT_1:82
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,u,w being Element of V holds
- Sum<* v,u,w *> = ((- v) - u) - w;
theorem :: RLVECT_1:83
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v being Element of V holds
Sum<* v,- v *> = 0.V & Sum<*- v,v *> = 0.V;
theorem :: RLVECT_1:84
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds
Sum<* v,- w *> = v - w & Sum<* - w,v *> = v - w;
theorem :: RLVECT_1:85
for V being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, v,w being Element of V holds
Sum<* - v,- w *> = - (v + w) & Sum<* - w,- v *> = - (v + w);