Copyright (c) 2003 Association of Mizar Users
environ
vocabulary PRE_TOPC, ARYTM, FUNCT_1, FINSEQ_1, EUCLID, SQUARE_1, RLVECT_1,
RVSUM_1, FINSEQ_2, ARYTM_1, RELAT_1, ARYTM_3, COMPLEX1, ABSVALUE,
FUNCT_3, EUCLID_2, BHSP_1;
notation SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
ABSVALUE, FINSEQ_1, FINSEQ_2, QUIN_1, PRE_TOPC, TOPRNS_1, RVSUM_1,
EUCLID, SQUARE_1;
constructors REAL_1, ABSVALUE, FINSEQOP, TOPRNS_1, SEQ_1, QUIN_1, SQUARE_1,
MEMBERED;
clusters FINSEQ_2, XREAL_0, NAT_1, RELSET_1, SEQ_1, QUIN_1, SQUARE_1,
MEMBERED;
requirements REAL, SUBSET, NUMERALS, ARITHM;
theorems EUCLID, RVSUM_1, REAL_1, REAL_2, FINSEQ_2, AXIOMS, XREAL_0, FINSEQ_1,
FINSEQ_3, SQUARE_1, JGRAPH_1, QUIN_1, ABSVALUE, TOPRNS_1, JORDAN2C,
XCMPLX_0, XCMPLX_1;
begin :: Preliminaries
reserve i, n, j for Nat,
x, y, a for real number,
v for Element of n-tuples_on REAL,
p, p1, p2, p3, q, q1, q2 for Point of TOP-REAL n;
theorem Th1:
for i holds i in Seg n implies mlt(v, 0*n).i = 0
proof let i;
assume
A1: i in Seg n;
A2: 0*n = n |-> (0 qua set) by EUCLID:def 4;
then A3: len 0*n = n by FINSEQ_2:69;
set v1 = v.i, v0 = (0*n).i;
A4: v0=0 by A1,A2,FINSEQ_2:70;
reconsider z = 0*n as Element of n-tuples_on REAL by A3,FINSEQ_2:110;
mlt(v, z).i = v1 * v0 by RVSUM_1:87
.= 0 by A4;
hence thesis;
end;
theorem Th2:
mlt(v, 0*n) = 0*n
proof
0*n = n |-> (0 qua set) by EUCLID:def 4;
then len 0*n = n by FINSEQ_2:69;
then reconsider z= 0*n as Element of n-tuples_on REAL by FINSEQ_2:110;
A1: len mlt(v, z) = n by FINSEQ_2:109;
0*n = n |-> (0 qua set) by EUCLID:def 4;
then A2: len 0*n = n by FINSEQ_2:69;
then A3: dom mlt(v, 0*n) = dom 0*n by A1,FINSEQ_3:31;
A4: dom 0*n = Seg n by A2,FINSEQ_1:def 3;
for j st j in dom 0*n holds mlt(v,0*n).j=(0*n).j
proof
let j;
assume A5: j in dom 0*n;
hence mlt(v,0*n).j = 0 by A4,Th1
.= (n |-> 0).j by A4,A5,FINSEQ_2:70
.= (0*n).j by EUCLID:def 4;
end;
hence thesis by A3,FINSEQ_1:17;
end;
theorem Th3:
for x being FinSequence of REAL holds (-1)*x = -x
proof let x be FinSequence of REAL;
reconsider z = x as Element of REAL len x by JORDAN2C:52;
reconsider w = z as Element of (len x)-tuples_on REAL by EUCLID:def 1;
-w=(-1)*w by RVSUM_1:76;
hence thesis;
end;
theorem Th4:
for x,y being FinSequence of REAL st len x=len y holds x-y=x+(-y)
proof let x,y be FinSequence of REAL;
assume len x=len y;
then reconsider z = x, z2 = y as Element of REAL len x by JORDAN2C:52;
set n=len x;
reconsider w = z, u = z2 as Element of n-tuples_on REAL by EUCLID:def 1;
w-u=w+(-u) by RVSUM_1:52;
hence thesis;
end;
theorem Th5:
for x being FinSequence of REAL holds len (-x)=len x
proof let x be FinSequence of REAL;
dom (-x)=dom x by RVSUM_1:34;
then Seg len(-x)=dom x by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th6:
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
len (x1+x2)=len x1
proof let x1,x2 be FinSequence of REAL;
assume A1: len x1=len x2;
set n=len x1;
reconsider z1=x1 as Element of (len x1)-tuples_on REAL by FINSEQ_2:110;
reconsider z2=x2 as Element of n-tuples_on REAL by A1,FINSEQ_2:110;
dom (z1+z2)=Seg n by FINSEQ_2:144;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th7:
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
len (x1-x2)=len x1
proof let x1,x2 be FinSequence of REAL;
assume A1: len x1=len x2;
set n=len x1;
reconsider z1=x1 as Element of (len x1)-tuples_on REAL by FINSEQ_2:110;
reconsider z2=x2 as Element of n-tuples_on REAL by A1,FINSEQ_2:110;
dom (z1-z2)=Seg n by FINSEQ_2:144;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th8:
for a being real number, x being FinSequence of REAL holds len (a*x)=len x
proof let a be real number, x be FinSequence of REAL;
set n=len x;
reconsider z=x as Element of n-tuples_on REAL by FINSEQ_2:110;
len (a*z)=n by FINSEQ_2:109;
hence thesis;
end;
theorem Th9:
for x,y,z being FinSequence of REAL st len x=len y & len y=len z holds
mlt(x+y,z) = mlt(x,z)+mlt(y,z)
proof let x,y,z be FinSequence of REAL;
assume len x=len y & len y=len z;
then reconsider x2=x, y2=y, z2=z as Element of (len x)-tuples_on REAL
by FINSEQ_2:110;
A1: dom (mlt(x+y,z))=Seg len(mlt(x2+y2,z2)) by FINSEQ_1:def 3
.=Seg len x by FINSEQ_2:109
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_2:109
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
A2: dom (mlt(x,z))=Seg len(mlt(x2,z2)) by FINSEQ_1:def 3
.=Seg len x by FINSEQ_2:109
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_2:109
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
A3: dom (mlt(y,z))=Seg len(mlt(y2,z2)) by FINSEQ_1:def 3
.=Seg len x by FINSEQ_2:109
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_2:109
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
for i being Nat st i in dom (mlt(x+y,z)) holds
mlt(x+y,z).i=(mlt(x,z)+mlt(y,z)).i
proof let i be Nat;
assume A4: i in dom mlt(x+y,z);
len (x2+y2)=len x by FINSEQ_2:109;
then A5: dom (x2+y2)=Seg len x by FINSEQ_1:def 3
.=Seg len(mlt(x2,z2)) by FINSEQ_2:109
.=dom (mlt(x,z)) by FINSEQ_1:def 3;
set a=x.i, b=y.i, d=(x+y).i, e=z.i;
A6: d=a+b by A1,A2,A4,A5,RVSUM_1:26;
thus mlt(x+y,z).i=d*e by A4,RVSUM_1:86
.=a*e+b*e by A6,XCMPLX_1:8
.=mlt(x,z).i +b*e by A1,A2,A4,RVSUM_1:86
.=mlt(x,z).i +mlt(y,z).i by A1,A3,A4,RVSUM_1:86
.=(mlt(x,z)+mlt(y,z)).i by A1,A4,RVSUM_1:26;
end;
hence thesis by A1,FINSEQ_1:17;
end;
begin :: Inner Product of Finite Sequences
definition let x1,x2 be FinSequence of REAL;
func |( x1,x2 )| -> real number equals :Def1:
Sum mlt(x1,x2);
correctness;
commutativity;
end;
theorem Th10:
for y1,y2 being FinSequence of REAL, x1,x2 being Element of REAL n st
x1=y1 & x2=y2 holds |(y1,y2)|=1/4*((|.(x1+x2).|)^2-(|.(x1-x2).|)^2)
proof let y1,y2 be FinSequence of REAL,x1,x2 be Element of REAL n;
assume A1: x1=y1 & x2=y2;
set z1=x1+x2, z2=x1-x2;
A2: 1/4*((|.(x1+x2).|)^2-(|.(x1-x2).|)^2)
=1/4*((sqrt Sum sqr (z1))^2-(|.(z2).|)^2) by EUCLID:def 5
.=1/4*((sqrt Sum sqr (z1))^2-(sqrt Sum sqr (z2))^2) by EUCLID:def 5;
Sum sqr (x1+x2)>=0 by RVSUM_1:116;
then A3: (sqrt Sum sqr (x1+x2))^2 =Sum sqr (x1+x2) by SQUARE_1:def 4;
Sum sqr (x1-x2)>=0 by RVSUM_1:116;
then A4: (sqrt Sum sqr (x1-x2))^2=Sum sqr (x1-x2) by SQUARE_1:def 4;
set v1=sqr (x1+x2), v2=sqr (x1-x2);
reconsider w1=x1, w2=x2 as Element of n-tuples_on REAL by EUCLID:def 1;
A5: Sum sqr (x1+x2)-Sum sqr (x1-x2)=Sum (v1 - v2) by RVSUM_1:120;
v1-v2=sqr w1 + 2*mlt(w1,w2) + sqr w2 -sqr (w1-w2) by RVSUM_1:98
.=sqr w1 + 2*mlt(w1,w2) + sqr w2
-(sqr w1 - 2*mlt(w1,w2) + sqr w2) by RVSUM_1:99
.= 2*mlt(w1,w2) +sqr w2+ sqr w1
-(sqr w1 - 2*mlt(w1,w2) + sqr w2) by RVSUM_1:32
.= 2*mlt(w1,w2) +sqr w2+ sqr w1
-(sqr w1 - 2*mlt(w1,w2))- sqr w2 by RVSUM_1:60
.= 2*mlt(w1,w2) +sqr w2+ sqr w1
- sqr w1 + 2*mlt(w1,w2)- sqr w2 by RVSUM_1:62
.= 2*mlt(w1,w2) +sqr w2+ 2*mlt(w1,w2)- sqr w2 by RVSUM_1:63
.= 2*mlt(w1,w2)+2*mlt(w1,w2) +sqr w2 - sqr w2 by RVSUM_1:32
.= 2*mlt(w1,w2)+2*mlt(w1,w2) by RVSUM_1:63
.= (2+2)*mlt(w1,w2) by RVSUM_1:72
.= 4*mlt(w1,w2);
then 1/4*((|.(x1+x2).|)^2-(|.(x1-x2).|)^2)
= 1/4*(4*Sum(mlt(w1,w2))) by A2,A3,A4,A5,RVSUM_1:117
.= 1/4*4*Sum(mlt(w1,w2)) by XCMPLX_1:4
.= Sum(mlt(w1,w2));
hence thesis by A1,Def1;
end;
theorem Th11:
for x being FinSequence of REAL holds |(x,x)| >= 0
proof let x be FinSequence of REAL;
reconsider z = x as Element of REAL len x by JORDAN2C:52;
set n=len x;
reconsider w = z as Element of n-tuples_on REAL by EUCLID:def 1;
|(x, x)| = Sum mlt(x, x) by Def1
.= Sum sqr(w) by RVSUM_1:97;
hence thesis by RVSUM_1:116;
end;
theorem Th12:
for x being FinSequence of REAL holds (|.x.|)^2=|(x,x)|
proof let x be FinSequence of REAL;
reconsider z=x as Element of (len x)-tuples_on REAL by FINSEQ_2:110;
A1: |(x,x)| = Sum mlt(x, x) by Def1
.= Sum sqr z by RVSUM_1:97
.= Sum sqr x;
A2: 0 <= |(x,x)| by Th11;
|.x.|^2 = (sqrt Sum sqr x)^2 by EUCLID:def 5
.= |(x,x)| by A1,A2,SQUARE_1:def 4;
hence thesis;
end;
theorem Th13:
for x being FinSequence of REAL holds |.x.| = sqrt |(x,x)|
proof let x be FinSequence of REAL;
set n=len x;
reconsider z=x as Element of (len x)-tuples_on REAL by FINSEQ_2:110;
reconsider y=z as Element of REAL n by EUCLID:def 1;
0 <= |.y.| by EUCLID:12;
then |.x.| = sqrt |.x.|^2 by SQUARE_1:89
.= sqrt |(x,x)| by Th12;
hence thesis;
end;
theorem Th14:
for x being FinSequence of REAL holds 0 <= |.x.|
proof let x be FinSequence of REAL;
A1: |.x.| = sqrt |(x,x)| by Th13;
0 <= |(x,x)| by Th11;
hence thesis by A1,SQUARE_1:def 4;
end;
theorem Th15:
for x being FinSequence of REAL holds |(x,x)|=0 iff x=0*(len x)
proof let x be FinSequence of REAL;
thus |(x,x)|=0 implies x=0*(len x)
proof assume |(x,x)|=0; then |.x.|^2=0 by Th12;
then A1: |.x.|=0 by SQUARE_1:73;
reconsider y=x as Element of REAL len x by JORDAN2C:52;
y=0*(len x) by A1,EUCLID:11;
hence thesis;
end;
assume x=0*(len x);
then |.x.|=0 by EUCLID:10;
hence |(x,x)|=0 by Th12,SQUARE_1:60;
end;
theorem
for x being FinSequence of REAL holds |(x,x)| = 0 iff |.x.| = 0
proof let x be FinSequence of REAL;
|(x,x)| = 0 implies |.x.| = 0
proof
assume |(x,x)| = 0;
then x=0*(len x) by Th15;
hence |.x.| = 0 by EUCLID:10;
end;
hence thesis by Th12,SQUARE_1:60;
end;
theorem Th17:
for x being FinSequence of REAL holds |(x, 0*(len x))| = 0
proof let x be FinSequence of REAL;
set n=len x;
reconsider p1=x as Element of n-tuples_on REAL by FINSEQ_2:110;
A1: 0*n = n |-> 0 by EUCLID:def 4;
|(x, 0*n)| = Sum mlt(p1,0*n) by Def1
.= Sum 0*n by Th2
.= 0 by A1,RVSUM_1:111;
hence thesis;
end;
theorem
for x being FinSequence of REAL holds |(0*(len x),x)| = 0 by Th17;
theorem Th19:
for x,y,z being FinSequence of REAL st len x=len y & len y=len z holds
|((x+y),z)| = |(x,z)| + |(y,z)|
proof let x,y,z be FinSequence of REAL;
assume A1: len x=len y & len y=len z;
then reconsider x2=x,y2=y,z2=z as Element of (len x)-tuples_on REAL
by FINSEQ_2:110;
|((x+y),z)|= Sum mlt(x+y,z) by Def1
.= Sum(mlt(x,z)+mlt(y,z)) by A1,Th9
.= Sum(mlt(x2,z2))+Sum(mlt(y2,z2)) by RVSUM_1:119
.= |(x,z)| + Sum(mlt(y,z)) by Def1
.= |(x,z)| + |(y,z)| by Def1;
hence thesis;
end;
theorem Th20:
for x,y being FinSequence of REAL,a being real number st
len x=len y holds |(a*x,y)| = a*|(x,y)|
proof let x,y be FinSequence of REAL,a be real number;
assume len x=len y;
then reconsider x2=x, y2 = y as Element of (len x)-tuples_on REAL
by FINSEQ_2:110;
reconsider a2=a as Element of REAL by XREAL_0:def 1;
|(a*x,y)| =Sum(mlt(a*x,y)) by Def1
.=Sum(a2*mlt(x2,y2)) by RVSUM_1:94
.=a2*Sum(mlt(x,y)) by RVSUM_1:117
.=a*|(x,y)| by Def1;
hence thesis;
end;
theorem Th21:
for x,y being FinSequence of REAL,a being real number st
len x=len y holds |(x,a*y)| = a*|(x,y)|
proof let x,y be FinSequence of REAL,a be real number;
assume len x=len y;
then reconsider x2=x, y2=y as Element of (len x)-tuples_on REAL by FINSEQ_2:
110;
reconsider a2=a as Element of REAL by XREAL_0:def 1;
|(x,a*y)| =Sum(mlt(x,a*y)) by Def1
.=Sum(a2*mlt(y2,x2)) by RVSUM_1:94
.=a2*Sum(mlt(x,y)) by RVSUM_1:117
.=a*|(x,y)| by Def1;
hence thesis;
end;
theorem Th22:
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
|(-x1, x2)| = -|(x1, x2)|
proof let x1,x2 be FinSequence of REAL;
assume A1: len x1=len x2;
|(-x1, x2)| = |((-1)*x1, x2)| by Th3
.= (-1)*|(x1, x2)| by A1,Th20;
hence thesis by XCMPLX_1:180;
end;
theorem
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
|(x1, -x2)| = -|(x1, x2)| by Th22;
theorem
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
|(-x1, -x2)| = |(x1, x2)|
proof let x1,x2 be FinSequence of REAL;
assume A1: len x1=len x2;
then len (-x2)=len x1 by Th5;
then |(-x1, -x2)| = -|(x1, -x2)| by Th22
.= --|(x1, x2)| by A1,Th22;
hence thesis;
end;
theorem Th25:
for x1,x2,x3 being FinSequence of REAL st len x1=len x2 & len x2=len x3
holds |(x1-x2, x3)| = |(x1, x3)| - |(x2, x3)|
proof let x1,x2,x3 be FinSequence of REAL;
assume A1: len x1=len x2 & len x2=len x3;
A2: len (-x2)=len x2 by Th5;
|(x1 - x2, x3)| = |(x1 + -x2, x3)| by A1,Th4
.= |(x1, x3)| + |(-x2, x3)| by A1,A2,Th19
.= |(x1, x3)| + - |(x2, x3)| by A1,Th22;
hence thesis by XCMPLX_0:def 8;
end;
theorem
for x,y being real number,x1,x2,x3 being FinSequence of REAL st
len x1=len x2 & len x2=len x3 holds
|((x*x1+y*x2), x3)| = x*|(x1,x3)| + y*|(x2,x3)|
proof let x,y be real number,x1,x2,x3 be FinSequence of REAL;
assume A1: len x1=len x2 & len x2=len x3;
A2: len (x*x1)=len x1 by Th8;
len (y*x2)=len x2 by Th8;
then |(x*x1 + y*x2, x3)| = |(x*x1, x3)| + |(y*x2, x3)| by A1,A2,Th19
.= x*|(x1,x3)| + |(y*x2,x3)| by A1,Th20
.= x*|(x1,x3)| + y*|(x2,x3)| by A1,Th20;
hence thesis;
end;
theorem
for x,y1,y2 being FinSequence of REAL st len x=len y1 & len y1=len y2 holds
|(x, y1+y2)| = |(x, y1)| + |(x, y2)| by Th19;
theorem
for x,y1,y2 being FinSequence of REAL st len x=len y1 & len y1=len y2 holds
|(x, y1-y2)| = |(x, y1)| - |(x, y2)| by Th25;
theorem Th29:
for x1,x2,y1,y2 being FinSequence of REAL st
len x1=len x2 & len x2=len y1 & len y1=len y2 holds
|(x1+x2, y1+y2)| = |(x1, y1)| + |(x1, y2)| + |(x2, y1)| + |(x2, y2)|
proof let x1,x2,y1,y2 be FinSequence of REAL;
assume A1: len x1=len x2 & len x2=len y1 & len y1=len y2;
then |(x1+x2, y2)| = |(x1, y2)| + |(x2, y2)| by Th19;
then A2: |(x1+x2, y1)| +|(x1+x2, y2)| = (|(x1, y1)|+|(x2, y1)|) +
(|(x1, y2)| + |(x2, y2)|) by A1,Th19;
len (x1+x2)=len x1 by A1,Th6;
then |(x1+x2, y1+y2)| =|(x1+x2, y1)| +|(x1+x2, y2)| by A1,Th19
.= |(x1, y1)|+|(x2, y1)|+(|(x1, y2)|+0)+|(x2, y2)| by A2,XCMPLX_1:1
.= |(x1, y1)|+|(x1, y2)|+|(x2, y1)|+|(x2, y2)| by XCMPLX_1:1;
hence thesis;
end;
theorem Th30:
for x1,x2,y1,y2 being FinSequence of REAL st
len x1=len x2 & len x2=len y1 & len y1=len y2 holds
|(x1-x2, y1-y2)| = |(x1, y1)| - |(x1, y2)| - |(x2, y1)| + |(x2, y2)|
proof let x1,x2,y1,y2 be FinSequence of REAL;
assume A1: len x1=len x2 & len x2=len y1 & len y1=len y2;
then |(x1,y1-y2)| = |(x1,y1)| - |(x1,y2)| by Th25;
then A2: |(x1,y1-y2)| - |(x2,y1-y2)|
= (|(x1,y1)|-|(x1,y2)|)-(|(x2,y1)|-|(x2,y2)|) by A1,Th25;
len (y1 - y2)=len y1 by A1,Th7;
then |(x1-x2, y1-y2)| = |(x1, y1-y2)| - |(x2, y1-y2)| by A1,Th25
.= |(x1,y1)|-|(x1,y2)|-|(x2,y1)|+|(x2,y2)| by A2,XCMPLX_1:37;
hence thesis;
end;
theorem Th31:
for x,y being FinSequence of REAL st len x=len y holds
|(x+y, x+y)| = |(x, x)| + 2*|(x, y)| + |(y, y)|
proof let x,y be FinSequence of REAL;
assume A1: len x=len y;
|(x, x)| + |(x, y)| + |(x, y)|
= |(x, x)| + (|(x, y)|+ |(x, y)|) by XCMPLX_1:1
.= |(x, x)| + 2*|(x, y)| by XCMPLX_1:11;
hence thesis by A1,Th29;
end;
theorem Th32:
for x,y being FinSequence of REAL st len x=len y holds
|(x-y, x-y)| = |(x, x)| - 2*|(x, y)| + |(y, y)|
proof let x,y be FinSequence of REAL;
assume len x=len y;
then |(x-y, x-y)| = |(x,x)| - |(x,y)| - |(y,x)| + |(y, y)| by Th30
.= |(x,x)| - (|(x,y)|+|(x,y)|) + |(y, y)| by XCMPLX_1:36
.= |(x,x)| - 2*|(x,y)| + |(y, y)| by XCMPLX_1:11;
hence thesis;
end;
theorem Th33:
for x,y being FinSequence of REAL st len x=len y holds
|.x+y.|^2 = |.x.|^2 + 2*|(y, x)| + |.y.|^2
proof let x,y be FinSequence of REAL;
assume A1: len x=len y;
|.x+y.|^2 = |(x+y, x+y)| by Th12
.= |(x, x)| + 2*|(x, y)| + |(y, y)| by A1,Th31
.= |.x.|^2 + 2*|(y, x)| + |(y, y)| by Th12
.= |.x.|^2 + 2*|(y, x)| + |.y.|^2 by Th12;
hence thesis;
end;
theorem Th34:
for x,y being FinSequence of REAL st len x=len y holds
|.x-y.|^2 = |.x.|^2 - 2*|(y, x)| + |.y.|^2
proof let x,y be FinSequence of REAL;
assume A1: len x=len y;
|.x-y.|^2 = |(x-y, x-y)| by Th12
.= |(x, x)| - 2*|(x, y)| + |(y, y)| by A1,Th32
.= |.x.|^2 - 2*|(y, x)| + |(y, y)| by Th12
.= |.x.|^2 - 2*|(y, x)| + |.y.|^2 by Th12;
hence thesis;
end;
theorem
for x,y being FinSequence of REAL st len x=len y holds
|.x+y.|^2 + |.x-y.|^2 = 2*(|.x.|^2 + |.y.|^2)
proof let x,y be FinSequence of REAL;
assume A1: len x=len y;
A2: (|.x.|^2 + 2*|(x, y)| + |.y.|^2)
= (|.x.|^2 + |.y.|^2 + 2*|(x, y)|) by XCMPLX_1:1;
A3: (|.x.|^2 - 2*|(x, y)| + |.y.|^2)
= (|.x.|^2 +(-2*|(x, y)|) + |.y.|^2) by XCMPLX_0:def 8
.= (|.x.|^2 + |.y.|^2 +(-2*|(x, y)|)) by XCMPLX_1:1
.= (|.x.|^2 + |.y.|^2 -2*|(x, y)| ) by XCMPLX_0:def 8;
|.x+y.|^2 + |.x-y.|^2
= (|.x.|^2 + 2*|(y, x)| + |.y.|^2) + |.x-y.|^2 by A1,Th33
.= (|.x.|^2 + 2*|(x, y)| + |.y.|^2) +
(|.x.|^2 - 2*|(y, x)| + |.y.|^2) by A1,Th34
.= (|.x.|^2 + |.y.|^2) + (|.x.|^2 + |.y.|^2) by A2,A3,XCMPLX_1:28
.= 2*(|.x.|^2 + |.y.|^2) by XCMPLX_1:11;
hence thesis;
end;
theorem
for x,y being FinSequence of REAL st len x=len y holds
|.x+y.|^2 - |.x-y.|^2 = 4* |(x,y)|
proof let x,y be FinSequence of REAL;
assume A1: len x=len y;
then |.x+y.|^2 - |.x-y.|^2
= (|.x.|^2 + 2*|(y,x)| + |.y.|^2) - |.x-y.|^2 by Th33
.= (|.x.|^2 + 2*|(x, y)| + |.y.|^2) -
(|.x.|^2 - 2*|(y, x)| + |.y.|^2) by A1,Th34
.= (|.x.|^2 + 2*|(x, y)|) - (|.x.|^2 - 2*|(x, y)|) by XCMPLX_1:32
.= 2*|(x, y)| + 2*|(x, y)| by XCMPLX_1:31
.= 2*(2*|(x, y)|) by XCMPLX_1:11
.= 2* (|(x, y)| + |(x, y)|) by XCMPLX_1:11
.= (|(x, y)| + |(x, y)|) + (|(x, y)| + |(x, y)|) by XCMPLX_1:11
.= (|(x, y)| + |(x, y)| + |(x, y)| + |(x, y)|) by XCMPLX_1:1
.= 4*|(x, y)| by XCMPLX_1:13;
hence thesis;
end;
theorem Th37: :: Schwartz
for x,y being FinSequence of REAL st len x=len y holds
abs |(x,y)| <= |.x.|*|.y.|
proof
let x,y be FinSequence of REAL;
assume A1: len x=len y;
A2: x = 0*(len x) implies abs(|(x,y)|) <= sqrt (|(x,x)|) * sqrt (|(y,y)|)
proof
assume
A3: x = 0*(len x);
then A4: |(x,y)| = 0 by A1,Th17;
|(x,x)|=0 by A3,Th17;
hence thesis by A4,ABSVALUE:7,SQUARE_1:82;
end;
A5: x <> 0*(len x) implies abs(|(x,y)|) <= sqrt (|(x,x)|) * sqrt (|(y,y)|)
proof
assume x <> 0*(len x);
then A6: |(x,x)| <> 0 by Th15;
A7: |(x,x)| >= 0 by Th11;
then A8: |(x,x)| > 0 by A6,REAL_1:def 5;
A9: for t be real number holds
|(x,x)| * t^2 + (2 * (|(x,y)|)) * t + |(y,y)| >= 0
proof
let t be real number;
set s=t^2;
A10: len (t * x)=len x by Th8;
|((t * x + y),(t * x + y))| >= 0 by Th11;
then |((t * x) , (t * x))| + 2 * (|((t*x),y)|) + |(y,y)| >= 0
by A1,A10,Th31;
then t * ( |(t*x,x)|) + 2 * |((t*x),y)| + |(y,y)| >= 0 by A10,Th21;
then t * ( t * |(x,x)|) + 2 * |((t*x),y)| + |(y,y)| >= 0 by A1,Th20;
then (t * t) * |(x,x)| + 2 * |((t*x),y)| + |(y,y)| >= 0
by XCMPLX_1:4;
then |(x,x)| * s + 2 * |((t*x),y)| + |(y,y)| >= 0 by SQUARE_1:def 3;
then |(x,x)| * s + 2 * (|(x,y)| * t) + |(y,y)| >= 0 by A1,Th20;
hence thesis by XCMPLX_1:4;
end;
set w=abs( |(x,y)| ), u=|(x,y)|;
A11: 0 <= w^2 by SQUARE_1:72;
A12: abs(|(x,y)|) >= 0 by ABSVALUE:5;
A13: |(y,y)| >= 0 by Th11;
delta(|(x,x)|,(2 * (|(x,y)|)),|(y,y)|) <= 0 by A8,A9,QUIN_1:10;
then (2 * u)^2 - 4 * (|(x,x)|) * (|(y,y)|) <= 0 by QUIN_1:def 1;
then 2^2 * ( u )^2 - 4 * (|(x,x)|) * (|(y,y)|) <= 0 by SQUARE_1:68;
then (2 * 2) * ( u )^2 - 4 * (|(x,x)|) * (|(y,y)|) <= 0
by SQUARE_1:def 3;
then 4 * (( u )^2) - 4 * ((|(x,x)|) * (|(y,y)|)) <= 0 by XCMPLX_1:4;
then 4 * ((( u )^2) - (|(x,x)|) * (|(y,y)|)) <= 0 by XCMPLX_1:40;
then ((|(x,y)|)^2) - (|(x,x)|) * (|(y,y)|) <= 0/4 by REAL_2:177;
then (|(x,y)|)^2 <= (|(x,x)|) * (|(y,y)|) by SQUARE_1:11;
then (abs(|(x,y)|))^2 <= (|(x,x)|) * (|(y,y)|) by SQUARE_1:62;
then (sqrt (abs(|(x,y)|))^2) <= sqrt ((|(x,x)|) * (|(y,y)|))
by A11,SQUARE_1:94;
then abs(|(x,y)|) <= sqrt (|(x,x)| * |(y,y)|) by A12,SQUARE_1:89;
hence thesis by A7,A13,SQUARE_1:97;
end;
sqrt (|(x,x)|)=|.x.| by Th13;
hence thesis by A2,A5,Th13;
end;
theorem :: Triangle
for x,y being FinSequence of REAL st len x=len y holds
|.x+y.| <= |.x.| + |.y.|
proof let x,y be FinSequence of REAL;
assume A1: len x=len y;
A2: 0 <= |.x+y.| by Th14;
A3: 0<= |.x.| by Th14;
0 <= |.y.| by Th14;
then A4: 0+0 <= |.x.| + |.y.| by A3,REAL_1:55;
A5: (|.x+y.|)^2 = (|.x.|)^2 + 2*|(y, x)| + (|.y.|)^2 by A1,Th33;
A6: |(x,y)| <= abs(|(x,y)|) by ABSVALUE:11;
abs(|(x,y)|) <= |.x.|*|.y.| by A1,Th37;
then |(x,y)| <= |.x.|*|.y.| by A6,AXIOMS:22;
then 2*|(x,y)| <= 2*(|.x.|*|.y.|) by AXIOMS:25;
then (|.x.|)^2+ 2*|(x,y)|<=(|.x.|)^2 + 2*(|.x.|*|.y.|) by REAL_1:55;
then (|.x.|)^2+ 2*|(x,y)| + (|.y.|)^2
<=(|.x.|)^2 + 2*(|.x.|*|.y.|)+ (|.y.|)^2 by REAL_1:55;
then (|.x+y.|)^2 <= (|.x.|)^2 + 2*|.x.|*|.y.|+(|.y.|)^2 by A5,XCMPLX_1:4;
then A7: (|.x+y.|)^2 <= (|.x.| + |.y.|)^2 by SQUARE_1:63;
0<= (|.x+y.|)^2 by SQUARE_1:72;
then sqrt((|.x+y.|)^2) <= sqrt((|.x.| + |.y.|)^2) by A7,SQUARE_1:94;
then |.x+y.| <= sqrt((|.x.| + |.y.|)^2) by A2,SQUARE_1:89;
hence thesis by A4,SQUARE_1:89;
end;
begin :: Inner Product of Points of TOP-REAL n
definition let n; let p,q be Point of TOP-REAL n;
func |(p,q)| -> real number means :Def2:
ex f,g being FinSequence of REAL st f = p & g = q & it = |(f,g)|;
existence
proof
p is Element of REAL n & q is Element of REAL n by EUCLID:25;
then reconsider f = p, g = q as FinSequence of REAL;
take |(f,g)|;
thus thesis;
end;
uniqueness;
commutativity;
end;
theorem
for n being Nat,p1,p2 being Point of TOP-REAL n holds
|(p1,p2)| = 1/4*((|. p1+p2 .|)^2-(|. p1-p2 .|)^2)
proof let n be Nat,p1,p2 be Point of TOP-REAL n;
consider f1,f2 being FinSequence of REAL such that
A1: f1 = p1 & f2 = p2 & |(p1,p2)| = |(f1,f2)| by Def2;
reconsider q1= p1, q2= p2 as Element of REAL n by EUCLID:25;
p1+p2=q1+q2 by EUCLID:def 10;
then A2: |. p1+p2 .|=|. q1+q2 .| by JGRAPH_1:def 5;
p1-p2=q1-q2 by EUCLID:def 13;
then |. p1-p2 .|=|. q1-q2 .| by JGRAPH_1:def 5;
hence thesis by A1,A2,Th10;
end;
theorem Th40:
|(p1 + p2, p3)| = |(p1, p3)| + |(p2, p3)|
proof
consider f1,f3 being FinSequence of REAL such that
A1: f1 = p1 & f3 = p3 &
|(p1, p3)| = |(f1,f3)| by Def2;
consider f2,f4 being FinSequence of REAL such that
A2: f2 = p2 & f4 = p3 & |(p2, p3)| = |(f2,f4)| by Def2;
consider f5,f6 being FinSequence of REAL such that
A3: f5 = p1+p2 & f6 = p3 & |(p1+p2, p3)| = |(f5,f6)| by Def2;
reconsider h1=f1 as Element of (len f1)-tuples_on REAL by FINSEQ_2:110;
A4: len f1=n by A1,EUCLID:28;
reconsider h2=f2 as Element of (len f2)-tuples_on REAL by FINSEQ_2:110;
A5: len f2=n by A2,EUCLID:28;
(len f1)-tuples_on REAL=REAL n by A4,EUCLID:def 1;
then A6: p1+p2=h1+h2 by A1,A2,A4,A5,EUCLID:def 10 .=f1+f2;
len f1=len f2 & len f2=len f3 by A1,A5,EUCLID:28;
hence thesis by A1,A2,A3,A6,Th19;
end;
theorem Th41:
for x being real number holds |(x*p1, p2)| = x*|(p1, p2)|
proof let x be real number;
consider f1,f2 being FinSequence of REAL such that
A1: f1 = p1 & f2 = p2 & |(p1, p2)| = |(f1,f2)| by Def2;
A2: len f1=n by A1,EUCLID:28;
A3: len f2=n by A1,EUCLID:28;
reconsider h1=f1 as Element of n-tuples_on REAL by A2,FINSEQ_2:110;
consider f3,f21 being FinSequence of REAL such that
A4: f3 = x*p1 & f21=p2 & |(x*p1, p2)| = |(f3,f21)| by Def2;
n-tuples_on REAL=REAL n by EUCLID:def 1;
then x*p1=x*h1 by A1,EUCLID:def 11 .=x*f1;
hence thesis by A1,A2,A3,A4,Th20;
end;
theorem
for x being real number holds |(p1, x*p2)| = x*|(p1, p2)| by Th41;
theorem Th43:
|(-p1, p2)| = -|(p1, p2)|
proof
|(-p1, p2)| = |((-1)*p1, p2)| by EUCLID:43
.= (-1)*|(p1, p2)| by Th41;
hence thesis by XCMPLX_1:180;
end;
theorem
|(p1, -p2)| = -|(p1, p2)| by Th43;
theorem
|(-p1, -p2)| = |(p1, p2)|
proof
|(-p1, -p2)| = -|(p1, -p2)| by Th43
.= --|(p1, p2)| by Th43;
hence thesis;
end;
theorem Th46:
|(p1-p2, p3)| = |(p1, p3)| - |(p2, p3)|
proof
|(p1 - p2, p3)| = |(p1 + -p2, p3)| by EUCLID:45
.= |(p1, p3)| + |(-p2, p3)| by Th40
.= |(p1, p3)| + - |(p2, p3)| by Th43;
hence thesis by XCMPLX_0:def 8;
end;
theorem
|((x*p1+y*p2), p3)| = x*|(p1,p3)| + y*|(p2,p3)|
proof
|(x*p1 + y*p2, p3)| = |(x*p1, p3)| + |(y*p2, p3)| by Th40
.= x*|(p1,p3)| + |(y*p2,p3)| by Th41
.= x*|(p1,p3)| + y*|(p2,p3)| by Th41;
hence thesis;
end;
theorem
|(p, q1+q2)| = |(p, q1)| + |(p, q2)| by Th40;
theorem
|(p, q1-q2)| = |(p, q1)| - |(p, q2)| by Th46;
theorem Th50:
|(p1+p2, q1+q2)| = |(p1, q1)| + |(p1, q2)| + |(p2, q1)| + |(p2, q2)|
proof
A1: |(p1+p2, q1)| = |(p1, q1)| + |(p2, q1)| by Th40;
A2: |(p1+p2, q2)| = |(p1, q2)| + |(p2, q2)| by Th40;
|(p1+p2, q1+q2)| = |(p1+p2, q1)| + |(p1+p2, q2)| by Th40
.= |(p1, q1)|+|(p2, q1)|+(|(p1, q2)|+0)+|(p2, q2)| by A1,A2,XCMPLX_1:1
.= |(p1, q1)|+|(p1, q2)|+|(p2, q1)|+|(p2, q2)| by XCMPLX_1:1;
hence thesis;
end;
theorem Th51:
|(p1-p2, q1-q2)| = |(p1, q1)| - |(p1, q2)| - |(p2, q1)| + |(p2, q2)|
proof
A1: |(p1,q1-q2)| = |(p1,q1)| - |(p1,q2)| by Th46;
A2: |(p2,q1-q2)| = |(p2,q1)| - |(p2,q2)| by Th46;
|(p1-p2, q1-q2)| = |(p1, q1-q2)| - |(p2, q1-q2)| by Th46
.= |(p1,q1)|-|(p1,q2)|-|(p2,q1)|+|(p2,q2)| by A1,A2,XCMPLX_1:37;
hence thesis;
end;
theorem Th52:
|(p+q, p+q)| = |(p, p)| + 2*|(p, q)| + |(q, q)|
proof
|(p, p)| + |(p, q)| + |(p, q)|
= |(p, p)| + (|(p, q)|+ |(p, q)|) by XCMPLX_1:1
.= |(p, p)| + 2*|(p, q)| by XCMPLX_1:11;
hence thesis by Th50;
end;
theorem Th53:
|(p-q, p-q)| = |(p, p)| - 2*|(p, q)| + |(q, q)|
proof
|(p-q, p-q)| = |(p,p)| - |(p,q)| - |(p,q)| + |(q, q)| by Th51
.= |(p,p)| - (|(p,q)| + |(p,q)|) + |(q, q)| by XCMPLX_1:36
.= |(p,p)| - 2*|(p,q)| + |(q, q)| by XCMPLX_1:11;
hence thesis;
end;
theorem Th54:
|(p, 0.REAL n)| = 0
proof
consider f1,f2 being FinSequence of REAL such that
A1: f1 = p & f2 = 0.REAL n &
|(p, 0.REAL n)| = |(f1,f2)| by Def2;
A2: f2=0*n by A1,EUCLID:def 9;
len f1=n by A1,EUCLID:28;
hence thesis by A1,A2,Th17;
end;
theorem
|(0.REAL n, p)| = 0 by Th54;
theorem
|(0.REAL n, 0.REAL n)| = 0 by Th54;
theorem Th57:
|(p,p)| >= 0
proof
consider f1,f2 being FinSequence of REAL such that
A1: f1 = p & f2 = p & |(p, p)| = |(f1,f2)| by Def2;
thus thesis by A1,Th11;
end;
theorem Th58:
|(p,p)| = |.p.|^2
proof
consider f1,f2 being FinSequence of REAL such that
A1: f1 = p & f2 = p & |(p, p)| = |(f1,f2)| by Def2;
A2: |(f1,f1)| = |.f1.|^2 by Th12;
p is Element of REAL n by EUCLID:25;
hence thesis by A1,A2,JGRAPH_1:def 5;
end;
theorem Th59:
|.p.| = sqrt |(p,p)|
proof
0 <= |.p.| by TOPRNS_1:26;
then |.p.| = sqrt |.p.|^2 by SQUARE_1:89
.= sqrt |(p,p)| by Th58;
hence thesis;
end;
theorem Th60:
0 <= |.p.|
proof
A1: |.p.| = sqrt |(p,p)| by Th59;
0 <= |(p,p)| by Th57;
hence thesis by A1,SQUARE_1:def 4;
end;
theorem Th61:
|. 0.REAL n .| = 0
proof
|. 0.REAL n .| = sqrt |(0.REAL n, 0.REAL n )| by Th59
.= 0 by Th54,SQUARE_1:82;
hence thesis;
end;
theorem Th62:
|(p,p)| = 0 iff |.p.| = 0
proof
|(p,p)| = 0 implies |.p.| = 0
proof
assume |(p,p)| = 0;
then |.p.|^2 = 0 by Th58;
hence |.p.| = 0 by SQUARE_1:73;
end;
hence thesis by Th58,SQUARE_1:60;
end;
theorem Th63:
|(p,p)| = 0 iff p = 0.REAL n
proof
|(p,p)| = 0 implies p = 0.REAL n
proof
assume
|(p,p)| = 0;
then |.p.| = 0 by Th62;
hence thesis by TOPRNS_1:25;
end;
hence thesis by Th54;
end;
theorem
|.p.|=0 iff p= 0.REAL n by Th61,TOPRNS_1:25;
theorem
p <> 0.REAL n iff |(p, p)| > 0
proof
p <> 0.REAL n implies |(p, p)| > 0
proof
assume p <> 0.REAL n;
then A1: |(p,p)| <> 0 by Th63;
0 <= |(p,p)| by Th57;
hence thesis by A1,REAL_1:def 5;
end;
hence thesis by Th63;
end;
theorem
p <> 0.REAL n iff |.p.| > 0
proof
p <> 0.REAL n implies |.p.| > 0
proof
assume p <> 0.REAL n;
then A1: 0 <> |.p.| by TOPRNS_1:25;
0 <= |.p.| by Th60;
hence thesis by A1,REAL_1:def 5;
end;
hence thesis by Th61;
end;
theorem Th67:
|.p+q.|^2 = |.p.|^2 + 2*|(q, p)| + |.q.|^2
proof
|.p+q.|^2 = |(p+q, p+q)| by Th58
.= |(p, p)| + 2*|(q, p)| + |(q, q)| by Th52
.= |.p.|^2 + 2*|(q, p)| + |(q, q)| by Th58
.= |.p.|^2 + 2*|(q, p)| + |.q.|^2 by Th58;
hence thesis;
end;
theorem Th68:
|.p-q.|^2 = |.p.|^2 - 2*|(q, p)| + |.q.|^2
proof
|.p-q.|^2 = |(p-q, p-q)| by Th58
.= |(p, p)| - 2*|(q, p)| + |(q, q)| by Th53
.= |.p.|^2 - 2*|(q, p)| + |(q, q)| by Th58
.= |.p.|^2 - 2*|(q, p)| + |.q.|^2 by Th58;
hence thesis;
end;
theorem
|.p+q.|^2 + |.p-q.|^2 = 2*(|.p.|^2 + |.q.|^2)
proof
A1: (|.p.|^2 + 2*|(p, q)| + |.q.|^2)
= (|.p.|^2 + |.q.|^2 + 2*|(p, q)|) by XCMPLX_1:1;
A2: (|.p.|^2 - 2*|(p, q)| + |.q.|^2)
= (|.p.|^2 +(-2*|(p, q)|) + |.q.|^2) by XCMPLX_0:def 8
.= (|.p.|^2 + |.q.|^2 +(-2*|(p, q)|)) by XCMPLX_1:1
.= (|.p.|^2 + |.q.|^2 -2*|(p, q)| ) by XCMPLX_0:def 8;
|.p+q.|^2 + |.p-q.|^2
= (|.p.|^2 + 2*|(p, q)| + |.q.|^2) + |.p-q.|^2 by Th67
.= (|.p.|^2 + |.q.|^2 + 2*|(p, q)|) +
(|.p.|^2 + |.q.|^2 - 2*|(p, q)|) by A1,A2,Th68
.= (|.p.|^2 + |.q.|^2) + (|.p.|^2 + |.q.|^2) by XCMPLX_1:28
.= 2*(|.p.|^2 + |.q.|^2) by XCMPLX_1:11;
hence thesis;
end;
theorem
|.p+q.|^2 - |.p-q.|^2 = 4* |(p,q)|
proof
|.p+q.|^2 - |.p-q.|^2
= (|.p.|^2 + 2*|(p,q)| + |.q.|^2) - |.p-q.|^2 by Th67
.= (|.p.|^2 + 2*|(p, q)| + |.q.|^2) -
(|.p.|^2 - 2*|(p, q)| + |.q.|^2) by Th68
.= (|.p.|^2 + 2*|(p, q)|) - (|.p.|^2 - 2*|(p, q)|) by XCMPLX_1:32
.= 2*|(p, q)| + 2*|(p, q)| by XCMPLX_1:31
.= 2*(2*|(p, q)|) by XCMPLX_1:11
.= 2* (|(p, q)| + |(p, q)|) by XCMPLX_1:11
.= (|(p, q)| + |(p, q)|) + (|(p, q)| + |(p, q)|) by XCMPLX_1:11
.= (|(p, q)| + |(p, q)| + |(p, q)| + |(p, q)|) by XCMPLX_1:1
.= 4*|(p, q)| by XCMPLX_1:13;
hence thesis;
end;
theorem
|(p,q)| = (1/4)*(|.p+q.|^2 - |.p-q.|^2)
proof
|.p+q.|^2 - |.p-q.|^2
= (|.p.|^2 + 2*|(p,q)| + |.q.|^2) - |.p-q.|^2 by Th67
.= (|.p.|^2 + 2*|(p, q)| + |.q.|^2) -
(|.p.|^2 - 2*|(p, q)| + |.q.|^2) by Th68
.= (|.p.|^2 + 2*|(p, q)|) - (|.p.|^2 - 2*|(p, q)|) by XCMPLX_1:32
.= 2*|(p, q)| + 2*|(p, q)| by XCMPLX_1:31
.= 2*(2*|(p, q)|) by XCMPLX_1:11
.= 2* (|(p, q)| + |(p, q)|) by XCMPLX_1:11
.= (|(p, q)| + |(p, q)|) + (|(p, q)| + |(p, q)|) by XCMPLX_1:11
.= (|(p, q)| + |(p, q)| + |(p, q)| + |(p, q)|) by XCMPLX_1:1
.= 4*|(p, q)| by XCMPLX_1:13;
then (1/4)*(|.p+q.|^2 - |.p-q.|^2) = (4*|(p, q)|)/4 by XCMPLX_1:100
.= (|(p, q)|+|(p, q)|+|(p, q)|+|(p, q)|)/4 by XCMPLX_1:13
.= |(p, q)| by XCMPLX_1:70;
hence thesis;
end;
theorem
|(p,q)| <= |(p,p)| + |(q,q)|
proof
A1: |(p-q, p-q)|
= |(p,p)| - 2*|(p,q)| + |(q,q)| by Th53
.= |(p,p)| + |(q,q)| - 2*|(p,q)| by XCMPLX_1:29;
0 <= |(p,p)| & 0 <= |(q,q)| by Th57;
then 0 + 0 <= |(p,p)| + |(q,q)| by REAL_1:55;
then A2: 0/2 <= (|(p,p)| + |(q,q)|)/2 by REAL_1:73;
0 <= |(p-q,p-q)| by Th57;
then 2*|(p,q)| <= |(p,p)| + |(q,q)| - 0 by A1,REAL_2:165;
then (2*|(p,q)|)/2 <= (|(p,p)| + |(q,q)|)/2 by REAL_1:73;
then |(p,q)| <= (|(p,p)| + |(q,q)|)/2 by XCMPLX_1:90;
then 0 + |(p,q)| <= (|(p,p)| + |(q,q)|)/2 + (|(p,p)| + |(q,q)|)/2
by A2,REAL_1:55;
then |(p,q)| <= 2*((|(p,p)| + |(q,q)|)/2) by XCMPLX_1:11;
then |(p,q)| <= (|(p,p)| + |(q,q)|)/(2/2) by XCMPLX_1:82;
hence thesis;
end;
theorem Th73: :: Schwartz
for p,q being Point of TOP-REAL n holds abs( |(p,q)|) <= |.p.|*|.q.|
proof let p,q be Point of TOP-REAL n;
set x=p,y=q;
A1:x = 0.REAL n implies abs(|(x,y)|) <= sqrt (|(x,x)|) * sqrt (|(y,y)|)
proof
assume
A2: x = 0.REAL n;
then A3: |(x,y)| = 0 by Th54;
sqrt (|(x,x)|) = 0 by A2,Th54,SQUARE_1:82;
hence thesis by A3,ABSVALUE:7;
end;
A4: x <> 0.REAL n implies abs(|(x,y)|) <= sqrt (|(x,x)|) * sqrt (|(y,y)|)
proof
assume x <> 0.REAL n;
then A5: |(x,x)| <> 0 by Th63;
A6: |(x,x)| >= 0 by Th57;
then A7: |(x,x)| > 0 by A5,REAL_1:def 5;
A8: for t be real number holds
|(x,x)| * t^2 + (2 * (|(x,y)|)) * t + |(y,y)| >= 0
proof
let t be real number;
set s=t^2;
|(t * x + y,t * x + y)| >= 0 by Th57;
then |(t * x, t * x)| + 2 * (|(t*x,y)|) + |(y,y)| >= 0
by Th52;
then t * ( |(t*x,x)|) + 2 * |(t*x,y)| + |(y,y)| >= 0 by Th41;
then t * (t * |(x,x)|) + 2 * |(t*x,y)| + |(y,y)| >= 0 by Th41;
then (t * t) * |(x,x)| + 2 * |(t*x,y)| + |(y,y)| >= 0
by XCMPLX_1:4;
then |(x,x)| * s + 2 * |((t*x),y)| + |(y,y)| >= 0 by SQUARE_1:def 3;
then |(x,x)| * s + 2 * (|(x,y)| * t) + |(y,y)| >= 0 by Th41;
hence thesis by XCMPLX_1:4;
end;
set w=abs( |(x,y)| ),u=|(x,y)|;
A9: 0 <= w^2 by SQUARE_1:72;
A10: abs(|(x,y)|) >= 0 by ABSVALUE:5;
A11: |(y,y)| >= 0 by Th57;
delta(|(x,x)|,(2 * (|(x,y)|)),|(y,y)|) <= 0 by A7,A8,QUIN_1:10;
then (2 * u)^2 - 4 * (|(x,x)|) * (|(y,y)|) <= 0 by QUIN_1:def 1;
then 2^2 * u^2 - 4 * (|(x,x)|) * (|(y,y)|) <= 0 by SQUARE_1:68;
then (2 * 2) * u^2 - 4 * (|(x,x)|) * (|(y,y)|) <= 0
by SQUARE_1:def 3;
then 4 * (u^2) - 4 * ((|(x,x)|) * (|(y,y)|)) <= 0 by XCMPLX_1:4;
then 4 * ((u^2) - (|(x,x)|) * (|(y,y)|)) <= 0 by XCMPLX_1:40;
then ((|(x,y)|)^2) - (|(x,x)|) * (|(y,y)|) <= 0/4 by REAL_2:177;
then (|(x,y)|)^2 <= (|(x,x)|) * (|(y,y)|) by SQUARE_1:11;
then (abs(|(x,y)|))^2 <= (|(x,x)|) * (|(y,y)|) by SQUARE_1:62;
then sqrt (abs(|(x,y)|))^2 <= sqrt ((|(x,x)|) * (|(y,y)|))
by A9,SQUARE_1:94;
then abs(|(x,y)|) <= sqrt (|(x,x)| * |(y,y)|) by A10,SQUARE_1:89;
hence thesis by A6,A11,SQUARE_1:97;
end;
sqrt (|(x,x)|)=|.x.| by Th59;
hence thesis by A1,A4,Th59;
end;
theorem :: Triangle
|.p+q.| <= |.p.| + |.q.|
proof
A1: 0 <= |.p+q.| by Th60;
A2: 0<= |.p.| by Th60;
0<= |.q.| by Th60;
then A3: 0+0 <= |.p.| + |.q.| by A2,REAL_1:55;
A4: (|.p+q.|)^2 = (|.p.|)^2 + 2*|(q, p)| + (|.q.|)^2 by Th67;
A5: |(p,q)| <= abs(|(p,q)|) by ABSVALUE:11;
abs(|(p,q)|) <= |.p.|*|.q.| by Th73;
then |(p,q)| <= |.p.|*|.q.| by A5,AXIOMS:22;
then 2*|(p,q)| <= 2*(|.p.|*|.q.|) by AXIOMS:25;
then (|.p.|)^2+ 2*|(p,q)|<=(|.p.|)^2 + 2*(|.p.|*|.q.|) by REAL_1:55;
then (|.p.|)^2+ 2*|(p,q)| + (|.q.|)^2
<= (|.p.|)^2 + 2*(|.p.|*|.q.|)+ (|.q.|)^2 by REAL_1:55;
then (|.p+q.|)^2 <= (|.p.|)^2 + 2*|.p.|*|.q.|+(|.q.|)^2 by A4,XCMPLX_1:4;
then A6: (|.p+q.|)^2 <= (|.p.| + |.q.|)^2 by SQUARE_1:63;
0<= (|.p+q.|)^2 by SQUARE_1:72;
then sqrt((|.p+q.|)^2) <= sqrt((|.p.| + |.q.|)^2) by A6,SQUARE_1:94;
then |.p+q.| <= sqrt((|.p.| + |.q.|)^2) by A1,SQUARE_1:89;
hence thesis by A3,SQUARE_1:89;
end;
definition let n, p, q;
pred p,q are_orthogonal means :Def3:
|(p,q)| = 0;
symmetry;
end;
theorem Th75:
p,0.REAL n are_orthogonal
proof |(p,0.REAL n)|=0 by Th54;
hence thesis by Def3;
end;
theorem
0.REAL n,p are_orthogonal by Th75;
theorem Th77:
p,p are_orthogonal iff p=0.REAL n
proof
p,p are_orthogonal iff |(p,p)|=0 by Def3;
hence thesis by Th63;
end;
theorem Th78:
p, q are_orthogonal implies a*p,q are_orthogonal
proof assume p, q are_orthogonal;
then |(p,q)|=0 by Def3;
then a*(|(p,q)|)=0;
then |(a*p,q)|=0 by Th41;
hence thesis by Def3;
end;
theorem
p, q are_orthogonal implies p,a*q are_orthogonal by Th78;
theorem
(for q holds p,q are_orthogonal) implies p=0.REAL n
proof assume (for q holds p,q are_orthogonal);
then p,p are_orthogonal;
hence thesis by Th77;
end;