:: Introduction to Banach and Hilbert spaces - Part I
:: by Jan Popio{\l}ek
::
:: Received July 19, 1991
:: Copyright (c) 1991-2026 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; :: redefines .|. (BHSP_1, definition)
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; :: redefines + (NORMSP_1, definition)
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;