:: Introduction to Banach and Hilbert spaces - Part I :: by Jan Popio{\l}ek :: :: Received July 19, 1991 :: Copyright (c) 1991-2018 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, RLVECT_1, STRUCT_0, SUBSET_1, ALGSTR_0, BINOP_1, FUNCT_1, ZFMISC_1, XBOOLE_0, REAL_1, PRE_TOPC, SUPINF_2, PROB_2, RLSUB_1, FUNCOP_1, CARD_1, ARYTM_3, RELAT_1, XXREAL_0, ARYTM_1, COMPLEX1, SQUARE_1, FUNCT_3, RVSUM_1, NORMSP_1, METRIC_1, NAT_1, BHSP_1, PARTFUN1, FUNCT_7; notations XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, NAT_1, STRUCT_0, ALGSTR_0, DOMAIN_1, PRE_TOPC, RLVECT_1, RLSUB_1, SQUARE_1, VFUNCT_1, NORMSP_1, QUIN_1, XXREAL_0; constructors BINOP_1, DOMAIN_1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, MEMBERED, COMPLEX1, QUIN_1, RLSUB_1, NORMSP_1, RELSET_1, VFUNCT_1; registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, STRUCT_0, XBOOLE_0, ALGSTR_0, FUNCT_2, VFUNCT_1, QUIN_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions STRUCT_0, ALGSTR_0, RLVECT_1, VALUED_0, FUNCT_2; equalities STRUCT_0, SQUARE_1, ALGSTR_0, RLVECT_1; expansions VALUED_0; theorems TARSKI, SQUARE_1, ABSVALUE, RLVECT_1, RLSUB_1, QUIN_1, FUNCT_2, NORMSP_1, COMPLEX1, FUNCOP_1, XREAL_1, XXREAL_0, ALGSTR_0, ORDINAL1, VFUNCT_1, PARTFUN1; schemes FUNCT_2; begin definition struct(RLSStruct) UNITSTR (# carrier -> set, ZeroF -> Element of the carrier, addF -> BinOp of the carrier, Mult -> Function of [:REAL, the carrier:], the carrier, scalar -> Function of [: the carrier, the carrier :], REAL #); end; registration cluster non empty strict for UNITSTR; existence proof set D = the non empty set,Z = the Element of D,a = the BinOp of D,m =the Function of [:REAL, D:], D,s = the Function of [: D,D:],REAL; take UNITSTR (#D,Z,a,m,s#); thus the carrier of UNITSTR (#D,Z,a,m,s#) is non empty; thus thesis; end; end; registration let D be non empty set, Z be Element of D, a be BinOp of D,m be Function of [:REAL, D:], D, s be Function of [: D,D:],REAL; cluster UNITSTR (#D,Z,a,m,s#) -> non empty; coherence; end; reserve X for non empty UNITSTR; reserve a, b for Real; reserve x, y for Point of X; deffunc 09(UNITSTR) = 0.$1; definition let X; let x, y; func x .|. y -> Real equals (the scalar of X).[x,y]; correctness; end; set V0 = the RealLinearSpace; Lm1: the carrier of (0).V0 = {0.V0} by RLSUB_1:def 3; reconsider nilfunc = [: the carrier of (0).V0, the carrier of (0).V0 :] --> In(0,REAL) as Function of [: the carrier of (0).V0, the carrier of (0).V0 :] , REAL; ( for x, y being VECTOR of (0).V0 holds nilfunc.[x,y] = 0)& 0.V0 in the carrier of (0).V0 by Lm1,FUNCOP_1:7,TARSKI:def 1; then Lm2: nilfunc.[0.V0,0.V0] = 0; Lm3: for u, v being VECTOR of (0).V0 holds nilfunc.[u,v] = nilfunc.[v,u] proof let u, v be VECTOR of (0).V0; u = 0.V0 & v = 0.V0 by Lm1,TARSKI:def 1; hence thesis; end; Lm4: for u, v, w being VECTOR of (0).V0 holds nilfunc.[u+v,w] = nilfunc.[u,w] + nilfunc.[v,w] proof let u, v, w be VECTOR of (0).V0; A1: w = 0.V0 by Lm1,TARSKI:def 1; u = 0.V0 & v = 0.V0 by Lm1,TARSKI:def 1; hence thesis by A1,Lm1,Lm2,TARSKI:def 1; end; Lm5: for u, v being VECTOR of (0).V0, a holds nilfunc.[a*u,v] = a * nilfunc.[u ,v] proof let u, v be VECTOR of (0).V0; let a; u = 0.V0 & v = 0.V0 by Lm1,TARSKI:def 1; hence thesis by Lm1,Lm2,TARSKI:def 1; end; set X0 = UNITSTR(# the carrier of (0).V0,0.(0).V0,the addF of (0).V0, the Mult of (0).V0, nilfunc #); Lm6: now let x, y, z be Point of X0; let a; 09(X0) = 0.V0 by RLSUB_1:11; hence x .|. x = In(0,REAL) iff x = 09(X0) by Lm1,FUNCOP_1:7,TARSKI:def 1; thus 0 <= x .|. x by FUNCOP_1:7; thus x .|. y = y .|. x by Lm3; thus (x+y) .|. z = x .|. z + y .|. z proof reconsider u = x, v = y, w = z as VECTOR of (0).V0; (x+y) .|. z = nilfunc.[u+v,w]; hence thesis by Lm4; end; thus (a*x) .|. y = a * ( x .|. y ) proof reconsider u = x, v = y as VECTOR of (0).V0; (a*x) .|. y = nilfunc.[a*u,v]; hence thesis by Lm5; end; end; definition let IT be non empty UNITSTR; attr IT is RealUnitarySpace-like means :Def2: for x, y, z being Point of IT, a holds ( x .|. x = 0 iff x = 0.IT ) & 0 <= x .|. x & x .|. y = y .|. x & (x+y) .|. z = x .|. z + y .|. z & (a*x) .|. y = a * ( x .|. y ); end; registration cluster RealUnitarySpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable strict for non empty UNITSTR; existence proof take X0; thus X0 is RealUnitarySpace-like by Lm6; thus X0 is vector-distributive scalar-distributive scalar-associative scalar-unital proof thus for a being Real for v,w being VECTOR of X0 holds a * (v + w ) = a * v + a * w proof let a be Real; let v,w be VECTOR of X0; reconsider v9= v, w9 = w as VECTOR of (0).V0; thus a * (v + w) = a *( v9 + w9) .= a * v9 + a * w9 by RLVECT_1:def 5 .= a * v + a * w; end; thus for a,b being Real for v being VECTOR of X0 holds (a + b) * v = a * v + b * v proof let a,b be Real; let v be VECTOR of X0; reconsider v9= v as VECTOR of (0).V0; thus (a + b) * v = (a + b) * v9 .= a * v9 + b * v9 by RLVECT_1:def 6 .= a * v + b * v; end; thus for a,b being Real for v being VECTOR of X0 holds (a * b) * v = a * (b * v) proof let a,b be Real; let v be VECTOR of X0; reconsider v9= v as VECTOR of (0).V0; thus (a * b) * v = (a * b) * v9 .= a * (b * v9) by RLVECT_1:def 7 .= a * (b * v); end; let v be VECTOR of X0; reconsider v9= v as VECTOR of (0).V0; thus 1 * v = 1 * v9 .= v by RLVECT_1:def 8; end; A1: for x,y be VECTOR of X0 for x9,y9 be VECTOR of (0).V0 st x = x9 & y = y9 holds x + y= x9 + y9 & for a holds a * x = a * x9; thus for v,w being VECTOR of X0 holds v + w = w + v proof let v,w be VECTOR of X0; reconsider v9= v, w9= w as VECTOR of (0).V0; thus v + w = w9+ v9 by A1 .= w + v; end; thus for u,v,w being VECTOR of X0 holds (u + v) + w = u + (v + w) proof let u,v,w be VECTOR of X0; reconsider u9= u, v9= v, w9= w as VECTOR of (0).V0; thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def 3 .= u + (v + w); end; thus for v being VECTOR of X0 holds v + 0.X0 = v proof let v be VECTOR of X0; reconsider v9= v as VECTOR of (0).V0; thus v + 0.X0 = v9+ 0.(0).V0 .=v by RLVECT_1:4; end; thus X0 is right_complementable proof let v be VECTOR of X0; reconsider v9= v as VECTOR of (0).V0; consider w9 be VECTOR of (0).V0 such that A2: v9 + w9 = 0.(0).V0 by ALGSTR_0:def 11; reconsider w = w9 as VECTOR of X0; take w; thus thesis by A2; end; thus thesis; end; end; definition mode RealUnitarySpace is RealUnitarySpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty UNITSTR; end; reserve X for RealUnitarySpace; reserve x, y, z, u, v for Point of X; definition let X, x, y; redefine func x .|. y; commutativity by Def2; end; theorem (0.X) .|. (0.X) = 0 by Def2; theorem x .|. (y+z) = x .|. y + x .|. z by Def2; theorem x .|. (a*y) = a * x .|. y by Def2; theorem (a*x) .|. y = x .|. (a*y) proof (a*x) .|. y = a * x .|. y by Def2; hence thesis by Def2; end; theorem Th5: (a*x+b*y) .|. z = a * x .|. z + b * y .|. z proof (a*x+b*y) .|. z = (a*x) .|. z + (b*y) .|. z by Def2 .= a * x .|. z + (b*y) .|. z by Def2; hence thesis by Def2; end; theorem x .|. (a*y + b*z) = a * x .|. y + b * x .|. z by Th5; theorem (-x) .|. y = x .|. (-y) proof (-x) .|. y = ((-1)*x) .|. y by RLVECT_1:16 .= (-1) * x .|. y by Def2 .= x .|. ((-1)*y) by Def2; hence thesis by RLVECT_1:16; end; theorem Th8: (-x) .|. y = - x .|. y proof (-x) .|. y = ((-1)*x) .|. y by RLVECT_1:16 .= (-1) * x .|. y by Def2; hence thesis; end; theorem x .|. (-y) = - x .|. y by Th8; theorem Th10: (-x) .|. (-y) = x .|. y proof (-x) .|. (-y) = - x .|. (-y) by Th8 .= - ( - x .|. y ) by Th8; hence thesis; end; theorem Th11: (x - y) .|. z = x .|. z - y .|. z proof (x - y) .|. z = x .|. z + (-y) .|. z by Def2 .= x .|. z + ( - y .|. z ) by Th8; hence thesis; end; theorem Th12: x .|. (y - z) = x .|. y - x .|. z proof x .|. (y - z) = x .|. y + x .|. (-z) by Def2 .= x .|. y + ( - x .|. z ) by Th8; hence thesis; end; theorem (x - y) .|. (u - v) = x .|. u - x .|. v - y .|. u + y .|. v proof (x - y) .|. (u - v) = x .|. (u - v) - y .|. (u - v) by Th11 .= ( x .|. u - x .|. v ) - y .|. (u - v) by Th12 .= ( x .|. u - x .|. v ) - ( y .|. u - y .|. v ) by Th12; hence thesis; end; theorem Th14: (0.X) .|. x = 0 proof 09(X) .|. x = (x + (-x)) .|. x by RLVECT_1:5 .= x .|. x + (-x) .|. x by Def2 .= x .|. x + ( - x .|. x ) by Th8; hence thesis; end; theorem x .|. 0.X = 0 by Th14; theorem Th16: (x + y) .|. (x + y) = x .|. x + 2 * x .|. y + y .|. y proof (x + y) .|. (x + y) = x .|. (x + y) + y .|. (x + y) by Def2 .= (x .|. x + x .|. y) + y .|. (x + y) by Def2 .= (x .|. x + x .|. y) + (x .|. y + y .|. y) by Def2 .= (x .|. x + (x .|. y + x .|. y)) + y .|. y; hence thesis; end; theorem (x + y) .|. (x - y) = x .|. x - y .|. y proof (x + y) .|. (x - y) = x .|. (x - y) + y .|. (x - y) by Def2 .= (x .|. x - x .|. y) + y .|. (x - y) by Th12 .= (x .|. x - x .|. y) + (x .|. y - y .|. y) by Th12; hence thesis; end; theorem Th18: (x - y) .|. (x - y) = x .|. x - 2 * x .|. y + y .|. y proof (x - y) .|. (x - y) = x .|. (x - y) - y .|. (x - y) by Th11 .= x .|. x - x .|. y - y .|. (x - y) by Th12 .= x .|. x - x .|. y - ( x .|. y - y .|. y ) by Th12 .= x .|. x - ( x .|. y + x .|. y ) + y .|. y; hence thesis; end; theorem Th19: |.x .|. y.| <= sqrt (x .|. x) * sqrt (y .|. y) proof A1: x <> 09(X) implies |.x .|. y.| <= sqrt (x .|. x) * sqrt (y .|. y) proof A2: for t be Real holds x .|. x * t^2 + (2 * x .|. y) * t + y .|. y >= 0 proof let t be Real; reconsider t as Real; (t * x + y) .|. (t * x + y) >= 0 by Def2; then (t * x) .|. (t * x) + 2 * (t * x) .|. y + y .|. y >= 0 by Th16; then t * x .|. (t * x) + 2 * (t * x) .|. y + y .|. y >= 0 by Def2; then t * ( t * x .|. x) + 2 * (t * x) .|. y + y .|. y >= 0 by Def2; then x .|. x * t^2 + 2 * (x .|. y * t) + y .|. y >= 0 by Def2; hence thesis; end; A3: x .|. x >= 0 by Def2; assume x <> 09(X); then x .|. x <> 0 by Def2; then delta(x .|. x,(2 * x .|. y),y.|.y) <= 0 by A3,A2,QUIN_1:10; then (2 * x .|. y)^2 - 4 * x .|. x * y .|. y <= 0 by QUIN_1:def 1; then 4 * ((x .|. y)^2 - x .|. x * y .|. y) <= 0; then (x .|. y)^2 - x .|. x * y .|. y <= 0/4 by XREAL_1:77; then (x .|. y)^2 <= x .|. x * y .|. y by XREAL_1:50; then (|.x .|. y.|)^2 >= 0 & (|.x .|. y.|)^2 <= x .|. x * y .|. y by COMPLEX1:75,XREAL_1:63; then sqrt (|.x .|. y.|)^2 <= sqrt (x .|. x * y .|. y) by SQUARE_1:26; then A4: |.x .|. y.| <= sqrt (x .|. x * y .|. y) by COMPLEX1:46,SQUARE_1:22; y .|. y >= 0 by Def2; hence thesis by A3,A4,SQUARE_1:29; end; x = 09(X) implies |.x .|. y.| <= sqrt (x .|. x) * sqrt (y .|. y) proof assume x = 09(X); then x .|. y = 0 & sqrt (x .|. x) = 0 by Th14,SQUARE_1:17; hence thesis by ABSVALUE:2; end; hence thesis by A1; end; definition let X, x, y; pred x, y are_orthogonal means x .|. y = 0; symmetry; end; theorem x, y are_orthogonal implies x, - y are_orthogonal proof assume x, y are_orthogonal; then - x .|. y = - 0; then x .|. (-y) = 0 by Th8; hence thesis; end; theorem x, y are_orthogonal implies -x, y are_orthogonal proof assume x, y are_orthogonal; then - x .|. y = - 0; then (-x) .|. y = 0 by Th8; hence thesis; end; theorem x, y are_orthogonal implies -x, -y are_orthogonal by Th10; theorem x, 0.X are_orthogonal by Th14; theorem x, y are_orthogonal implies (x + y) .|. (x + y) = x .|. x + y .|. y proof assume x, y are_orthogonal; then A1: x .|. y = 0; (x + y) .|. (x + y) = x .|. x + 2 * x .|. y + y .|. y by Th16; hence thesis by A1; end; theorem x, y are_orthogonal implies (x - y) .|. (x - y) = x .|. x + y .|. y proof assume x, y are_orthogonal; then A1: x .|. y = 0; (x - y) .|. (x - y) = x .|. x - 2 * x .|. y + y .|. y by Th18 .= x .|. x + y .|. y - 0 by A1; hence thesis; end; definition let X, x; func ||.x.|| -> Real equals sqrt (x .|. x); correctness; end; theorem Th26: ||.x.|| = 0 iff x = 0.X proof thus ||.x.|| = 0 implies x = 09(X) proof assume A1: ||.x.|| = 0; 0 <= x .|. x by Def2; then x .|. x = 0 by A1,SQUARE_1:24; hence thesis by Def2; end; assume x = 09(X); hence thesis by Def2,SQUARE_1:17; end; theorem Th27: ||.a * x.|| = |.a.| * ||.x.|| proof A1: 0 <= a^2 & 0 <= x .|. x by Def2,XREAL_1:63; ||.a * x.|| = sqrt (a * (x .|. (a * x))) by Def2 .= sqrt (a * (a * (x .|. x))) by Def2 .= sqrt (a^2 * (x .|. x)) .= sqrt (a^2) * sqrt (x .|. x) by A1,SQUARE_1:29 .= |.a.| * sqrt (x .|. x) by COMPLEX1:72; hence thesis; end; theorem Th28: 0 <= ||.x.|| proof 0 <= x .|. x by Def2; hence thesis by SQUARE_1:def 2; end; theorem |.x .|. y.| <= ||.x.|| * ||.y.|| by Th19; theorem Th30: ||.x + y.|| <= ||.x.|| + ||.y.|| proof A1: sqrt ||.x + y.||^2 = sqrt ((x + y) .|. (x + y)) by Th28,SQUARE_1:22; (x + y) .|. (x + y) >= 0 & ||.x + y.||^2 >= 0 by Def2,XREAL_1:63; then ||.x + y.||^2 = (x + y) .|. (x + y) by A1,SQUARE_1:28; then A2: ||.x + y.||^2 = x .|. x + 2 * x .|. y + y .|. y by Th16; x .|. x >= 0 by Def2; then A3: ||.x + y.||^2 = (sqrt (x .|. x))^2 + 2 * x .|. y + y .|. y by A2, SQUARE_1:def 2; A4: ||.x.|| >= 0 & ||.y.|| >= 0 by Th28; |.x .|. y.| <= ||.x.|| * ||.y.|| & x .|. y <= |.x .|. y.| by Th19, ABSVALUE:4; then x .|. y <= ||.x.|| * ||.y.|| by XXREAL_0:2; then 2 * x .|. y <= 2 * (||.x.|| * ||.y.||) by XREAL_1:64; then ||.x.||^2 + 2 * x .|. y <= ||.x.||^2 + 2 * ||.x.|| * ||.y.|| by XREAL_1:7; then A5: ||.x.||^2 + 2 * x .|. y + ||.y.||^2 <= ||.x.||^2 + 2 * ||.x.|| * ||.y .|| + ||.y.||^2 by XREAL_1:6; y .|. y >= 0 by Def2; then ||.x + y.||^2 <= (||.x.|| + ||.y.||)^2 by A3,A5,SQUARE_1:def 2; hence thesis by A4,SQUARE_1:16; end; theorem Th31: ||.-x.|| = ||.x.|| proof A1: |.-1.| = -(-1) by ABSVALUE:def 1; ||.-x.|| = ||.(-1) * x.|| by RLVECT_1:16 .= 1 * ||.x.|| by A1,Th27; hence thesis; end; theorem Th32: ||.x.|| - ||.y.|| <= ||.x - y.|| proof (x - y) + y = x - (y - y) by RLVECT_1:29 .= x - 09(X) by RLVECT_1:15 .= x by RLVECT_1:13; then ||.x.|| <= ||.x - y.|| + ||.y.|| by Th30; hence thesis by XREAL_1:20; end; theorem |.||.x.|| - ||.y.||.| <= ||.x - y.|| proof (y - x) + x = y - (x - x) by RLVECT_1:29 .= y - 09(X) by RLVECT_1:15 .= y by RLVECT_1:13; then ||.y.|| <= ||.y - x.|| + ||.x.|| by Th30; then ||.y.|| - ||.x.|| <= ||.y - x.|| by XREAL_1:20; then ||.y.|| - ||.x.|| <= ||.-(x - y).|| by RLVECT_1:33; then ||.y.|| - ||.x.|| <= ||.x - y.|| by Th31; then A1: -||.x - y.|| <= -(||.y.|| - ||.x.||) by XREAL_1:24; ||.x.|| - ||.y.|| <= ||.x - y.|| by Th32; hence thesis by A1,ABSVALUE:5; end; definition let X, x, y; func dist(x,y) -> Real equals ||.x - y.||; correctness; commutativity proof let IT be Real; let x,y; ||.x - y.|| = ||.-(y-x).|| by RLVECT_1:33 .= ||.y - x.|| by Th31; hence thesis; end; end; theorem Th34: dist(x,x) = 0 proof thus dist(x,x) = ||.09(X).|| by RLVECT_1:15 .= 0 by Th26; end; theorem dist(x,z) <= dist(x,y) + dist(y,z) proof dist(x,z) = ||.(x-z)+09(X).|| by RLVECT_1:4 .= ||.(x-z)+(y-y).|| by RLVECT_1:15 .= ||.x-(z-(y-y)).|| by RLVECT_1:29 .= ||.x-(y+(z-y)).|| by RLVECT_1:29 .= ||.(x-y)-(z-y).|| by RLVECT_1:27 .= ||.(x-y)+(y-z).|| by RLVECT_1:33; hence thesis by Th30; end; theorem Th36: x <> y iff dist(x,y) <> 0 proof thus x <> y implies dist(x,y) <> 0 proof assume that A1: x <> y and A2: dist(x,y) = 0; x - y = 09(X) by A2,Th26; hence contradiction by A1,RLVECT_1:21; end; thus thesis by Th34; end; theorem dist(x,y) >= 0 by Th28; theorem x <> y iff dist(x,y) > 0 proof thus x <> y implies dist(x,y) > 0 proof assume x <> y; then dist(x,y) <> 0 by Th36; hence thesis by Th28; end; thus thesis by Th34; end; theorem dist(x,y) = sqrt ((x-y) .|. (x-y)); theorem dist(x + y,u + v) <= dist(x,u) + dist(y,v) proof dist(x + y,u + v) = ||.((-u) + (-v)) + (x + y).|| by RLVECT_1:31 .= ||.x + ((-u) + (-v)) + y.|| by RLVECT_1:def 3 .= ||.x - u + (-v) + y.|| by RLVECT_1:def 3 .= ||.x - u + (y - v).|| by RLVECT_1:def 3; hence thesis by Th30; end; theorem dist(x - y,u - v) <= dist(x,u) + dist(y,v) proof dist(x - y,u - v) = ||.((x - y) - u) + v.|| by RLVECT_1:29 .= ||.(x - (u + y)) + v.|| by RLVECT_1:27 .= ||.((x - u) - y) + v.|| by RLVECT_1:27 .= ||.(x - u) - (y - v).|| by RLVECT_1:29 .= ||.(x - u) + -(y - v).||; then dist(x - y,u - v) <= ||.x - u.|| + ||.-(y - v).|| by Th30; hence thesis by Th31; end; theorem dist(x - z, y - z) = dist(x,y) proof thus dist(x - z,y - z) = ||.((x - z) - y) + z.|| by RLVECT_1:29 .= ||.(x - (y + z)) + z.|| by RLVECT_1:27 .= ||.((x - y) - z) + z.|| by RLVECT_1:27 .= ||.(x - y) - (z - z).|| by RLVECT_1:29 .= ||.(x - y) - 09(X).|| by RLVECT_1:15 .= dist(x,y) by RLVECT_1:13; end; theorem dist(x - z,y - z) <= dist(z,x) + dist(z,y) proof dist(x - z,y - z) = ||.(x - z) + (z - y).|| by RLVECT_1:33 .= ||.-(z - x) + (z - y).|| by RLVECT_1:33; then dist(x - z,y - z) <= ||.-(z - x).|| + ||.z - y.|| by Th30; hence thesis by Th31; end; reserve seq, seq1, seq2, seq3 for sequence of X; reserve n for Nat; definition let X be non empty addLoopStr; let seq be sequence of X; let x be Point of X; func seq + x -> sequence of X means :Def6: for n holds it.n = seq.n + x; existence proof deffunc F(Nat) = seq.$1 + x; consider seq be sequence of X such that A1: for n being Element of NAT holds seq.n = F(n) from FUNCT_2:sch 4; take seq; let n; n in NAT by ORDINAL1:def 12; hence thesis by A1; end; uniqueness proof let seq1, seq2 be sequence of X; assume that A2: for n holds seq1.n = seq.n + x and A3: for n holds seq2.n = seq.n + x; let n be Element of NAT; seq1.n = seq.n + x by A2; hence thesis by A3; end; end; theorem Th44: for X being non empty addLoopStr, seq being sequence of X holds (-seq).n = - seq.n proof let X be non empty addLoopStr, seq be sequence of X; A1: dom -seq = NAT by FUNCT_2:def 1; A2: dom seq = NAT by FUNCT_2:def 1; A3: n in NAT by ORDINAL1:def 12; hence (-seq).n = (-seq)/.n by PARTFUN1:def 6,A1 .= -seq/.n by A1,VFUNCT_1:def 5,A3 .= - seq.n by A3,PARTFUN1:def 6,A2; end; definition let X, seq1, seq2; redefine func seq1 + seq2; commutativity proof let seq1, seq2; let n be Element of NAT; thus (seq1 + seq2).n = seq2.n + seq1.n by NORMSP_1:def 2 .= (seq2 + seq1).n by NORMSP_1:def 2; end; end; theorem seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3 proof let n be Element of NAT; thus (seq1 + (seq2 + seq3)).n = seq1.n + (seq2 + seq3).n by NORMSP_1:def 2 .= seq1.n + (seq2.n + seq3.n) by NORMSP_1:def 2 .= (seq1.n + seq2.n) + seq3.n by RLVECT_1:def 3 .= (seq1 + seq2).n + seq3.n by NORMSP_1:def 2 .= ((seq1 + seq2) + seq3).n by NORMSP_1:def 2; end; theorem seq1 is constant & seq2 is constant implies seq1 + seq2 is constant proof assume that A1: seq1 is constant and A2: seq2 is constant; set seq = seq1 + seq2; consider x such that A3: for n being Nat holds seq1.n = x by A1; consider y such that A4: for n being Nat holds seq2.n = y by A2; take z = x + y; let n be Nat; thus seq.n = seq1.n + seq2.n by NORMSP_1:def 2 .= x + seq2.n by A3 .= z by A4; end; theorem seq1 is constant & seq2 is constant implies seq1 - seq2 is constant proof assume that A1: seq1 is constant and A2: seq2 is constant; set seq = seq1 - seq2; consider x such that A3: for n being Nat holds seq1.n = x by A1; consider y such that A4: for n being Nat holds seq2.n = y by A2; take z = x - y; let n be Nat; thus seq.n = seq1.n - seq2.n by NORMSP_1:def 3 .= x - seq2.n by A3 .= z by A4; end; theorem seq1 is constant implies a * seq1 is constant proof assume A1: seq1 is constant; set seq = a * seq1; consider x such that A2: for n being Nat holds seq1.n = x by A1; take z = a * x; let n be Nat; thus seq.n = a * seq1.n by NORMSP_1:def 5 .= z by A2; end; theorem seq1 - seq2 = seq1 + -seq2 proof let n be Element of NAT; thus (seq1 - seq2).n = seq1.n - seq2.n by NORMSP_1:def 3 .= seq1.n + (-seq2).n by Th44 .= (seq1 + -seq2).n by NORMSP_1:def 2; end; theorem seq = seq + 0.X proof let n be Element of NAT; thus (seq + 09(X)).n = seq.n + 09(X) by Def6 .= seq.n by RLVECT_1:4; end; theorem a * (seq1 + seq2) = a * seq1 + a * seq2 proof let n be Element of NAT; thus (a * (seq1 + seq2)).n = a * (seq1 + seq2).n by NORMSP_1:def 5 .= a * (seq1.n + seq2.n) by NORMSP_1:def 2 .= a * seq1.n + a * seq2.n by RLVECT_1:def 5 .= (a * seq1).n + a * seq2.n by NORMSP_1:def 5 .= (a * seq1).n + (a * seq2).n by NORMSP_1:def 5 .= (a * seq1 + a * seq2).n by NORMSP_1:def 2; end; theorem (a + b) * seq = a * seq + b * seq proof let n be Element of NAT; thus ((a + b) * seq).n = (a + b) * seq.n by NORMSP_1:def 5 .= a * seq.n + b * seq.n by RLVECT_1:def 6 .= (a * seq).n + b * seq.n by NORMSP_1:def 5 .= (a * seq).n + (b * seq).n by NORMSP_1:def 5 .= (a * seq + b * seq).n by NORMSP_1:def 2; end; theorem (a * b) * seq = a * (b * seq) proof let n be Element of NAT; thus ((a * b) * seq).n = (a * b) * seq.n by NORMSP_1:def 5 .= a * (b * seq.n) by RLVECT_1:def 7 .= a * (b * seq).n by NORMSP_1:def 5 .= (a * (b * seq)).n by NORMSP_1:def 5; end; theorem (1 qua Real) * seq = seq proof let n be Element of NAT; thus (1 * seq).n = 1 * seq.n by NORMSP_1:def 5 .= seq.n by RLVECT_1:def 8; end; theorem (-1) * seq = - seq proof let n be Element of NAT; thus ((-1) * seq).n = (-1) * seq.n by NORMSP_1:def 5 .= - seq.n by RLVECT_1:16 .= (-seq).n by Th44; end; theorem seq - x = seq + -x proof let n be Element of NAT; thus (seq - x).n = seq.n - x by NORMSP_1:def 4 .= (seq + -x).n by Def6; end; theorem seq1 - seq2 = - (seq2 - seq1) proof let n be Element of NAT; thus (seq1 - seq2).n = seq1.n - seq2.n by NORMSP_1:def 3 .= - (seq2.n - seq1.n) by RLVECT_1:33 .= - (seq2 - seq1).n by NORMSP_1:def 3 .= (- (seq2 - seq1)).n by Th44; end; theorem seq = seq - 0.X proof let n be Element of NAT; thus (seq - 09(X)).n = seq.n - 09(X) by NORMSP_1:def 4 .= seq.n by RLVECT_1:13; end; theorem seq = - ( - seq ) proof let n be Element of NAT; thus (- ( - seq )).n = - (- seq).n by Th44 .= - ( - seq.n) by Th44 .= seq.n by RLVECT_1:17; end; theorem seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 proof let n be Element of NAT; thus (seq1 - (seq2 + seq3)).n = seq1.n - (seq2 + seq3).n by NORMSP_1:def 3 .= seq1.n - (seq2.n + seq3.n) by NORMSP_1:def 2 .= (seq1.n - seq2.n) - seq3.n by RLVECT_1:27 .= (seq1 - seq2).n - seq3.n by NORMSP_1:def 3 .= ((seq1 - seq2) - seq3).n by NORMSP_1:def 3; end; theorem (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3) proof let n be Element of NAT; thus ((seq1 + seq2) - seq3).n = (seq1 + seq2).n - seq3.n by NORMSP_1:def 3 .= (seq1.n + seq2.n) - seq3.n by NORMSP_1:def 2 .= seq1.n + (seq2.n - seq3.n) by RLVECT_1:def 3 .= seq1.n + (seq2 - seq3).n by NORMSP_1:def 3 .= (seq1 + (seq2 - seq3)).n by NORMSP_1:def 2; end; theorem seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 proof let n be Element of NAT; thus (seq1 - (seq2 - seq3)).n = seq1.n - (seq2 - seq3).n by NORMSP_1:def 3 .= seq1.n - (seq2.n - seq3.n) by NORMSP_1:def 3 .= (seq1.n - seq2.n) + seq3.n by RLVECT_1:29 .= (seq1 - seq2).n + seq3.n by NORMSP_1:def 3 .= ((seq1 - seq2) + seq3).n by NORMSP_1:def 2; end; theorem a * (seq1 - seq2) = a * seq1 - a * seq2 proof let n be Element of NAT; thus (a * (seq1 - seq2)).n = a * (seq1 - seq2).n by NORMSP_1:def 5 .= a * (seq1.n - seq2.n) by NORMSP_1:def 3 .= a * seq1.n - a * seq2.n by RLVECT_1:34 .= (a * seq1).n - a * seq2.n by NORMSP_1:def 5 .= (a * seq1).n - (a * seq2).n by NORMSP_1:def 5 .= (a * seq1 - a * seq2).n by NORMSP_1:def 3; end;