Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### The Inner Product of Finite Sequences and of Points of \$n\$-dimensional Topological Space

by
Kanchun , and
Yatsuka Nakamura

MML identifier: EUCLID_2
[ Mizar article, MML identifier index ]

```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;

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 :: EUCLID_2:1
for i holds i in Seg n implies mlt(v, 0*n).i = 0;

theorem :: EUCLID_2:2
mlt(v, 0*n) = 0*n;

theorem :: EUCLID_2:3
for x being FinSequence of REAL holds (-1)*x = -x;

theorem :: EUCLID_2:4
for x,y being FinSequence of REAL st len x=len y holds x-y=x+(-y);

theorem :: EUCLID_2:5
for x being FinSequence of REAL holds len (-x)=len x;

theorem :: EUCLID_2:6
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
len (x1+x2)=len x1;

theorem :: EUCLID_2:7
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
len (x1-x2)=len x1;

theorem :: EUCLID_2:8
for a being real number, x being FinSequence of REAL holds len (a*x)=len x;

theorem :: EUCLID_2:9
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);

begin :: Inner Product of Finite Sequences

definition let x1,x2 be FinSequence of REAL;
func |( x1,x2 )| -> real number equals
:: EUCLID_2:def 1
Sum mlt(x1,x2);
commutativity;
end;

theorem :: EUCLID_2:10
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);

theorem :: EUCLID_2:11
for x being FinSequence of REAL holds |(x,x)| >= 0;

theorem :: EUCLID_2:12
for x being FinSequence of REAL holds (|.x.|)^2=|(x,x)|;

theorem :: EUCLID_2:13
for x being FinSequence of REAL holds |.x.| = sqrt |(x,x)|;

theorem :: EUCLID_2:14
for x being FinSequence of REAL holds 0 <= |.x.|;

theorem :: EUCLID_2:15
for x being FinSequence of REAL holds |(x,x)|=0 iff x=0*(len x);

theorem :: EUCLID_2:16
for x being FinSequence of REAL holds |(x,x)| = 0 iff |.x.| = 0;

theorem :: EUCLID_2:17
for x being FinSequence of REAL holds |(x, 0*(len x))| = 0;

theorem :: EUCLID_2:18
for x being FinSequence of REAL holds |(0*(len x),x)| = 0;

theorem :: EUCLID_2:19
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)|;

theorem :: EUCLID_2:20
for x,y being FinSequence of REAL,a being real number st
len x=len y holds |(a*x,y)| = a*|(x,y)|;

theorem :: EUCLID_2:21
for x,y being FinSequence of REAL,a being real number st
len x=len y holds |(x,a*y)| = a*|(x,y)|;

theorem :: EUCLID_2:22
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
|(-x1, x2)| = -|(x1, x2)|;

theorem :: EUCLID_2:23
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
|(x1, -x2)| = -|(x1, x2)|;

theorem :: EUCLID_2:24
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
|(-x1, -x2)| = |(x1, x2)|;

theorem :: EUCLID_2:25
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)|;

theorem :: EUCLID_2:26
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)|;

theorem :: EUCLID_2:27
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)|;

theorem :: EUCLID_2:28
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)|;

theorem :: EUCLID_2:29
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)|;

theorem :: EUCLID_2:30
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)|;

theorem :: EUCLID_2:31
for x,y being FinSequence of REAL st len x=len y holds
|(x+y, x+y)| = |(x, x)| + 2*|(x, y)| + |(y, y)|;

theorem :: EUCLID_2:32
for x,y being FinSequence of REAL st len x=len y holds
|(x-y, x-y)| = |(x, x)| - 2*|(x, y)| + |(y, y)|;

theorem :: EUCLID_2:33
for x,y being FinSequence of REAL st len x=len y holds
|.x+y.|^2 = |.x.|^2 + 2*|(y, x)| + |.y.|^2;

theorem :: EUCLID_2:34
for x,y being FinSequence of REAL st len x=len y holds
|.x-y.|^2 = |.x.|^2 - 2*|(y, x)| + |.y.|^2;

theorem :: EUCLID_2:35
for x,y being FinSequence of REAL st len x=len y holds
|.x+y.|^2 + |.x-y.|^2 = 2*(|.x.|^2 + |.y.|^2);

theorem :: EUCLID_2:36
for x,y being FinSequence of REAL st len x=len y holds
|.x+y.|^2 - |.x-y.|^2 = 4* |(x,y)|;

theorem :: EUCLID_2:37  :: Schwartz
for x,y being FinSequence of REAL st len x=len y holds
abs |(x,y)| <= |.x.|*|.y.|;

theorem :: EUCLID_2:38 :: Triangle
for x,y being FinSequence of REAL st len x=len y holds
|.x+y.| <= |.x.| + |.y.|;

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
:: EUCLID_2:def 2
ex f,g being FinSequence of REAL st f = p & g = q & it = |(f,g)|;
commutativity;
end;

theorem :: EUCLID_2:39
for n being Nat,p1,p2 being Point of TOP-REAL n holds
|(p1,p2)| = 1/4*((|. p1+p2 .|)^2-(|. p1-p2 .|)^2);

theorem :: EUCLID_2:40
|(p1 + p2, p3)| = |(p1, p3)| + |(p2, p3)|;

theorem :: EUCLID_2:41
for x being real number holds |(x*p1, p2)| = x*|(p1, p2)|;

theorem :: EUCLID_2:42
for x being real number holds |(p1, x*p2)| = x*|(p1, p2)|;

theorem :: EUCLID_2:43
|(-p1, p2)| = -|(p1, p2)|;

theorem :: EUCLID_2:44
|(p1, -p2)| = -|(p1, p2)|;

theorem :: EUCLID_2:45
|(-p1, -p2)| = |(p1, p2)|;

theorem :: EUCLID_2:46
|(p1-p2, p3)| = |(p1, p3)| - |(p2, p3)|;

theorem :: EUCLID_2:47
|((x*p1+y*p2), p3)| = x*|(p1,p3)| + y*|(p2,p3)|;

theorem :: EUCLID_2:48
|(p, q1+q2)| = |(p, q1)| + |(p, q2)|;

theorem :: EUCLID_2:49
|(p, q1-q2)| = |(p, q1)| - |(p, q2)|;

theorem :: EUCLID_2:50
|(p1+p2, q1+q2)| = |(p1, q1)| + |(p1, q2)| + |(p2, q1)| + |(p2, q2)|;

theorem :: EUCLID_2:51
|(p1-p2, q1-q2)| = |(p1, q1)| - |(p1, q2)| - |(p2, q1)| + |(p2, q2)|;

theorem :: EUCLID_2:52
|(p+q, p+q)| = |(p, p)| + 2*|(p, q)| + |(q, q)|;

theorem :: EUCLID_2:53
|(p-q, p-q)| = |(p, p)| - 2*|(p, q)| + |(q, q)|;

theorem :: EUCLID_2:54
|(p, 0.REAL n)| = 0;

theorem :: EUCLID_2:55
|(0.REAL n, p)| = 0;

theorem :: EUCLID_2:56
|(0.REAL n, 0.REAL n)| = 0;

theorem :: EUCLID_2:57
|(p,p)| >= 0;

theorem :: EUCLID_2:58
|(p,p)| = |.p.|^2;

theorem :: EUCLID_2:59
|.p.| = sqrt |(p,p)|;

theorem :: EUCLID_2:60
0 <= |.p.|;

theorem :: EUCLID_2:61
|. 0.REAL n .| = 0;

theorem :: EUCLID_2:62
|(p,p)| = 0 iff |.p.| = 0;

theorem :: EUCLID_2:63
|(p,p)| = 0 iff p = 0.REAL n;

theorem :: EUCLID_2:64
|.p.|=0 iff p= 0.REAL n;

theorem :: EUCLID_2:65
p <> 0.REAL n iff |(p, p)| > 0;

theorem :: EUCLID_2:66
p <> 0.REAL n iff |.p.| > 0;

theorem :: EUCLID_2:67
|.p+q.|^2 = |.p.|^2 + 2*|(q, p)| + |.q.|^2;

theorem :: EUCLID_2:68
|.p-q.|^2 = |.p.|^2 - 2*|(q, p)| + |.q.|^2;

theorem :: EUCLID_2:69
|.p+q.|^2 + |.p-q.|^2 = 2*(|.p.|^2 + |.q.|^2);

theorem :: EUCLID_2:70
|.p+q.|^2 - |.p-q.|^2 = 4* |(p,q)|;

theorem :: EUCLID_2:71
|(p,q)| = (1/4)*(|.p+q.|^2 - |.p-q.|^2);

theorem :: EUCLID_2:72
|(p,q)| <= |(p,p)| + |(q,q)|;

theorem :: EUCLID_2:73  :: Schwartz
for p,q being Point of TOP-REAL n holds abs( |(p,q)|) <= |.p.|*|.q.|;

theorem :: EUCLID_2:74  :: Triangle
|.p+q.| <= |.p.| + |.q.|;

definition let n, p, q;
pred p,q are_orthogonal means
:: EUCLID_2:def 3
|(p,q)| = 0;
symmetry;
end;

theorem :: EUCLID_2:75
p,0.REAL n are_orthogonal;

theorem :: EUCLID_2:76
0.REAL n,p are_orthogonal;

theorem :: EUCLID_2:77
p,p are_orthogonal iff p=0.REAL n;

theorem :: EUCLID_2:78
p, q are_orthogonal implies a*p,q are_orthogonal;

theorem :: EUCLID_2:79
p, q are_orthogonal implies p,a*q are_orthogonal;

theorem :: EUCLID_2:80
(for q holds p,q are_orthogonal) implies p=0.REAL n;

```