:: The Euclidean Space
:: by Agata Darmochwa{\l}
::
:: Received November 21, 1991
:: Copyright (c) 1991 Association of Mizar Users


begin

definition
let n be Nat;
func REAL n -> FinSequence-DOMAIN of REAL equals :: EUCLID:def 1
n -tuples_on REAL;
coherence
n -tuples_on REAL is FinSequence-DOMAIN of REAL ;
end;

:: deftheorem defines REAL EUCLID:def 1 :
for n being Nat holds REAL n = n -tuples_on REAL;

registration
let n be Nat;
cluster -> n -element Element of REAL n;
coherence
for b1 being Element of REAL n holds b1 is n -element ;
end;

definition
func absreal -> Function of REAL,REAL means :Def2: :: EUCLID:def 2
 for r being real number holds it . r = abs r;
existence
ex b1 being Function of REAL,REAL st
for r being real number holds b1 . r = abs r
proof end;
uniqueness
for b1, b2 being Function of REAL,REAL st ( for r being real number holds b1 . r = abs r ) & ( for r being real number holds b2 . r = abs r ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines absreal EUCLID:def 2 :
for b1 being Function of REAL,REAL holds
( b1 = absreal iff for r being real number holds b1 . r = abs r );

definition
let x be real-valued FinSequence;
:: original: |.
redefine func abs x -> FinSequence of REAL equals :: EUCLID:def 3
absreal * x;
coherence
|.x.| is FinSequence of REAL
proof end;
compatibility
for b1 being FinSequence of REAL holds
( b1 = |.x.| iff b1 = absreal * x )
proof end;
end;

:: deftheorem defines abs EUCLID:def 3 :
for x being real-valued FinSequence holds abs x = absreal * x;

definition
let n be Nat;
func 0* n -> real-valued FinSequence equals :: EUCLID:def 4
n |-> 0;
coherence
n |-> 0 is real-valued FinSequence ;
end;

:: deftheorem defines 0* EUCLID:def 4 :
for n being Nat holds 0* n = n |-> 0;

definition
let n be Nat;
:: original: 0*
redefine func 0* n -> Element of REAL n;
coherence
0* n is Element of REAL n ;
end;

definition
let n be Nat;
let x be Element of REAL n;
:: original: -
redefine func - x -> Element of REAL n;
coherence
- x is Element of REAL n
proof end;
end;

definition
let n be Nat;
let x, y be Element of REAL n;
:: original: +
redefine func x + y -> Element of REAL n;
coherence
x + y is Element of REAL n
proof end;
:: original: -
redefine func x - y -> Element of REAL n;
coherence
x - y is Element of REAL n
proof end;
end;

definition
let n be Nat;
let x be Element of REAL n;
let r be real number ;
:: original: (#)
redefine func r * x -> Element of REAL n;
coherence
r (#) x is Element of REAL n
proof end;
end;

definition
let n be Nat;
let x be Element of REAL n;
:: original: |.
redefine func abs x -> Element of n -tuples_on REAL;
coherence
|.x.| is Element of n -tuples_on REAL by FINSEQ_2:133;
end;

definition
let n be Nat;
let x be Element of REAL n;
:: original: ^2
redefine func sqr x -> Element of n -tuples_on REAL;
coherence
x ^2 is Element of n -tuples_on REAL by FINSEQ_2:133;
end;

definition
let f be real-valued FinSequence;
func |.f.| -> Real equals :: EUCLID:def 5
 sqrt (Sum (sqr f));
coherence
sqrt (Sum (sqr f)) is Real ;
end;

:: deftheorem defines |. EUCLID:def 5 :
for f being real-valued FinSequence holds |.f.| = sqrt (Sum (sqr f));

theorem :: EUCLID:1
canceled;

theorem :: EUCLID:2
canceled;

theorem :: EUCLID:3
for n being Nat
for x being b1 -element FinSequence holds dom x = Seg n
proof end;

theorem :: EUCLID:4
for k being Nat
for f being real-valued FinSequence holds f . k in REAL ;

theorem :: EUCLID:5
canceled;

theorem :: EUCLID:6
for n, k being Nat
for x being Element of REAL n holds (abs x) . k = abs (x . k) by VALUED_1:18;

Lm1: for f being real-valued FinSequence holds f is FinSequence of REAL
proof end;

Lm2: for f being real-valued FinSequence holds f is Element of REAL (len f)
proof end;

theorem :: EUCLID:7
for n being Nat holds abs (0* n) = n |-> 0
proof end;

theorem Th8: :: EUCLID:8
for f being complex-valued Function holds abs (- f) = abs f
proof end;

theorem Th9: :: EUCLID:9
for r being real number
for f being real-valued FinSequence holds abs (r * f) = (abs r) * (abs f) by RFUNCT_1:37;

theorem Th10: :: EUCLID:10
for n being Nat holds |.(0* n).| = 0
proof end;

Lm3: for f being real-valued FinSequence holds sqr (abs f) = sqr f
proof end;

theorem Th11: :: EUCLID:11
for n being Nat
for x being Element of REAL n st |.x.| = 0 holds
x = 0* n
proof end;

theorem Th12: :: EUCLID:12
for f being real-valued FinSequence holds |.f.| >= 0
proof end;

registration
let f be real-valued FinSequence;
cluster |.f.| -> non negative ;
coherence
not |.f.| is negative by Th12;
end;

theorem Th13: :: EUCLID:13
for f being real-valued FinSequence holds |.(- f).| = |.f.|
proof end;

theorem :: EUCLID:14
for r being real number
for f being real-valued FinSequence holds |.(r * f).| = (abs r) * |.f.|
proof end;

theorem Th15: :: EUCLID:15
for n being Nat
for x1, x2 being Element of REAL n holds |.(x1 + x2).| <= |.x1.| + |.x2.|
proof end;

theorem Th16: :: EUCLID:16
for n being Nat
for x1, x2 being Element of REAL n holds |.(x1 - x2).| <= |.x1.| + |.x2.|
proof end;

theorem :: EUCLID:17
for n being Nat
for x1, x2 being Element of REAL n holds |.x1.| - |.x2.| <= |.(x1 + x2).|
proof end;

theorem :: EUCLID:18
for n being Nat
for x1, x2 being Element of REAL n holds |.x1.| - |.x2.| <= |.(x1 - x2).|
proof end;

theorem Th19: :: EUCLID:19
for n being Nat
for x1, x2 being Element of REAL n holds
( |.(x1 - x2).| = 0 iff x1 = x2 )
proof end;

registration
let n be Nat;
let x1 be Element of REAL n;
cluster |.(x1 - x1).| -> zero ;
coherence
|.(x1 - x1).| is empty by Th19;
end;

theorem :: EUCLID:20
for n being Nat
for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| > 0
proof end;

theorem Th21: :: EUCLID:21
for n being Nat
for x1, x2 being Element of REAL n holds |.(x1 - x2).| = |.(x2 - x1).|
proof end;

theorem Th22: :: EUCLID:22
for n being Nat
for x1, x2, x being Element of REAL n holds |.(x1 - x2).| <= |.(x1 - x).| + |.(x - x2).|
proof end;

definition
let n be Nat;
func Pitag_dist n -> Function of [:(REAL n),(REAL n):],REAL means :Def6: :: EUCLID:def 6
 for x, y being Element of REAL n holds it . (x,y) = |.(x - y).|;
existence
ex b1 being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b1 . (x,y) = |.(x - y).|
proof end;
uniqueness
for b1, b2 being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b1 . (x,y) = |.(x - y).| ) & ( for x, y being Element of REAL n holds b2 . (x,y) = |.(x - y).| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Pitag_dist EUCLID:def 6 :
for n being Nat
for b2 being Function of [:(REAL n),(REAL n):],REAL holds
( b2 = Pitag_dist n iff for x, y being Element of REAL n holds b2 . (x,y) = |.(x - y).| );

theorem :: EUCLID:23
for x, y being real-valued FinSequence holds sqr (x - y) = sqr (y - x)
proof end;

theorem Th24: :: EUCLID:24
for n being Nat holds Pitag_dist n is_metric_of REAL n
proof end;

definition
let n be Nat;
func Euclid n -> strict MetrSpace equals :: EUCLID:def 7
 MetrStruct(# (REAL n),(Pitag_dist n) #);
coherence
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrSpace
proof end;
end;

:: deftheorem defines Euclid EUCLID:def 7 :
for n being Nat holds Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #);

registration
let n be Nat;
cluster Euclid n -> non empty strict ;
coherence
not Euclid n is empty ;
end;

definition
let n be Nat;
func TOP-REAL n -> strict RLTopStruct means :Def8: :: EUCLID:def 8
( TopStruct(# the carrier of it, the topology of it #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = RealVectSpace (Seg n) );
existence
ex b1 being strict RLTopStruct st
( TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) )
proof end;
uniqueness
for b1, b2 being strict RLTopStruct st TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b2, the topology of b2 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = RealVectSpace (Seg n) holds
b1 = b2 ;
end;

:: deftheorem Def8 defines TOP-REAL EUCLID:def 8 :
for n being Nat
for b2 being strict RLTopStruct holds
( b2 = TOP-REAL n iff ( TopStruct(# the carrier of b2, the topology of b2 #) = TopSpaceMetr (Euclid n) & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = RealVectSpace (Seg n) ) );

registration
let n be Nat;
cluster TOP-REAL n -> non empty strict ;
coherence
not TOP-REAL n is empty
proof end;
end;

registration
let n be Nat;
cluster TOP-REAL n -> TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ;
coherence
( TOP-REAL n is TopSpace-like & TOP-REAL n is Abelian & TOP-REAL n is add-associative & TOP-REAL n is right_zeroed & TOP-REAL n is right_complementable & TOP-REAL n is vector-distributive & TOP-REAL n is scalar-distributive & TOP-REAL n is scalar-associative & TOP-REAL n is scalar-unital )
proof end;
end;

theorem Th25: :: EUCLID:25
for n being Nat holds the carrier of (TOP-REAL n) = REAL n
proof end;

theorem Th26: :: EUCLID:26
for n being Nat
for p being Point of (TOP-REAL n) holds p is Function of (Seg n),REAL
proof end;

theorem Th27: :: EUCLID:27
for n being Nat
for p being Point of (TOP-REAL n) holds p is FinSequence of REAL
proof end;

registration
let n be Nat;
cluster TOP-REAL n -> constituted-FinSeqs strict ;
coherence
TOP-REAL n is constituted-FinSeqs
proof end;
end;

registration
let n be Nat;
cluster -> FinSequence-like Element of the carrier of (TOP-REAL n);
coherence
for b1 being Point of (TOP-REAL n) holds b1 is FinSequence-like ;
end;

registration
let n be Nat;
cluster -> real-valued Element of the carrier of (TOP-REAL n);
coherence
for b1 being Point of (TOP-REAL n) holds b1 is real-valued by Th27;
end;

Lm4: for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2
proof end;

Lm5: for n being Nat
for p being Point of (TOP-REAL n)
for x being real number
for r being real-valued Function st p = r holds
x * p = x (#) r
proof end;

registration
let r, s be real number ;
let n be Nat;
let p be Element of (TOP-REAL n);
let f be real-valued FinSequence;
identify r * p with s * f when r = s, p = f;
compatibility
( r = s & p = f implies r * p = s * f ) by Lm5;
end;

registration
let n be Nat;
let p, q be Element of (TOP-REAL n);
let f, g be real-valued FinSequence;
identify p + q with f + g when p = f, q = g;
compatibility
( p = f & q = g implies p + q = f + g ) by Lm4;
end;

registration
let n be Nat;
let p be Element of (TOP-REAL n);
let f be real-valued FinSequence;
identify - p with - f when p = f;
compatibility
( p = f implies - p = - f )
proof end;
end;

registration
let n be Nat;
let p, q be Element of (TOP-REAL n);
let f, g be real-valued FinSequence;
identify p - q with f - g when p = f, q = g;
compatibility
( p = f & q = g implies p - q = f - g ) ;
end;

registration
let n be Nat;
cluster -> n -element Element of the carrier of (TOP-REAL n);
coherence
for b1 being Point of (TOP-REAL n) holds b1 is n -element
proof end;
end;

notation
let n be Nat;
synonym 0.REAL n for 0* n;
end;

definition
let n be Nat;
:: original: 0*
redefine func 0.REAL n -> Point of (TOP-REAL n);
coherence
0* n is Point of (TOP-REAL n)
proof end;
end;

theorem :: EUCLID:28
canceled;

theorem :: EUCLID:29
for n being Nat
for x being Element of REAL n holds sqr (abs x) = sqr x by Lm3;

theorem :: EUCLID:30
for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds (p1 + p2) + p3 = p1 + (p2 + p3) by RLVECT_1:def 6;

theorem :: EUCLID:31
for n being Nat
for p being Point of (TOP-REAL n) holds
( (0. (TOP-REAL n)) + p = p & p + (0. (TOP-REAL n)) = p ) by RLVECT_1:10;

theorem :: EUCLID:32
for n being Nat
for x being real number holds x * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:23;

theorem :: EUCLID:33
for n being Nat
for p being Point of (TOP-REAL n) holds
( 1 * p = p & 0 * p = 0. (TOP-REAL n) ) by RLVECT_1:23, RLVECT_1:def 11;

theorem :: EUCLID:34
for n being Nat
for p being Point of (TOP-REAL n)
for x, y being real number holds (x * y) * p = x * (y * p) by RLVECT_1:def 10;

theorem :: EUCLID:35
for n being Nat
for p being Point of (TOP-REAL n)
for x being real number holds
( not x * p = 0. (TOP-REAL n) or x = 0 or p = 0. (TOP-REAL n) ) by RLVECT_1:24;

theorem :: EUCLID:36
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds x * (p1 + p2) = (x * p1) + (x * p2) by RLVECT_1:def 8;

theorem :: EUCLID:37
for n being Nat
for p being Point of (TOP-REAL n)
for x, y being real number holds (x + y) * p = (x * p) + (y * p) by RLVECT_1:def 9;

theorem :: EUCLID:38
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds
( not x * p1 = x * p2 or x = 0 or p1 = p2 ) by RLVECT_1:50;

theorem :: EUCLID:39
for n being Nat
for p being Point of (TOP-REAL n) holds - (- p) = p ;

theorem :: EUCLID:40
for n being Nat
for p being Point of (TOP-REAL n) holds p + (- p) = 0. (TOP-REAL n) by RLVECT_1:16;

theorem :: EUCLID:41
for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 + p2 = 0. (TOP-REAL n) holds
p1 = - p2 by RLVECT_1:19;

theorem :: EUCLID:42
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds - (p1 + p2) = (- p1) - p2 by RLVECT_1:44;

theorem :: EUCLID:43
for n being Nat
for p being Point of (TOP-REAL n) holds - p = (- 1) * p ;

theorem :: EUCLID:44
for n being Nat
for p being Point of (TOP-REAL n)
for x being real number holds
( - (x * p) = (- x) * p & - (x * p) = x * (- p) ) by RLVECT_1:39, RLVECT_1:98;

theorem :: EUCLID:45
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds p1 - p2 = p1 + (- p2) ;

theorem :: EUCLID:46
for n being Nat
for p being Point of (TOP-REAL n) holds p - p = 0. (TOP-REAL n) by RLVECT_1:16;

theorem :: EUCLID:47
for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 - p2 = 0. (TOP-REAL n) holds
p1 = p2 by RLVECT_1:35;

theorem :: EUCLID:48
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds
( - (p1 - p2) = p2 - p1 & - (p1 - p2) = (- p1) + p2 ) by RLVECT_1:47;

theorem :: EUCLID:49
for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds p1 + (p2 - p3) = (p1 + p2) - p3 by RLVECT_1:def 6;

theorem :: EUCLID:50
for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds p1 - (p2 + p3) = (p1 - p2) - p3 by RLVECT_1:41;

theorem :: EUCLID:51
for n being Nat
for p1, p2, p3 being Point of (TOP-REAL n) holds p1 - (p2 - p3) = (p1 - p2) + p3 by RLVECT_1:43;

theorem :: EUCLID:52
for n being Nat
for p, p1 being Point of (TOP-REAL n) holds
( p = (p + p1) - p1 & p = (p - p1) + p1 ) by RLVECT_4:1;

theorem :: EUCLID:53
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being real number holds x * (p1 - p2) = (x * p1) - (x * p2) by RLVECT_1:48;

theorem :: EUCLID:54
for n being Nat
for p being Point of (TOP-REAL n)
for x, y being real number holds (x - y) * p = (x * p) - (y * p) by RLVECT_1:49;

theorem :: EUCLID:55
for p being Point of (TOP-REAL 2) ex x, y being Real st p = <*x,y*>
proof end;

definition
canceled;
canceled;
canceled;
canceled;
canceled;
let p be Point of (TOP-REAL 2);
func p `1 -> Real equals :: EUCLID:def 14
p . 1;
coherence
p . 1 is Real ;
func p `2 -> Real equals :: EUCLID:def 15
p . 2;
coherence
p . 2 is Real ;
end;

:: deftheorem EUCLID:def 9 :
canceled;

:: deftheorem EUCLID:def 10 :
canceled;

:: deftheorem EUCLID:def 11 :
canceled;

:: deftheorem EUCLID:def 12 :
canceled;

:: deftheorem EUCLID:def 13 :
canceled;

:: deftheorem defines `1 EUCLID:def 14 :
for p being Point of (TOP-REAL 2) holds p `1 = p . 1;

:: deftheorem defines `2 EUCLID:def 15 :
for p being Point of (TOP-REAL 2) holds p `2 = p . 2;

notation
let x, y be real number ;
synonym |[x,y]| for <*x,y*>;
end;

definition
let x, y be real number ;
:: original: |[
redefine func |[x,y]| -> Point of (TOP-REAL 2);
coherence
|[x,y]| is Point of (TOP-REAL 2)
proof end;
end;

theorem :: EUCLID:56
for x, y being real number holds
( |[x,y]| `1 = x & |[x,y]| `2 = y ) by FINSEQ_1:61;

theorem Th57: :: EUCLID:57
for p being Point of (TOP-REAL 2) holds p = |[(p `1),(p `2)]|
proof end;

theorem :: EUCLID:58
0. (TOP-REAL 2) = |[0,0]|
proof end;

theorem Th59: :: EUCLID:59
for p1, p2 being Point of (TOP-REAL 2) holds p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2))]|
proof end;

theorem :: EUCLID:60
for x1, y1, x2, y2 being real number holds |[x1,y1]| + |[x2,y2]| = |[(x1 + x2),(y1 + y2)]|
proof end;

theorem Th61: :: EUCLID:61
for x being real number
for p being Point of (TOP-REAL 2) holds x * p = |[(x * (p `1)),(x * (p `2))]|
proof end;

theorem :: EUCLID:62
for x, x1, y1 being real number holds x * |[x1,y1]| = |[(x * x1),(x * y1)]|
proof end;

theorem Th63: :: EUCLID:63
for p being Point of (TOP-REAL 2) holds - p = |[(- (p `1)),(- (p `2))]|
proof end;

theorem :: EUCLID:64
for x1, y1 being real number holds - |[x1,y1]| = |[(- x1),(- y1)]|
proof end;

theorem Th65: :: EUCLID:65
for p1, p2 being Point of (TOP-REAL 2) holds p1 - p2 = |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2))]|
proof end;

theorem :: EUCLID:66
for x1, y1, x2, y2 being real number holds |[x1,y1]| - |[x2,y2]| = |[(x1 - x2),(y1 - y2)]|
proof end;

theorem :: EUCLID:67
for n being Nat
for P being Subset of (TOP-REAL n)
for Q being non empty Subset of (Euclid n) st P = Q holds
(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q)
proof end;

theorem :: EUCLID:68
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2 ;

theorem :: EUCLID:69
for n being Nat
for x being real number
for p being Point of (TOP-REAL n)
for r being real-valued Function st p = r holds
x * p = x (#) r ;

theorem Th70: :: EUCLID:70
for n being Nat holds 0.REAL n = 0. (TOP-REAL n)
proof end;

theorem :: EUCLID:71
for n being Nat holds the carrier of (Euclid n) = the carrier of (TOP-REAL n)
proof end;

theorem :: EUCLID:72
for n being Nat
for p1 being Point of (TOP-REAL n)
for r1 being real-valued Function st p1 = r1 holds
- p1 = - r1 ;

theorem :: EUCLID:73
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 - p2 = r1 - r2 ;

theorem :: EUCLID:74
for n being Nat holds 0. (TOP-REAL n) = 0* n by Th70;

theorem :: EUCLID:75
for n being Nat
for p being Point of (TOP-REAL n) holds |.(- p).| = |.p.| by Th13;

registration
let n be Nat;
let D be set ;
cluster n -tuples_on D -> FinSequence-membered ;
coherence
n -tuples_on D is FinSequence-membered
proof end;
end;

registration
let n be Nat;
cluster REAL n -> FinSequence-membered ;
coherence
REAL n is FinSequence-membered ;
end;

registration
let n be Nat;
cluster REAL n -> real-functions-membered ;
coherence
REAL n is real-functions-membered
proof end;
end;