:: The Inner Product of Finite Sequences and of Points of $n$-dimensional
:: Topological Space
:: by Kanchun and Yatsuka Nakamura
::
:: Received February 3, 2003
:: Copyright (c) 2003-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, NAT_1, SUBSET_1, FINSEQ_2, PRE_TOPC, EUCLID, RVSUM_1,
FUNCT_1, CARD_1, FINSEQ_1, RELAT_1, VALUED_0, ARYTM_3, COMPLEX1,
SQUARE_1, ARYTM_1, CARD_3, XXREAL_0, TARSKI, FUNCT_3, SUPINF_2, REAL_1;
notations TARSKI, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1,
FINSEQ_1, FINSEQ_2, VALUED_0, QUIN_1, STRUCT_0, PRE_TOPC, RVSUM_1,
RLVECT_1, EUCLID, SQUARE_1, XXREAL_0;
constructors REAL_1, SQUARE_1, BINOP_2, COMPLEX1, QUIN_1, FINSEQOP, MONOID_0,
TOPRNS_1, RELSET_1, BINOP_1;
registrations FUNCT_1, RELSET_1, NUMBERS, XREAL_0, SQUARE_1, BINOP_2,
MEMBERED, FINSEQ_2, MONOID_0, EUCLID, VALUED_0, FINSEQ_1, QUIN_1;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
equalities SQUARE_1, FINSEQ_2, RVSUM_1, VALUED_1, ALGSTR_0, ORDINAL1;
expansions RVSUM_1;
theorems EUCLID, RVSUM_1, FINSEQ_2, FINSEQ_1, FINSEQ_3, SQUARE_1, QUIN_1,
ABSVALUE, TOPRNS_1, COMPLEX1, XREAL_1, XXREAL_0, FUNCOP_1, XCMPLX_1,
FINSEQOP, ORDINAL1, FUNCT_1, CARD_1;
begin :: Preliminaries
reserve i, n for Nat,
x, y, a for Real,
v for Element of n-tuples_on REAL,
p, p1, p2, p3, q, q1, q2 for Point of TOP-REAL n;
theorem Th1:
mlt(v, 0*n).i = 0
proof
A1: 0*n = n |-> (0 qua set) by EUCLID:def 4;
set v0 = (0*n).i;
A2: dom(0*n) = Seg n by FINSEQ_2:124;
i in Seg n or not i in Seg n;
then
A3: v0=0 by A1,A2,FUNCOP_1:7,FUNCT_1:def 2;
mlt(v,0*n).i = v.i * v0 by RVSUM_1:60
.= 0 by A3;
hence thesis;
end;
theorem Th2:
mlt(v, 0*n) = 0*n
proof
len 0*n = n by CARD_1:def 7;
then reconsider z= 0*n as Element of n-tuples_on REAL by FINSEQ_2:92;
A1: len 0*n = n by CARD_1:def 7;
A2: for j be Nat st j in dom 0*n holds mlt(v,0*n).j=(0*n).j
proof
let j be Nat;
assume
j in dom 0*n;
thus mlt(v,0*n).j = 0 by Th1
.= (n |-> 0).j
.= (0*n).j by EUCLID:def 4;
end;
len mlt(v, z) = n by CARD_1:def 7;
then dom mlt(v, 0*n) = dom 0*n by A1,FINSEQ_3:29;
hence thesis by A2,FINSEQ_1:13;
end;
begin :: Inner Product of Finite Sequences
theorem
for y1,y2 being real-valued FinSequence, 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 real-valued FinSequence,x1,x2 be Element of REAL n;
assume
A1: x1=y1 & x2=y2;
reconsider w1=x1, w2=x2 as Element of n-tuples_on REAL by EUCLID:def 1;
set v1=sqr (x1+x2), v2=sqr (x1-x2);
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:86;
then
A3: (sqrt Sum sqr (x1+x2))^2 =Sum sqr (x1+x2) by SQUARE_1:def 2;
A4: Sum sqr (x1+x2)-Sum sqr (x1-x2)=Sum (v1 - v2) by RVSUM_1:90;
Sum sqr (x1-x2)>=0 by RVSUM_1:86;
then
A5: (sqrt Sum sqr (x1-x2))^2=Sum sqr (x1-x2) by SQUARE_1:def 2;
A6: 2*mlt(w1,w2) +sqr w2+ 2*mlt(w1,w2) = 2*mlt(w1,w2)+(2*mlt(w1,w2) + sqr w2 )
.= 2*mlt(w1,w2)+2*mlt(w1,w2) + sqr w2 by FINSEQOP:28;
A7: sqr w1 + (2*mlt(w1,w2) + sqr w2) = (2*mlt(w1,w2) + sqr w2) + sqr w1;
v1-v2=sqr w1 + 2*mlt(w1,w2) + sqr w2 -sqr (w1-w2) by RVSUM_1:68
.= sqr w1 + 2*mlt(w1,w2) + sqr w2 -(sqr w1 - 2*mlt(w1,w2) + sqr w2) by
RVSUM_1:69
.= 2*mlt(w1,w2) +sqr w2+ sqr w1 -(sqr w1 - 2*mlt(w1,w2) + sqr w2) by A7,
FINSEQOP:28
.= 2*mlt(w1,w2) +sqr w2+ sqr w1 -(sqr w1 - 2*mlt(w1,w2))- sqr w2 by
RVSUM_1:39
.= 2*mlt(w1,w2) +sqr w2+ sqr w1 - sqr w1 + 2*mlt(w1,w2)- sqr w2 by
RVSUM_1:41
.= (2*mlt(w1,w2) +sqr w2+ 2*mlt(w1,w2))- sqr w2 by RVSUM_1:42
.= 2*mlt(w1,w2)+2*mlt(w1,w2) by A6,RVSUM_1:42
.= (2+2)*mlt(w1,w2) by RVSUM_1:50
.= 4*mlt(w1,w2);
then 1/4*((|.(x1+x2).|)^2-(|.(x1-x2).|)^2) = 1/4*(4*Sum(mlt(w1,w2))) by A2,A3
,A5,A4,RVSUM_1:87
.= Sum(mlt(w1,w2));
hence thesis by A1;
end;
Lm1:
now
let x be real-valued FinSequence;
rng x c= REAL;
hence x is FinSequence of REAL by FINSEQ_1:def 4;
end;
theorem Th4:
for x being real-valued FinSequence holds |.x.|^2 = |(x,x)|
proof
let x be real-valued FinSequence;
A1: 0 <= |(x,x)| by RVSUM_1:119;
|.x.|^2 = (sqrt Sum sqr x)^2 by EUCLID:def 5
.= |(x,x)| by A1,SQUARE_1:def 2;
hence thesis;
end;
theorem Th5:
for x being real-valued FinSequence holds |.x.| = sqrt |(x,x)|
proof
let x be real-valued FinSequence;
|.x.| = sqrt |.x.|^2 by EUCLID:9,SQUARE_1:22
.= sqrt |(x,x)| by Th4;
hence thesis;
end;
::$CT
theorem Th6:
for x being real-valued FinSequence holds |(x,x)|=0 iff x=0*(len x)
proof
let x be real-valued FinSequence;
thus |(x,x)|=0 implies x=0*(len x)
proof
x is FinSequence of REAL by Lm1;
then reconsider y=x as Element of REAL len x by EUCLID:76;
assume |(x,x)|=0;
then |.x.|^2=0 by Th4;
then |.x.|=0 by XCMPLX_1:6;
then y=0*(len x) by EUCLID:8;
hence thesis;
end;
assume x=0*(len x);
then |.x.|=0 by EUCLID:7;
then |(x,x)|=0^2 by Th4;
hence thesis;
end;
theorem
for x being real-valued FinSequence holds |(x,x)| = 0 iff |.x.| = 0
proof
let x be real-valued FinSequence;
A1: |(x,x)| = 0^2 implies |.x.| = 0
proof
assume |(x,x)| = 0^2;
then x=0*(len x) by Th6;
hence thesis by EUCLID:7;
end;
|.x.| = 0 implies |(x,x)| = 0^2 by Th4;
hence thesis by A1;
end;
theorem Th8:
for x being real-valued FinSequence holds |(x, 0*(len x))| = 0
proof
let x be real-valued FinSequence;
set n=len x;
x is FinSequence of REAL by Lm1;
then reconsider p1=x as Element of n-tuples_on REAL by FINSEQ_2:92;
A1: 0*n = n |-> 0 by EUCLID:def 4;
|(x, 0*n)| = Sum mlt(p1,0*n) .= Sum 0*n by Th2
.= 0 by A1,RVSUM_1:81;
hence thesis;
end;
theorem
for x being real-valued FinSequence holds |(0*(len x),x)| = 0 by Th8;
theorem Th10:
for x,y being real-valued FinSequence st len x=len y holds |.x+y.|^2
= |.x.|^2 + 2*|(y, x)| + |.y.|^2
proof
let x,y be real-valued FinSequence;
assume
A1: len x=len y;
|.x+y.|^2 = |(x+y, x+y)| by Th4
.= |(x, x)| + 2*|(x, y)| + |(y, y)| by A1,RVSUM_1:128
.= |.x.|^2 + 2*|(y, x)| + |(y, y)| by Th4
.= |.x.|^2 + 2*|(y, x)| + |.y.|^2 by Th4;
hence thesis;
end;
theorem Th11:
for x,y being real-valued FinSequence st len x=len y holds |.x-y.|^2
= |.x.|^2 - 2*|(y, x)| + |.y.|^2
proof
let x,y be real-valued FinSequence;
assume
A1: len x=len y;
|.x-y.|^2 = |(x-y, x-y)| by Th4
.= |(x, x)| - 2*|(x, y)| + |(y, y)| by A1,RVSUM_1:129
.= |.x.|^2 - 2*|(y, x)| + |(y, y)| by Th4
.= |.x.|^2 - 2*|(y, x)| + |.y.|^2 by Th4;
hence thesis;
end;
theorem
for x,y being real-valued FinSequence st len x=len y holds |.x+y.|^2 + |.x
-y.|^2 = 2*(|.x.|^2 + |.y.|^2)
proof
let x,y be real-valued FinSequence;
assume
A1: len x=len y;
then
|.x+y.|^2 + |.x-y.|^2 = (|.x.|^2 + 2*|(y, x)| + |.y.|^2) + |.x-y.|^2 by Th10
.= (|.x.|^2 + 2*|(x, y)| + |.y.|^2) + (|.x.|^2 - 2*|(y, x)| + |.y.|^2)
by A1,Th11
.= 2*(|.x.|^2 + |.y.|^2);
hence thesis;
end;
theorem
for x,y being real-valued FinSequence st len x=len y holds |.x+y.|^2 - |.x
-y.|^2 = 4* |(x,y)|
proof
let x,y be real-valued FinSequence;
assume
A1: len x=len y;
then |.x+y.|^2 - |.x-y.|^2 = (|.x.|^2 + 2*|(y,x)| + |.y.|^2) - |.x-y.|^2 by
Th10
.= (|.x.|^2 + 2*|(x, y)| + |.y.|^2) - (|.x.|^2 - 2*|(y, x)| + |.y.|^2)
by A1,Th11
.= 4*|(x, y)|;
hence thesis;
end;
theorem Th14: :: Schwartz
for x,y being real-valued FinSequence st len x=len y holds
|.|(x,y)|.| <= |.x.|*|.y.|
proof
let x,y be real-valued FinSequence;
assume
A1: len x=len y;
A2: x = 0*(len x) implies |.|(x,y)|.| <= sqrt (|(x,x)|) * sqrt (|(y,y)|)
proof
assume x = 0*(len x);
then |(x,y)| = 0 & |(x,x)|=0 by A1,Th8;
hence thesis by ABSVALUE:2;
end;
A3: x <> 0*(len x) implies |.|(x,y)|.| <= sqrt (|(x,x)|) * sqrt (|(y,y)|)
proof
A4: for t be Real holds |(x,x)| * t^2 + (2 * (|(x,y)|)) * t + |(y,
y)| >= 0
proof
let t be Real;
set s=t^2;
A5: len (t * x)=len x by RVSUM_1:117;
|((t * x + y),(t * x + y))| >= 0 by RVSUM_1:119;
then
|((t * x) , (t * x))| + 2 * (|((t*x),y)|) + |(y,y)| >= 0 by A1,A5,
RVSUM_1:128;
then t * ( |(t*x,x)|) + 2 * |((t*x),y)| + |(y,y)| >= 0 by A5,RVSUM_1:121;
then t * ( t * |(x,x)|) + 2 * |((t*x),y)| + |(y,y)| >= 0 by A1,
RVSUM_1:121;
then |(x,x)| * s + 2 * (|(x,y)| * t) + |(y,y)| >= 0 by A1,RVSUM_1:121;
hence thesis;
end;
set w=|.|(x,y)|.|, u=|(x,y)|;
A6: |(x,x)| >= 0 by RVSUM_1:119;
assume x <> 0*(len x);
then |(x,x)| <> 0 by Th6;
then |(x,x)| > 0 by A6,XXREAL_0:1;
then delta(|(x,x)|,(2 * (|(x,y)|)),|(y,y)|) <= 0 by A4,QUIN_1:10;
then (2 * u)^2 - 4 * (|(x,x)|) * (|(y,y)|) <= 0 by QUIN_1:def 1;
then 4 * ((( u )^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 0 <= w^2 & (|.|(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
A7: |.|(x,y)|.| <= sqrt (|(x,x)| * |(y,y)|) by COMPLEX1:46,SQUARE_1:22;
|(y,y)| >= 0 by RVSUM_1:119;
hence thesis by A6,A7,SQUARE_1:29;
end;
sqrt (|(x,x)|)=|.x.| by Th5;
hence thesis by A2,A3,Th5;
end;
theorem Th15: :: Triangle
for x,y being real-valued FinSequence st len x=len y holds
|.x+y.| <= |.x.| + |.y.|
proof
let x,y be real-valued FinSequence;
assume
A1: len x=len y;
then |(x,y)| <= |.|(x,y)|.| & |.|(x,y)|.| <= |.x.|*|.y.| by Th14,ABSVALUE:4;
then |(x,y)| <= |.x.|*|.y.| by XXREAL_0:2;
then 2*|(x,y)| <= 2*(|.x.|*|.y.|) by XREAL_1:64;
then
A2: (|.x.|)^2+ 2*|(x,y)|<=(|.x.|)^2 + 2*(|.x.|*|.y.|) by XREAL_1:7;
(|.x+y.|)^2 = (|.x.|)^2 + 2*|(y, x)| + (|.y.|)^2 by A1,Th10;
then
A3: (|.x+y.|)^2 <= (|.x.|)^2 + 2*|.x.|*|.y.|+(|.y.|)^2 by A2,XREAL_1:7;
0<= (|.x+y.|)^2 by XREAL_1:63;
then sqrt((|.x+y.|)^2) <= sqrt((|.x.| + |.y.|)^2) by A3,SQUARE_1:26;
then
A4: |.x+y.| <= sqrt((|.x.| + |.y.|)^2) by EUCLID:9,SQUARE_1:22;
0<= |.x.| & 0 <= |.y.| by EUCLID:9;
then 0+0 <= |.x.| + |.y.| by XREAL_1:7;
hence thesis by A4,SQUARE_1:22;
end;
begin :: Inner Product of Points of TOP-REAL n
::$CT
theorem Th16:
|(p1 + p2, p3)| = |(p1, p3)| + |(p2, p3)|
proof
reconsider f1=p1, f2=p2, f3=p3 as FinSequence of REAL by EUCLID:24;
reconsider q1 = p1, q2=p2 as Element of REAL n by EUCLID:22;
len f2=n by CARD_1:def 7;
then
A1: len f1=len f2 & len f2=len f3 by CARD_1:def 7;
thus thesis by A1,RVSUM_1:120;
end;
theorem Th17:
for x being Real holds |(x*p1, p2)| = x*|(p1, p2)|
proof
let x be Real;
reconsider f1=p1,f2=p2 as FinSequence of REAL by EUCLID:24;
reconsider q1 = p1 as Element of REAL n by EUCLID:22;
len f1=n & len f2=n by CARD_1:def 7;
hence thesis by RVSUM_1:121;
end;
theorem
for x being Real holds |(p1, x*p2)| = x*|(p1, p2)| by Th17;
theorem Th19:
|(-p1, p2)| = -|(p1, p2)|
proof
|(-p1, p2)| = |((-1)*p1, p2)|
.= (-1)*|(p1, p2)| by Th17;
hence thesis;
end;
theorem
|(p1, -p2)| = -|(p1, p2)| by Th19;
theorem
|(-p1, -p2)| = |(p1, p2)|
proof
|(-p1, -p2)| = -|(p1, -p2)| by Th19
.= --|(p1, p2)| by Th19;
hence thesis;
end;
theorem Th22:
|(p1-p2, p3)| = |(p1, p3)| - |(p2, p3)|
proof
|(p1 - p2, p3)| = |(p1, p3)| + |(-p2, p3)| by Th16
.= |(p1, p3)| + - |(p2, p3)| by Th19;
hence thesis;
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 Th16
.= x*|(p1,p3)| + |(y*p2,p3)| by Th17
.= x*|(p1,p3)| + y*|(p2,p3)| by Th17;
hence thesis;
end;
theorem
|(p, q1+q2)| = |(p, q1)| + |(p, q2)| by Th16;
theorem
|(p, q1-q2)| = |(p, q1)| - |(p, q2)| by Th22;
theorem Th26:
|(p1+p2, q1+q2)| = |(p1, q1)| + |(p1, q2)| + |(p2, q1)| + |(p2, q2)|
proof
A1: |(p1+p2, q1)| = |(p1, q1)| + |(p2, q1)| & |(p1+p2, q2)| = |(p1, q2)| +
|(p2, q2)| by Th16;
|(p1+p2, q1+q2)| = |(p1+p2, q1)| + |(p1+p2, q2)| by Th16
.= |(p1, q1)|+|(p1, q2)|+|(p2, q1)|+|(p2, q2)| by A1;
hence thesis;
end;
theorem Th27:
|(p1-p2, q1-q2)| = |(p1, q1)| - |(p1, q2)| - |(p2, q1)| + |(p2, q2)|
proof
A1: |(p1,q1-q2)| = |(p1,q1)| - |(p1,q2)| & |(p2,q1-q2)| = |(p2,q1)| - |(p2,
q2)| by Th22;
|(p1-p2, q1-q2)| = |(p1, q1-q2)| - |(p2, q1-q2)| by Th22
.= |(p1,q1)|-|(p1,q2)|-|(p2,q1)|+|(p2,q2)| by A1;
hence thesis;
end;
theorem Th28:
|(p+q, p+q)| = |(p, p)| + 2*|(p, q)| + |(q, q)|
proof
|(p, p)| + |(p, q)| + |(p, q)| = |(p, p)| + 2*|(p, q)|;
hence thesis by Th26;
end;
theorem Th29:
|(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 Th27
.= |(p,p)| - 2*|(p,q)| + |(q, q)|;
hence thesis;
end;
theorem Th30:
|(p, 0.TOP-REAL n)| = 0
proof
reconsider f1=p as FinSequence of REAL by EUCLID:24;
len f1=n by CARD_1:def 7;
then 0*(len f1) = 0.TOP-REAL n by EUCLID:70;
hence thesis by Th8;
end;
theorem
|(0.TOP-REAL n, p)| = 0 by Th30;
theorem
|(0.TOP-REAL n, 0.TOP-REAL n)| = 0 by Th30;
theorem Th33:
|(p,p)| >= 0 by RVSUM_1:119;
theorem Th34:
|(p,p)| = |.p.|^2 by Th4;
theorem Th35:
|.p.| = sqrt |(p,p)|
proof
|.p.| = sqrt |.p.|^2 by SQUARE_1:22,TOPRNS_1:25
.= sqrt |(p,p)| by Th34;
hence thesis;
end;
theorem Th36:
0 <= |.p.|
proof
|.p.| = sqrt |(p,p)| & 0 <= |(p,p)| by Th33,Th35;
hence thesis by SQUARE_1:def 2;
end;
theorem Th37:
|. 0.TOP-REAL n .| = 0
by TOPRNS_1:23;
theorem Th38:
|(p,p)| = 0 iff |.p.| = 0
proof
A1: |(p,p)| = 0^2 implies |.p.| = 0
proof
assume |(p,p)| = 0^2;
then |.p.|^2 = 0 by Th34;
hence thesis by XCMPLX_1:6;
end;
|.p.| = 0 implies |(p,p)| = 0^2 by Th34;
hence thesis by A1;
end;
theorem Th39:
|(p,p)| = 0 iff p = 0.TOP-REAL n
proof
|(p,p)| = 0 implies p = 0.TOP-REAL n
proof
assume |(p,p)| = 0;
then n in NAT & |.p.| = 0 by Th38,ORDINAL1:def 12;
hence thesis by TOPRNS_1:24;
end;
hence thesis by Th30;
end;
theorem
|.p.|=0 iff p = 0.TOP-REAL n
by Th37,TOPRNS_1:24;
theorem
p <> 0.TOP-REAL n iff |(p, p)| > 0
proof
p <> 0.TOP-REAL n implies |(p, p)| > 0
proof
assume p <> 0.TOP-REAL n;
then
A1: |(p,p)| <> 0 by Th39;
0 <= |(p,p)| by Th33;
hence thesis by A1,XXREAL_0:1;
end;
hence thesis by Th39;
end;
theorem
p <> 0.TOP-REAL n iff |.p.| > 0
proof
p <> 0.TOP-REAL n implies |.p.| > 0
proof
assume
A1: p <> 0.TOP-REAL n;
n in NAT & 0 <= |.p.| by Th36,ORDINAL1:def 12;
hence thesis by A1,TOPRNS_1:24,XXREAL_0:1;
end;
hence thesis by Th37;
end;
theorem Th43:
|.p+q.|^2 = |.p.|^2 + 2*|(q, p)| + |.q.|^2
proof
|.p+q.|^2 = |(p+q, p+q)| by Th34
.= |(p, p)| + 2*|(q, p)| + |(q, q)| by Th28
.= |.p.|^2 + 2*|(q, p)| + |(q, q)| by Th34
.= |.p.|^2 + 2*|(q, p)| + |.q.|^2 by Th34;
hence thesis;
end;
theorem Th44:
|.p-q.|^2 = |.p.|^2 - 2*|(q, p)| + |.q.|^2
proof
|.p-q.|^2 = |(p-q, p-q)| by Th34
.= |(p, p)| - 2*|(q, p)| + |(q, q)| by Th29
.= |.p.|^2 - 2*|(q, p)| + |(q, q)| by Th34
.= |.p.|^2 - 2*|(q, p)| + |.q.|^2 by Th34;
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)| );
|.p+q.|^2 + |.p-q.|^2 = (|.p.|^2 + 2*|(p, q)| + |.q.|^2) + |.p-q.|^2 by Th43
.= (|.p.|^2 + |.q.|^2 + 2*|(p, q)|) + (|.p.|^2 + |.q.|^2 - 2*|(p, q)|)
by A1,Th44
.= 2*(|.p.|^2 + |.q.|^2);
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 Th43
.= (|.p.|^2 + 2*|(p, q)| + |.q.|^2) - (|.p.|^2 - 2*|(p, q)| + |.q.|^2)
by Th44
.= 4*|(p, q)|;
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 Th43
.= (|.p.|^2 + 2*|(p, q)| + |.q.|^2) - (|.p.|^2 - 2*|(p, q)| + |.q.|^2)
by Th44
.= 4*|(p, q)|;
hence thesis;
end;
theorem
|(p,q)| <= |(p,p)| + |(q,q)|
proof
0 <= |(p,p)| & 0 <= |(q,q)| by Th33;
then 0 + 0 <= |(p,p)| + |(q,q)| by XREAL_1:7;
then
A1: 0/2 <= (|(p,p)| + |(q,q)|)/2 by XREAL_1:72;
|(p-q, p-q)| = |(p,p)| - 2*|(p,q)| + |(q,q)| by Th29
.= |(p,p)| + |(q,q)| - 2*|(p,q)|;
then 2*|(p,q)| <= |(p,p)| + |(q,q)| - 0 by Th33,XREAL_1:11;
then (2*|(p,q)|)/2 <= (|(p,p)| + |(q,q)|)/2 by XREAL_1:72;
then 0 + |(p,q)| <= (|(p,p)| + |(q,q)|)/2 + (|(p,p)| + |(q,q)|)/2 by A1,
XREAL_1:7;
hence thesis;
end;
theorem :: Schwartz
|.|(p,q)|.| <= |.p.|*|.q.|
proof
len p = n & len q = n by CARD_1:def 7;
hence thesis by Th14;
end;
theorem :: Triangle
|.p+q.| <= |.p.| + |.q.|
proof
A1: len p = n & len q = n by CARD_1:def 7;
thus thesis by A1,Th15;
end;
theorem Th51:
p,0.TOP-REAL n are_orthogonal
by Th30;
theorem
0.TOP-REAL n,p are_orthogonal by Th51;
theorem Th53:
p,p are_orthogonal iff p=0.TOP-REAL n
by Th39;
theorem Th54:
p, q are_orthogonal implies a*p,q are_orthogonal
proof
assume p, q are_orthogonal;
then |(p,q)|=0;
then a*(|(p,q)|)=0;
then |(a*p,q)|=0 by Th17;
hence thesis;
end;
theorem
p, q are_orthogonal implies p,a*q are_orthogonal by Th54;
theorem
(for q holds p,q are_orthogonal) implies p=0.TOP-REAL n by Th53;