:: The Inner Product of Finite Sequences and of Points of $n$-dimensional Topological Space
:: by Kanchun and Yatsuka Nakamura
::
:: Copyright (c) 2003-2021 Association of Mizar Users

theorem Th1: :: EUCLID_2:1
for i, n being Nat
for v being Element of n -tuples_on REAL 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 n being Nat
for y1, y2 being real-valued FinSequence
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;

Lm1: now :: thesis: for x being real-valued FinSequence holds x is FinSequence of REAL
let x be real-valued FinSequence; :: thesis: x is FinSequence of REAL
rng x c= REAL ;
hence x is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum
end;

theorem Th4: :: EUCLID_2:4
for x being real-valued FinSequence holds |.x.| ^2 = |(x,x)|
proof end;

theorem Th5: :: EUCLID_2:5
for x being real-valued FinSequence holds |.x.| = sqrt |(x,x)|
proof end;

theorem :: EUCLID_2:6
canceled;

::$CT theorem Th6: :: EUCLID_2:7 for x being real-valued FinSequence holds ( |(x,x)| = 0 iff x = 0* (len x) ) proof end; theorem :: EUCLID_2:8 for x being real-valued FinSequence holds ( |(x,x)| = 0 iff |.x.| = 0 ) proof end; theorem Th8: :: EUCLID_2:9 for x being real-valued FinSequence holds |(x,(0* (len x)))| = 0 proof end; theorem :: EUCLID_2:10 for x being real-valued FinSequence holds |((0* (len x)),x)| = 0 by Th8; theorem Th10: :: EUCLID_2:11 for x, y being real-valued FinSequence st len x = len y holds |.(x + y).| ^2 = (() + (2 * |(y,x)|)) + () proof end; theorem Th11: :: EUCLID_2:12 for x, y being real-valued FinSequence st len x = len y holds |.(x - y).| ^2 = (() - (2 * |(y,x)|)) + () proof end; theorem :: EUCLID_2:13 for x, y being real-valued FinSequence st len x = len y holds (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * (() + ()) proof end; theorem :: EUCLID_2:14 for x, y being real-valued FinSequence st len x = len y holds (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)| proof end; theorem Th14: :: EUCLID_2:15 for x, y being real-valued FinSequence st len x = len y holds |.|(x,y)|.| <= |.x.| * |.y.| proof end; theorem Th15: :: EUCLID_2:16 for x, y being real-valued FinSequence st len x = len y holds |.(x + y).| <= |.x.| + |.y.| proof end; theorem :: EUCLID_2:17 canceled; ::$CT
theorem Th16: :: EUCLID_2:18
for n being Nat
for p1, p2, p3 being Point of () holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
proof end;

theorem Th17: :: EUCLID_2:19
for n being Nat
for p1, p2 being Point of ()
for x being Real holds |((x * p1),p2)| = x * |(p1,p2)|
proof end;

theorem :: EUCLID_2:20
for n being Nat
for p1, p2 being Point of ()
for x being Real holds |(p1,(x * p2))| = x * |(p1,p2)| by Th17;

theorem Th19: :: EUCLID_2:21
for n being Nat
for p1, p2 being Point of () holds |((- p1),p2)| = - |(p1,p2)|
proof end;

theorem :: EUCLID_2:22
for n being Nat
for p1, p2 being Point of () holds |(p1,(- p2))| = - |(p1,p2)| by Th19;

theorem :: EUCLID_2:23
for n being Nat
for p1, p2 being Point of () holds |((- p1),(- p2))| = |(p1,p2)|
proof end;

theorem Th22: :: EUCLID_2:24
for n being Nat
for p1, p2, p3 being Point of () holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|
proof end;

theorem :: EUCLID_2:25
for n being Nat
for x, y being Real
for p1, p2, p3 being Point of () holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
proof end;

theorem :: EUCLID_2:26
for n being Nat
for p, q1, q2 being Point of () holds |(p,(q1 + q2))| = |(p,q1)| + |(p,q2)| by Th16;

theorem :: EUCLID_2:27
for n being Nat
for p, q1, q2 being Point of () holds |(p,(q1 - q2))| = |(p,q1)| - |(p,q2)| by Th22;

theorem Th26: :: EUCLID_2:28
for n being Nat
for p1, p2, q1, q2 being Point of () holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
proof end;

theorem Th27: :: EUCLID_2:29
for n being Nat
for p1, p2, q1, q2 being Point of () holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
proof end;

theorem Th28: :: EUCLID_2:30
for n being Nat
for p, q being Point of () holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|
proof end;

theorem Th29: :: EUCLID_2:31
for n being Nat
for p, q being Point of () holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
proof end;

theorem Th30: :: EUCLID_2:32
for n being Nat
for p being Point of () holds |(p,(0. ()))| = 0
proof end;

theorem :: EUCLID_2:33
for n being Nat
for p being Point of () holds |((0. ()),p)| = 0 by Th30;

theorem :: EUCLID_2:34
for n being Nat holds |((0. ()),(0. ()))| = 0 by Th30;

theorem Th33: :: EUCLID_2:35
for n being Nat
for p being Point of () holds |(p,p)| >= 0 by RVSUM_1:119;

theorem Th34: :: EUCLID_2:36
for n being Nat
for p being Point of () holds |(p,p)| = |.p.| ^2 by Th4;

theorem Th35: :: EUCLID_2:37
for n being Nat
for p being Point of () holds |.p.| = sqrt |(p,p)|
proof end;

theorem Th36: :: EUCLID_2:38
for n being Nat
for p being Point of () holds 0 <= |.p.|
proof end;

theorem Th37: :: EUCLID_2:39
for n being Nat holds |.(0. ()).| = 0 by TOPRNS_1:23;

theorem Th38: :: EUCLID_2:40
for n being Nat
for p being Point of () holds
( |(p,p)| = 0 iff |.p.| = 0 )
proof end;

theorem Th39: :: EUCLID_2:41
for n being Nat
for p being Point of () holds
( |(p,p)| = 0 iff p = 0. () )
proof end;

theorem :: EUCLID_2:42
for n being Nat
for p being Point of () holds
( |.p.| = 0 iff p = 0. () ) by ;

theorem :: EUCLID_2:43
for n being Nat
for p being Point of () holds
( p <> 0. () iff |(p,p)| > 0 )
proof end;

theorem :: EUCLID_2:44
for n being Nat
for p being Point of () holds
( p <> 0. () iff |.p.| > 0 )
proof end;

theorem Th43: :: EUCLID_2:45
for n being Nat
for p, q being Point of () holds |.(p + q).| ^2 = (() + (2 * |(q,p)|)) + ()
proof end;

theorem Th44: :: EUCLID_2:46
for n being Nat
for p, q being Point of () holds |.(p - q).| ^2 = (() - (2 * |(q,p)|)) + ()
proof end;

theorem :: EUCLID_2:47
for n being Nat
for p, q being Point of () holds (|.(p + q).| ^2) + (|.(p - q).| ^2) = 2 * (() + ())
proof end;

theorem :: EUCLID_2:48
for n being Nat
for p, q being Point of () holds (|.(p + q).| ^2) - (|.(p - q).| ^2) = 4 * |(p,q)|
proof end;

theorem :: EUCLID_2:49
for n being Nat
for p, q being Point of () holds |(p,q)| = (1 / 4) * ((|.(p + q).| ^2) - (|.(p - q).| ^2))
proof end;

theorem :: EUCLID_2:50
for n being Nat
for p, q being Point of () holds |(p,q)| <= |(p,p)| + |(q,q)|
proof end;

theorem :: EUCLID_2:51
for n being Nat
for p, q being Point of () holds |.|(p,q)|.| <= |.p.| * |.q.|
proof end;

theorem :: EUCLID_2:52
for n being Nat
for p, q being Point of () holds |.(p + q).| <= |.p.| + |.q.|
proof end;

theorem Th51: :: EUCLID_2:53
for n being Nat
for p being Point of () holds p, 0. () are_orthogonal by Th30;

theorem :: EUCLID_2:54
for n being Nat
for p being Point of () holds 0. (),p are_orthogonal by Th51;

theorem Th53: :: EUCLID_2:55
for n being Nat
for p being Point of () holds
( p,p are_orthogonal iff p = 0. () ) by Th39;

theorem Th54: :: EUCLID_2:56
for n being Nat
for a being Real
for p, q being Point of () st p,q are_orthogonal holds
a * p,q are_orthogonal
proof end;

theorem :: EUCLID_2:57
for n being Nat
for a being Real
for p, q being Point of () st p,q are_orthogonal holds
p,a * q are_orthogonal by Th54;

theorem :: EUCLID_2:58
for n being Nat
for p being Point of () st ( for q being Point of () holds p,q are_orthogonal ) holds
p = 0. () by Th53;