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


definition
let n be Nat;
func REAL n -> FinSequenceSet of REAL equals :: EUCLID:def 1
n -tuples_on REAL;
coherence
n -tuples_on REAL is FinSequenceSet 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 REAL n -> non empty ;
coherence
not REAL n is empty ;
end;

registration
let n be Nat;
cluster -> n -element for 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 holds it . r = |.r.|;
existence
ex b1 being Function of REAL,REAL st
for r being Real holds b1 . r = |.r.|
proof end;
uniqueness
for b1, b2 being Function of REAL,REAL st ( for r being Real holds b1 . r = |.r.| ) & ( for r being Real holds b2 . r = |.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 holds b1 . r = |.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 |-> (In (0,REAL));
coherence
n |-> (In (0,REAL)) is real-valued FinSequence ;
end;

:: deftheorem defines 0* EUCLID:def 4 :
for n being Nat holds 0* n = n |-> (In (0,REAL));

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;
:: 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:113;
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:113;
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));

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

theorem :: EUCLID:1
canceled;

theorem :: EUCLID:2
canceled;

theorem :: EUCLID:3
canceled;

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

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

theorem Th3: :: EUCLID:6
for r being Real
for f being real-valued FinSequence holds abs (r * f) = |.r.| * (abs f) by RFUNCT_1:25;

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

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

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

theorem Th6: :: EUCLID:9
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 Th6;
end;

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

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

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

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

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

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

theorem Th13: :: EUCLID:16
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 zero by Th13;
end;

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

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

theorem Th16: :: EUCLID:19
for n being Nat
for x, x1, x2 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:20
for x, y being real-valued FinSequence holds sqr (x - y) = sqr (y - x)
proof end;

theorem Th18: :: EUCLID:21
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 Th19: :: EUCLID:22
for n being Nat holds the carrier of (TOP-REAL n) = REAL n
proof end;

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

theorem Th21: :: EUCLID:24
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 by Th21;
end;

registration
let n be Nat;
cluster -> FinSequence-like for 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 for Element of the carrier of (TOP-REAL n);
coherence
for b1 being Point of (TOP-REAL n) holds b1 is real-valued by Th21;
end;

Lm3: 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;

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

registration
let r, s be Real;
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 Lm4;
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 Lm3;
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 for 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:25
for n being Nat
for x being Element of REAL n holds sqr (abs x) = sqr x by Lm2;

theorem :: EUCLID:26
canceled;

theorem :: EUCLID:27
canceled;

theorem :: EUCLID:28
canceled;

theorem :: EUCLID:29
canceled;

theorem :: EUCLID:30
canceled;

theorem :: EUCLID:31
canceled;

theorem :: EUCLID:32
canceled;

theorem :: EUCLID:33
canceled;

theorem :: EUCLID:34
canceled;

theorem :: EUCLID:35
canceled;

theorem :: EUCLID:36
canceled;

theorem :: EUCLID:37
canceled;

theorem :: EUCLID:38
canceled;

theorem :: EUCLID:39
canceled;

theorem :: EUCLID:40
canceled;

theorem :: EUCLID:41
canceled;

theorem :: EUCLID:42
canceled;

theorem :: EUCLID:43
canceled;

theorem :: EUCLID:44
canceled;

theorem :: EUCLID:45
canceled;

theorem :: EUCLID:46
canceled;

theorem :: EUCLID:47
canceled;

theorem :: EUCLID:48
canceled;

theorem :: EUCLID:49
canceled;

theorem :: EUCLID:50
canceled;

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

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

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

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

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

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

theorem :: EUCLID:52
for x, y being Real holds
( |[x,y]| `1 = x & |[x,y]| `2 = y ) by FINSEQ_1:44;

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

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

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

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

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

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

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

theorem :: EUCLID:60
for x1, y1 being Real holds - |[x1,y1]| = |[(- x1),(- y1)]|
proof end;

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

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

theorem :: EUCLID:63
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;

:: to enable the 03.2009. revision A.T.
theorem :: EUCLID:64
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:65
for n being Nat
for x being Real
for p being Point of (TOP-REAL n)
for r being real-valued Function st p = r holds
x * p = x (#) r ;

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

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

theorem :: EUCLID:68
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:69
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:70
for n being Nat holds 0. (TOP-REAL n) = 0* n by Th38;

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

registration
let n be Nat;
let D be set ;
cluster n -tuples_on D -> FinSequence-membered ;
coherence
n -tuples_on D is FinSequence-membered ;
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;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

definition
let n be Nat;
func 1* n -> FinSequence of REAL equals :: EUCLID:def 11
n |-> 1;
coherence
n |-> 1 is FinSequence of REAL
proof end;
end;

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

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

definition
let n be Nat;
func 1.REAL n -> Point of (TOP-REAL n) equals :: EUCLID:def 12
 1* n;
coherence
1* n is Point of (TOP-REAL n) by Th19;
end;

:: deftheorem defines 1.REAL EUCLID:def 12 :
for n being Nat holds 1.REAL n = 1* n;

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

theorem Th45: :: EUCLID:73
for n being Nat holds |.(1* n).| = sqrt n
proof end;

theorem :: EUCLID:74
for n being Nat holds |.(1.REAL n).| = sqrt n by Th45;

theorem :: EUCLID:75
for n being Nat st 1 <= n holds
1 <= |.(1.REAL n).|
proof end;

theorem :: EUCLID:76
for f being FinSequence of REAL holds
( f is Element of REAL (len f) & f is Point of (TOP-REAL (len f)) )
proof end;

theorem :: EUCLID:77
REAL 0 = {(0. (TOP-REAL 0))}
proof end;