:: The Euclidean Space
:: by Agata Darmochwa{\l}
::
:: 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 ;
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 ;
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 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),() #);
coherence
MetrStruct(# (REAL n),() #) is strict MetrSpace
proof end;
end;

:: deftheorem defines Euclid EUCLID:def 7 :
for n being Nat holds Euclid n = MetrStruct(# (REAL 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 () & 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 () & 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 () & 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 () & 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 () & 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
proof end;
end;

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

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

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

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

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

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

Lm4: for n being Nat
for p1, p2 being Point of ()
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 ()
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 ();
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 ();
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 ();
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 ();
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 ();
coherence
for b1 being Point of () 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 ();
coherence
0* n is Point of ()
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 () holds (p1 + p2) + p3 = p1 + (p2 + p3) by RLVECT_1:def 6;

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

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

theorem :: EUCLID:33
for n being Nat
for p being Point of () holds
( 1 * p = p & 0 * p = 0. () ) by ;

theorem :: EUCLID:34
for n being Nat
for p being Point of ()
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 ()
for x being real number holds
( not x * p = 0. () or x = 0 or p = 0. () ) by RLVECT_1:24;

theorem :: EUCLID:36
for n being Nat
for p1, p2 being Point of ()
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 ()
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 ()
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 () holds - (- p) = p ;

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

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

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

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

theorem :: EUCLID:44
for n being Nat
for p being Point of ()
for x being real number holds
( - (x * p) = (- x) * p & - (x * p) = x * (- p) ) by ;

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

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

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

theorem :: EUCLID:48
for n being Nat
for p1, p2 being Point of () 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 () 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 () 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 () holds p1 - (p2 - p3) = (p1 - p2) + p3 by RLVECT_1:43;

theorem :: EUCLID:52
for n being Nat
for p, p1 being Point of () 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 ()
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 ()
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 () ex x, y being Real st p = <*x,y*>
proof end;

definition
canceled;
canceled;
canceled;
canceled;
canceled;
let p be Point of ();
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 () holds p `1 = p . 1;

:: deftheorem defines `2 EUCLID:def 15 :
for p being Point of () 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 ();
coherence
|[x,y]| is Point of ()
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 () holds p = |[(p `1),(p `2)]|
proof end;

theorem :: EUCLID:58
0. () =
proof end;

theorem Th59: :: EUCLID:59
for p1, p2 being Point of () 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 () 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 () 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 () 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 ()
for Q being non empty Subset of () st P = Q holds
() | P = TopSpaceMetr (() | Q)
proof end;

theorem :: EUCLID:68
for n being Nat
for p1, p2 being Point of ()
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 ()
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. ()
proof end;

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

theorem :: EUCLID:72
for n being Nat
for p1 being Point of ()
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 ()
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. () = 0* n by Th70;

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

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

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

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