Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

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

**by****Kanchun , and****Yatsuka Nakamura**- Received February 3, 2003
- 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;

Back to top