:: The Inner Product of Finite Sequences and of Points of $n$-dimensionalTopological Space
:: by Kanchun and Yatsuka Nakamura
::
:: Received February 3, 2003
:: Copyright (c) 2003 Association of Mizar Users

theorem Th1: :: EUCLID_2:1

for n being Nat
for v being Element of n -tuples_on REAL
for i being Nat st i in Seg n holds
(mlt v,(0* n)) . i = 0

proof end;

theorem Th2: :: EUCLID_2:2

for n being Nat
for v being Element of n -tuples_on REAL holds mlt v,(0* n) = 0* n

proof end;

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 Th5: :: EUCLID_2:5

for x being FinSequence of REAL holds len (- x) = len x

proof end;

theorem Th6: :: EUCLID_2:6

for x1, x2 being FinSequence of REAL st len x1 = len x2 holds
len (x1 + x2) = len x1

proof end;

theorem Th7: :: EUCLID_2:7

for x1, x2 being FinSequence of REAL st len x1 = len x2 holds
len (x1 - x2) = len x1

proof end;

theorem Th8: :: EUCLID_2:8

for a being real number
for x being FinSequence of REAL holds len (a * x) = len x

proof end;

theorem Th9: :: 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)

proof end;

definition

let x1, x2 be real-valued FinSequence;
func |(x1,x2)| -> real number equals :: EUCLID_2:def 1
Sum (mlt x1,x2);
correctness
coherence
Sum (mlt x1,x2) is real number ;
;
commutativity
for b₁ being real number
for x1, x2 being real-valued FinSequence st b₁ = Sum (mlt x1,x2) holds
b₁ = Sum (mlt x2,x1) ;

end;

:: deftheorem defines |( EUCLID_2:def 1 :

for x1, x2 being real-valued FinSequence holds |(x1,x2)| = Sum (mlt x1,x2);

definition

let x1, x2 be real-valued FinSequence;
:: original: |(
redefine func |(x1,x2)| -> Element of REAL ;
correctness
coherence
|(x1,x2)| is Element of REAL ;
;
commutativity
for x1, x2 being real-valued FinSequence holds |(x1,x2)| = |(x2,x1)| ;

end;

theorem Th10: :: EUCLID_2:10

for n being Nat
for y1, y2 being FinSequence of REAL
for x1, x2 being Element of REAL n st x1 = y1 & x2 = y2 holds
|(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2 ) - (|.(x1 - x2).| ^2 ))

proof end;

theorem Th11: :: EUCLID_2:11

for x being FinSequence of REAL holds |(x,x)| >= 0

proof end;

theorem Th12: :: EUCLID_2:12

for x being FinSequence of REAL holds |.x.| ^2 = |(x,x)|

proof end;

theorem Th13: :: EUCLID_2:13

for x being FinSequence of REAL holds |.x.| = sqrt |(x,x)|

proof end;

theorem Th14: :: EUCLID_2:14

for x being FinSequence of REAL holds 0 <= |.x.|

proof end;

theorem Th15: :: EUCLID_2:15

for x being FinSequence of REAL holds
( |(x,x)| = 0 iff x = 0* (len x) )

proof end;

theorem :: EUCLID_2:16

for x being FinSequence of REAL holds
( |(x,x)| = 0 iff |.x.| = 0 )

proof end;

theorem Th17: :: EUCLID_2:17

for x being FinSequence of REAL holds |(x,(0* (len x)))| = 0

proof end;

theorem :: EUCLID_2:18

for x being FinSequence of REAL holds |((0* (len x)),x)| = 0 by Th17;

theorem Th19: :: 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)|

proof end;

theorem Th20: :: EUCLID_2:20

for x, y being FinSequence of REAL
for a being real number st len x = len y holds
|((a * x),y)| = a * |(x,y)|

proof end;

theorem Th21: :: EUCLID_2:21

for x, y being FinSequence of REAL
for a being real number st len x = len y holds
|(x,(a * y))| = a * |(x,y)|

proof end;

theorem Th22: :: EUCLID_2:22

for x1, x2 being FinSequence of REAL st len x1 = len x2 holds
|((- x1),x2)| = - |(x1,x2)|

proof end;

theorem :: EUCLID_2:23

for x1, x2 being FinSequence of REAL st len x1 = len x2 holds
|(x1,(- x2))| = - |(x1,x2)| by Th22;

theorem :: EUCLID_2:24

for x1, x2 being FinSequence of REAL st len x1 = len x2 holds
|((- x1),(- x2))| = |(x1,x2)|

proof end;

theorem Th25: :: 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)|

proof end;

theorem :: EUCLID_2:26

for x, y being real number
for 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 end;

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)| by Th19;

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)| by Th25;

theorem Th29: :: 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)|

proof end;

theorem Th30: :: 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)|

proof end;

theorem Th31: :: 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)|

proof end;

theorem Th32: :: 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)|

proof end;

theorem Th33: :: 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 )

proof end;

theorem Th34: :: 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 )

proof end;

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 ))

proof end;

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)|

proof end;

theorem Th37: :: EUCLID_2:37

for x, y being FinSequence of REAL st len x = len y holds
abs |(x,y)| <= |.x.| * |.y.|

proof end;

theorem :: EUCLID_2:38

for x, y being FinSequence of REAL st len x = len y holds
|.(x + y).| <= |.x.| + |.y.|

proof end;

definition

canceled;

end;

:: deftheorem EUCLID_2:def 2 :

canceled;

theorem :: EUCLID_2:39

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

proof end;

theorem Th40: :: EUCLID_2:40

for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|

proof end;

theorem Th41: :: EUCLID_2:41

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|

proof end;

theorem :: EUCLID_2:42

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds |(p1,(x * p2))| = x * |(p1,p2)| by Th41;

theorem Th43: :: EUCLID_2:43

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds |((- p1),p2)| = - |(p1,p2)|

proof end;

theorem :: EUCLID_2:44

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds |(p1,(- p2))| = - |(p1,p2)| by Th43;

theorem :: EUCLID_2:45

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds |((- p1),(- p2))| = |(p1,p2)|

proof end;

theorem Th46: :: EUCLID_2:46

for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|

proof end;

theorem :: EUCLID_2:47

for n being Nat
for x, y being real number
for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)

proof end;

theorem :: EUCLID_2:48

for n being Nat
for p, q1, q2 being Point of (TOP-REAL n) holds |(p,(q1 + q2))| = |(p,q1)| + |(p,q2)| by Th40;

theorem :: EUCLID_2:49

for n being Nat
for p, q1, q2 being Point of (TOP-REAL n) holds |(p,(q1 - q2))| = |(p,q1)| - |(p,q2)| by Th46;

theorem Th50: :: EUCLID_2:50

for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|

proof end;

theorem Th51: :: EUCLID_2:51

for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|

proof end;

theorem Th52: :: EUCLID_2:52

for n being Nat
for p, q being Point of (TOP-REAL n) holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|

proof end;

theorem Th53: :: EUCLID_2:53

for n being Nat
for p, q being Point of (TOP-REAL n) holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|

proof end;

theorem Th54: :: EUCLID_2:54

for n being Nat
for p being Point of (TOP-REAL n) holds |(p,(0. (TOP-REAL n)))| = 0

proof end;

theorem :: EUCLID_2:55

for n being Nat
for p being Point of (TOP-REAL n) holds |((0. (TOP-REAL n)),p)| = 0 by Th54;

theorem :: EUCLID_2:56

for n being Nat holds |((0. (TOP-REAL n)),(0. (TOP-REAL n)))| = 0 by Th54;

theorem Th57: :: EUCLID_2:57

for n being Nat
for p being Point of (TOP-REAL n) holds |(p,p)| >= 0

proof end;

theorem Th58: :: EUCLID_2:58

for n being Nat
for p being Point of (TOP-REAL n) holds |(p,p)| = |.p.| ^2

proof end;

theorem Th59: :: EUCLID_2:59

for n being Nat
for p being Point of (TOP-REAL n) holds |.p.| = sqrt |(p,p)|

proof end;

theorem Th60: :: EUCLID_2:60

for n being Nat
for p being Point of (TOP-REAL n) holds 0 <= |.p.|

proof end;

theorem Th61: :: EUCLID_2:61

for n being Nat holds |.(0. (TOP-REAL n)).| = 0

proof end;

theorem Th62: :: EUCLID_2:62

for n being Nat
for p being Point of (TOP-REAL n) holds
( |(p,p)| = 0 iff |.p.| = 0 )

proof end;

theorem Th63: :: EUCLID_2:63

for n being Nat
for p being Point of (TOP-REAL n) holds
( |(p,p)| = 0 iff p = 0. (TOP-REAL n) )

proof end;

theorem :: EUCLID_2:64

for n being Nat
for p being Point of (TOP-REAL n) holds
( |.p.| = 0 iff p = 0. (TOP-REAL n) )

proof end;

theorem :: EUCLID_2:65

for n being Nat
for p being Point of (TOP-REAL n) holds
( p <> 0. (TOP-REAL n) iff |(p,p)| > 0 )

proof end;

theorem :: EUCLID_2:66

for n being Nat
for p being Point of (TOP-REAL n) holds
( p <> 0. (TOP-REAL n) iff |.p.| > 0 )

proof end;

theorem Th67: :: EUCLID_2:67

for n being Nat
for p, q being Point of (TOP-REAL n) holds |.(p + q).| ^2 = ((|.p.| ^2 ) + (2 * |(q,p)|)) + (|.q.| ^2 )

proof end;

theorem Th68: :: EUCLID_2:68

for n being Nat
for p, q being Point of (TOP-REAL n) holds |.(p - q).| ^2 = ((|.p.| ^2 ) - (2 * |(q,p)|)) + (|.q.| ^2 )

proof end;

theorem :: EUCLID_2:69

for n being Nat
for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2 ) + (|.(p - q).| ^2 ) = 2 * ((|.p.| ^2 ) + (|.q.| ^2 ))

proof end;

theorem :: EUCLID_2:70

for n being Nat
for p, q being Point of (TOP-REAL n) holds (|.(p + q).| ^2 ) - (|.(p - q).| ^2 ) = 4 * |(p,q)|

proof end;

theorem :: EUCLID_2:71

for n being Nat
for p, q being Point of (TOP-REAL n) holds |(p,q)| = (1 / 4) * ((|.(p + q).| ^2 ) - (|.(p - q).| ^2 ))

proof end;

theorem :: EUCLID_2:72

for n being Nat
for p, q being Point of (TOP-REAL n) holds |(p,q)| <= |(p,p)| + |(q,q)|

proof end;

theorem Th73: :: EUCLID_2:73

for n being Nat
for p, q being Point of (TOP-REAL n) holds abs |(p,q)| <= |.p.| * |.q.|

proof end;

theorem :: EUCLID_2:74

for n being Nat
for p, q being Point of (TOP-REAL n) holds |.(p + q).| <= |.p.| + |.q.|

proof end;

definition

let p, q be real-valued FinSequence;
pred p,q are_orthogonal means :Def3: :: EUCLID_2:def 3
|(p,q)| = 0 ;
symmetry
for p, q being real-valued FinSequence st |(p,q)| = 0 holds
|(q,p)| = 0 ;

end;

:: deftheorem Def3 defines are_orthogonal EUCLID_2:def 3 :

for p, q being real-valued FinSequence holds
( p,q are_orthogonal iff |(p,q)| = 0 );

theorem Th75: :: EUCLID_2:75

for n being Nat
for p being Point of (TOP-REAL n) holds p, 0. (TOP-REAL n) are_orthogonal

proof end;

theorem :: EUCLID_2:76

for n being Nat
for p being Point of (TOP-REAL n) holds 0. (TOP-REAL n),p are_orthogonal by Th75;

theorem Th77: :: EUCLID_2:77

for n being Nat
for p being Point of (TOP-REAL n) holds
( p,p are_orthogonal iff p = 0. (TOP-REAL n) )

proof end;

theorem Th78: :: EUCLID_2:78

for n being Nat
for a being real number
for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds
a * p,q are_orthogonal

proof end;

theorem :: EUCLID_2:79

for n being Nat
for a being real number
for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds
p,a * q are_orthogonal by Th78;

theorem :: EUCLID_2:80

for n being Nat
for p being Point of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) holds p,q are_orthogonal ) holds
p = 0. (TOP-REAL n)

proof end;