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;