Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Vectors in Real Linear Space

**by****Wojciech A. Trybulec**- Received July 24, 1989
- MML identifier: RLVECT_1

- [ Mizar article, MML identifier index ]

environ vocabulary BINOP_1, FUNCT_1, ARYTM_1, RELAT_1, FINSEQ_1, BOOLE, RLVECT_1, ANPROJ_1, ORDINAL2, ARYTM; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0, XREAL_0, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, REAL_1, FINSEQ_1, NAT_1, STRUCT_0; constructors DOMAIN_1, BINOP_1, REAL_1, FINSEQ_1, NAT_1, STRUCT_0, XREAL_0, MEMBERED, XBOOLE_0, ORDINAL2; clusters RELSET_1, FINSEQ_1, STRUCT_0, XREAL_0, SUBSET_1, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2, NUMBERS, ARYTM_3, XCMPLX_0; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin definition struct (ZeroStr) LoopStr (# carrier -> set, add -> BinOp of the carrier, Zero -> Element of the carrier #); end; definition struct (LoopStr) RLSStruct (# carrier -> set, Zero -> Element of the carrier, add -> BinOp of the carrier, Mult -> Function of [:REAL, the carrier:], the carrier #); end; definition cluster non empty RLSStruct; end; reserve V for non empty RLSStruct; reserve x,y,y1,y2 for set; definition let V be RLSStruct; mode VECTOR of V is Element of V; end; definition let V be 1-sorted; let x; pred x in V means :: RLVECT_1:def 1 x in the carrier of V; end; canceled 2; theorem :: RLVECT_1:3 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. :: definition let V be ZeroStr; func 0.V -> Element of V equals :: RLVECT_1:def 2 the Zero of V; end; reserve v for VECTOR of V; reserve a,b for Real; definition cluster strict non empty LoopStr; end; definition let V be non empty LoopStr, v,w be Element of V; func v + w -> Element of V equals :: RLVECT_1:def 3 (the add of V).[v,w]; end; definition let V; let v; let a; func a * v -> Element of V equals :: RLVECT_1:def 4 (the Mult of V).[a,v]; end; :: :: Definitional theorems of zero element, addition, multiplication. :: canceled; theorem :: RLVECT_1:5 for V being non empty LoopStr, v,w being Element of V holds v + w = (the add of V).(v,w); definition 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 non empty LoopStr; attr IT is Abelian means :: RLVECT_1:def 5 for v,w being Element of IT holds v + w = w + v; attr IT is add-associative means :: RLVECT_1:def 6 for u,v,w being Element of IT holds (u + v) + w = u + (v + w); attr IT is right_zeroed means :: RLVECT_1:def 7 for v being Element of IT holds v + 0.IT = v; attr IT is right_complementable means :: RLVECT_1:def 8 for v being Element of IT ex w being Element of IT st v + w = 0.IT; end; definition let IT be non empty RLSStruct; attr IT is RealLinearSpace-like means :: RLVECT_1:def 9 (for a for v,w being VECTOR of IT holds a * (v + w) = a * v + a * w) & (for a,b for v being VECTOR of IT holds (a + b) * v = a * v + b * v) & (for a,b for v being VECTOR of IT holds (a * b) * v = a * (b * v)) & (for v being VECTOR of IT holds 1 * v = v); end; definition cluster strict Abelian add-associative right_zeroed right_complementable (non empty LoopStr); end; definition cluster non empty strict Abelian add-associative right_zeroed right_complementable RealLinearSpace-like (non empty RLSStruct); end; definition mode RealLinearSpace is Abelian add-associative right_zeroed right_complementable RealLinearSpace-like (non empty RLSStruct); end; definition let V be Abelian (non empty LoopStr), v,w be Element of V; redefine func v + w; commutativity; end; canceled; theorem :: RLVECT_1:7 (for v,w being VECTOR of V holds v + w = w + v) & (for u,v,w being VECTOR of V holds (u + v) + w = u + (v + w)) & (for v being VECTOR of V holds v + 0.V = v) & (for v being VECTOR of V ex w being VECTOR of V st v + w = 0.V) & (for a for v,w being VECTOR of V holds a * (v + w) = a * v + a * w) & (for a,b for v being VECTOR of V holds (a + b) * v = a * v + b * v) & (for a,b for v being VECTOR of V holds (a * b) * v = a * (b * v)) & (for v being VECTOR of V holds 1 * v = v) implies V is RealLinearSpace; :: :: Axioms of real linear space. :: reserve V for RealLinearSpace; reserve v,w for VECTOR of V; canceled 2; theorem :: RLVECT_1:10 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v being Element of V holds v + 0.V = v & 0.V + v = v; :: :: Definitions of reverse element to the vector and of :: subtraction of vectors. :: definition let V be non empty LoopStr; let v be Element of V; assume V is add-associative right_zeroed right_complementable; func - v -> Element of V means :: RLVECT_1:def 10 v + it = 0.V; end; definition let V be non empty LoopStr; let v,w be Element of V; func v - w -> Element of V equals :: RLVECT_1:def 11 v + (- w); end; :: :: Definitional theorems of reverse element and substraction. :: canceled 5; theorem :: RLVECT_1:16 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v being Element of V holds v + -v = 0.V & -v + v = 0.V; canceled 2; theorem :: RLVECT_1:19 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,w being Element of V holds v + w = 0.V implies v = - w; theorem :: RLVECT_1:20 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,u being Element of V ex w being Element of V st v + w = u; theorem :: RLVECT_1:21 for V being add-associative right_zeroed right_complementable (non empty LoopStr), w,u,v1,v2 being Element of V st w + v1 = w + v2 or v1 + w = v2 + w holds v1 = v2; theorem :: RLVECT_1:22 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,w being Element of V holds v + w = v or w + v = v implies w = 0.V; theorem :: RLVECT_1:23 a = 0 or v = 0.V implies a * v = 0.V; theorem :: RLVECT_1:24 a * v = 0.V implies a = 0 or v = 0.V; theorem :: RLVECT_1:25 for V being add-associative right_zeroed right_complementable (non empty LoopStr) holds - 0.V = 0.V; theorem :: RLVECT_1:26 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v being Element of V holds v - 0.V = v; theorem :: RLVECT_1:27 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v being Element of V holds 0.V - v = - v; theorem :: RLVECT_1:28 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v being Element of V holds v - v = 0.V; theorem :: RLVECT_1:29 - v = (- 1) * v; theorem :: RLVECT_1:30 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v being Element of V holds - (- v) = v; theorem :: RLVECT_1:31 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,w being Element of V holds - v = - w implies v = w; canceled; theorem :: RLVECT_1:33 v = - v implies v = 0.V; theorem :: RLVECT_1:34 v + v = 0.V implies v = 0.V; theorem :: RLVECT_1:35 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,w being Element of V holds v - w = 0.V implies v = w; theorem :: RLVECT_1:36 for V being add-associative right_zeroed right_complementable (non empty LoopStr), u,v being Element of V ex w being Element of V st v - w = u; theorem :: RLVECT_1:37 for V being add-associative right_zeroed right_complementable (non empty LoopStr), w,v1,v2 being Element of V st w - v1 = w - v2 holds v1 = v2; theorem :: RLVECT_1:38 a * (- v) = (- a) * v; theorem :: RLVECT_1:39 a * (- v) = - (a * v); theorem :: RLVECT_1:40 (- a) * (- v) = a * v; theorem :: RLVECT_1:41 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,u,w being Element of V holds v - (u + w) = (v - w) - u; theorem :: RLVECT_1:42 for V being add-associative (non empty LoopStr), v,u,w being Element of V holds (v + u) - w = v + (u - w); theorem :: RLVECT_1:43 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,u,w being Element of V holds v - (u - w) = (v -u) + w; theorem :: RLVECT_1:44 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,w being Element of V holds - (v + w) = (- w) - v; theorem :: RLVECT_1:45 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,w being Element of V holds - (v + w) = -w + -v; theorem :: RLVECT_1:46 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,w being Element of V holds (- v) - w = (- w) - v; theorem :: RLVECT_1:47 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,w being Element of V holds - (v - w) = w + (- v); theorem :: RLVECT_1:48 a * (v - w) = a * v - a * w; theorem :: RLVECT_1:49 (a - b) * v = a * v - b * v; theorem :: RLVECT_1:50 a <> 0 & a * v = a * w implies v = w; theorem :: RLVECT_1:51 v <> 0.V & a * v = b * v implies a = b; :: :: Definition of the sum of the finite sequence of vectors. :: definition let V be non empty 1-sorted; let v,u be Element of V; redefine func <* v,u *> -> FinSequence of the carrier of V; end; definition let V be non empty 1-sorted; let v,u,w be Element of V; redefine func <* v,u,w *> -> FinSequence of the carrier of V; end; reserve V for non empty LoopStr; reserve F,G,H for FinSequence of the carrier of V; reserve f,f',g for Function of NAT, the carrier of V; reserve v,u for Element of V; reserve j,k,n for Nat; definition let V; let F; func Sum(F) -> Element of V means :: RLVECT_1:def 12 ex f st it = f.(len F) & f.0 = 0.V & for j,v st j < len F & v = F.(j + 1) holds f.(j + 1) = f.j + v; end; canceled 2; theorem :: RLVECT_1:54 k in Seg n & len F = n implies F.k is Element of V; theorem :: RLVECT_1:55 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 the carrier of V; theorem :: RLVECT_1:56 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:57 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), F,G being FinSequence of the carrier 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:58 for V being add-associative right_zeroed (non empty LoopStr), F,G being FinSequence of the carrier of V holds Sum(F ^ G) = Sum(F) + Sum(G); reserve V for add-associative right_zeroed right_complementable (non empty LoopStr); reserve F for FinSequence of the carrier of V; reserve v,v1,v2,u,w for Element of V; reserve i,j,k,n for Nat; reserve p,q for FinSequence; theorem :: RLVECT_1:59 for V being Abelian add-associative right_zeroed (non empty LoopStr), F,G being FinSequence of the carrier 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:60 for V being non empty LoopStr holds Sum(<*>(the carrier of V)) = 0.V; theorem :: RLVECT_1:61 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v being Element of V holds Sum<* v *> = v; theorem :: RLVECT_1:62 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,u being Element of V holds Sum<* v,u *> = v + u; theorem :: RLVECT_1:63 for V being add-associative right_zeroed right_complementable (non empty LoopStr), v,u,w being Element of V holds Sum<* v,u,w *> = v + u + w; theorem :: RLVECT_1:64 for V being RealLinearSpace, a being Real holds a * Sum(<*>(the carrier of V)) = 0.V; canceled; theorem :: RLVECT_1:66 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:67 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:68 - Sum(<*>(the carrier of V)) = 0.V; theorem :: RLVECT_1:69 - Sum<* v *> = - v; theorem :: RLVECT_1:70 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,u being Element of V holds - Sum<* v,u *> = (- v) - u; theorem :: RLVECT_1:71 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,u,w being Element of V holds - Sum<* v,u,w *> = ((- v) - u) - w; theorem :: RLVECT_1:72 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,w being Element of V holds Sum<* v,w *> = Sum<* w,v *>; theorem :: RLVECT_1:73 Sum<* v,w *> = Sum<* v *> + Sum<* w *>; theorem :: RLVECT_1:74 Sum<* 0.V,0.V *> = 0.V; theorem :: RLVECT_1:75 Sum<* 0.V,v *> = v & Sum<* v,0.V *> = v; theorem :: RLVECT_1:76 Sum<* v,- v *> = 0.V & Sum<* - v,v *> = 0.V; theorem :: RLVECT_1:77 Sum<* v,- w *> = v - w; theorem :: RLVECT_1:78 Sum<* - v,- w *> = - (w + v); theorem :: RLVECT_1:79 for V being RealLinearSpace, v being VECTOR of V holds Sum<* v,v *> = 2 * v; theorem :: RLVECT_1:80 for V being RealLinearSpace, v being VECTOR of V holds Sum<* - v,- v *> = (- 2) * v; theorem :: RLVECT_1:81 Sum<* u,v,w *> = Sum<* u *> + Sum<* v *> + Sum<* w *>; theorem :: RLVECT_1:82 Sum<* u,v,w *> = Sum<* u,v *> + w; theorem :: RLVECT_1:83 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,u,w being Element of V holds Sum<* u,v,w *> = Sum<* v,w *> + u; theorem :: RLVECT_1:84 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,u,w being Element of V holds Sum<* u,v,w *> = Sum<* u,w *> + v; theorem :: RLVECT_1:85 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,u,w being Element of V holds Sum<* u,v,w *> = Sum<* u,w,v *>; theorem :: RLVECT_1:86 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,u,w being Element of V holds Sum<* u,v,w *> = Sum<* v,u,w *>; theorem :: RLVECT_1:87 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,u,w being Element of V holds Sum<* u,v,w *> = Sum<* v,w,u *>; canceled; theorem :: RLVECT_1:89 for V being Abelian add-associative right_zeroed right_complementable (non empty LoopStr), v,u,w being Element of V holds Sum<* u,v,w *> = Sum<* w,v,u *>; theorem :: RLVECT_1:90 Sum<* 0.V,0.V,0.V *> = 0.V; theorem :: RLVECT_1:91 Sum<* 0.V,0.V,v *> = v & Sum<* 0.V,v,0.V *> = v & Sum<* v,0.V,0.V *> = v; theorem :: RLVECT_1:92 Sum<* 0.V,u,v *> = u + v & Sum<* u,v,0.V *> = u + v & Sum<* u,0.V,v *> = u + v; theorem :: RLVECT_1:93 for V being RealLinearSpace, v being VECTOR of V holds Sum<* v,v,v *> = 3 * v; theorem :: RLVECT_1:94 len F = 0 implies Sum(F) = 0.V; theorem :: RLVECT_1:95 len F = 1 implies Sum(F) = F.1; theorem :: RLVECT_1:96 len F = 2 & v1 = F.1 & v2 = F.2 implies Sum(F) = v1 + v2; theorem :: RLVECT_1:97 len F = 3 & v1 = F.1 & v2 = F.2 & v = F.3 implies Sum(F) = v1 + v2 + v; :: :: Auxiliary theorems. :: definition let R be non empty ZeroStr, a be Element of R; attr a is non-zero means :: RLVECT_1:def 13 a <> 0.R; end; reserve j, k, n for natural number; theorem :: RLVECT_1:98 j < 1 implies j = 0; theorem :: RLVECT_1:99 1 <= k iff k <> 0; canceled 2; theorem :: RLVECT_1:102 k <> 0 implies n < n + k; theorem :: RLVECT_1:103 k < k + n iff 1 <= n; theorem :: RLVECT_1:104 Seg k = Seg(k + 1) \ {k + 1}; theorem :: RLVECT_1:105 p = (p ^ q) | (dom p); theorem :: RLVECT_1:106 rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q;

Back to top