Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### The Euclidean Space

by
Agata Darmochwal

MML identifier: EUCLID
[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM, FINSEQ_2, FINSEQ_1, FUNCT_1, ABSVALUE, ARYTM_1, RVSUM_1,
COMPLEX1, SQUARE_1, RLVECT_1, RELAT_1, PCOMPS_1, METRIC_1, PRE_TOPC,
FUNCT_2, ARYTM_3, MCART_1, EUCLID, BOOLE;
notation XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
NAT_1, DOMAIN_1, FUNCT_1, STRUCT_0, METRIC_1, FUNCT_2, REAL_1, ABSVALUE,
FINSEQ_1, FINSEQ_2, FINSEQOP, FRAENKEL, SQUARE_1, RVSUM_1, PRE_TOPC,
PCOMPS_1;
constructors DOMAIN_1, REAL_1, ABSVALUE, FINSEQOP, FRAENKEL, SQUARE_1,
RVSUM_1, PCOMPS_1, SEQ_1, MEMBERED, PARTFUN1, XBOOLE_0;
clusters METRIC_1, FINSEQ_2, PCOMPS_1, RELSET_1, XREAL_0, FINSEQ_1, ARYTM_3,
SQUARE_1, SEQ_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;

begin

reserve k,j,n for Nat, r for real number;

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

reserve x for FinSequence of REAL;

definition
func absreal -> Function of REAL,REAL means
:: EUCLID:def 2
for r holds it.r = abs r;
end;

definition let x;
func abs x -> FinSequence of REAL equals
:: EUCLID:def 3
absreal*x;
end;

definition let n;
func 0*n -> FinSequence of REAL equals
:: EUCLID:def 4
n |-> (0 qua Real);
end;

definition let n;
redefine func 0*n -> Element of REAL n;
end;

reserve x,x1,x2,y,z for Element of REAL n;

definition let n,x;
redefine func -x -> Element of REAL n;
end;

definition let n,x,y;
redefine func x + y -> Element of REAL n;
func x - y -> Element of REAL n;
end;

definition let n; let r be real number; let x;
redefine func r*x -> Element of REAL n;
end;

definition let n,x;
redefine func abs x -> Element of n-tuples_on REAL;
end;

definition let n,x;
redefine func sqr x -> Element of n-tuples_on REAL;
end;

definition let x be FinSequence of REAL;
func |.x.| -> Real equals
:: EUCLID:def 5
sqrt Sum sqr x;
end;

canceled;

theorem :: EUCLID:2
len x = n;

theorem :: EUCLID:3
dom x = Seg n;

theorem :: EUCLID:4
x.k in REAL;

theorem :: EUCLID:5
(for k st k in Seg n holds x1.k = x2.k) implies x1 = x2;

theorem :: EUCLID:6
r = x.k implies (abs x).k = abs r;

theorem :: EUCLID:7
abs 0*n = n |-> (0 qua Real);

theorem :: EUCLID:8
abs -x = abs x;

theorem :: EUCLID:9
abs(r*x) = abs(r)*(abs x);

theorem :: EUCLID:10
|.0*n.| = 0;

theorem :: EUCLID:11
|.x.| = 0 implies x = 0*n;

theorem :: EUCLID:12
|.x.| >= 0;

theorem :: EUCLID:13
|.-x.| = |.x.|;

theorem :: EUCLID:14
|.r*x.| = abs(r)*|.x.|;

theorem :: EUCLID:15
|.x1 + x2.| <= |.x1.| + |.x2.|;

theorem :: EUCLID:16
|.x1 - x2.| <= |.x1.| + |.x2.|;

theorem :: EUCLID:17
|.x1.| - |.x2.| <= |.x1 + x2.|;

theorem :: EUCLID:18
|.x1.| - |.x2.| <= |.x1 - x2.|;

theorem :: EUCLID:19
|.x1 - x2.| = 0 iff x1 = x2;

theorem :: EUCLID:20
x1 <> x2 implies |.x1 - x2.| > 0;

theorem :: EUCLID:21
|.x1 - x2.| = |.x2 - x1.|;

theorem :: EUCLID:22
|.x1 - x2.| <= |.x1 - x.| + |.x - x2.|;

definition let n;
func Pitag_dist n -> Function of [:REAL n,REAL n:],REAL means
:: EUCLID:def 6
for x,y being Element of REAL n holds it.(x,y) = |.x-y.|;
end;

theorem :: EUCLID:23
sqr(x-y) = sqr(y-x);

theorem :: EUCLID:24
Pitag_dist n is_metric_of REAL n;

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

definition let n;
cluster Euclid n -> non empty;
end;

definition let n;
func TOP-REAL n -> strict TopSpace equals
:: EUCLID:def 8
TopSpaceMetr (Euclid n);
end;

definition let n;
cluster TOP-REAL n -> non empty;
end;

reserve p,p1,p2,p3 for Point of TOP-REAL n,
x,x1,x2,y,y1,y2 for real number;

theorem :: EUCLID:25
the carrier of TOP-REAL n = REAL n;

theorem :: EUCLID:26
p is Function of Seg n, REAL;

theorem :: EUCLID:27
p is FinSequence of REAL;

theorem :: EUCLID:28
for f being FinSequence st f = p holds len f = n;

definition let n;
func 0.REAL n -> Point of TOP-REAL n equals
:: EUCLID:def 9
0*n;
end;

definition let n,p1,p2;
func p1 + p2 -> Point of TOP-REAL n means
:: EUCLID:def 10
for p1',p2' being Element of REAL n st p1' = p1 & p2' = p2
holds it = p1' + p2';
commutativity;
end;

theorem :: EUCLID:29
for x being Element of REAL n holds sqr abs x = sqr x;

theorem :: EUCLID:30
p1 + p2 + p3 = p1 + (p2 + p3);

theorem :: EUCLID:31
0.REAL n + p = p & p + 0.REAL n = p;

definition let x,n,p;
func x*p -> Point of TOP-REAL n means
:: EUCLID:def 11
for p' being Element of REAL n st p' = p holds it = x*p';
end;

theorem :: EUCLID:32
x*0.REAL n = 0.REAL n;

theorem :: EUCLID:33
1*p = p & 0 * p = 0.REAL n;

theorem :: EUCLID:34
(x*y)*p = x*(y*p);

theorem :: EUCLID:35
x*p = 0.REAL n implies x = 0 or p = 0.REAL n;

theorem :: EUCLID:36
x*(p1 + p2) = x*p1 + x*p2;

theorem :: EUCLID:37
(x + y)*p = x*p + y*p;

theorem :: EUCLID:38
x*p1 = x*p2 implies x = 0 or p1 = p2;

definition let n,p;
func -p -> Point of TOP-REAL n means
:: EUCLID:def 12
for p' being Element of REAL n st p' = p holds it = -p';
end;

theorem :: EUCLID:39
--p = p;

theorem :: EUCLID:40
p + -p = 0.REAL n;

theorem :: EUCLID:41
p1 + p2 = 0.REAL n implies p1 = -p2 & p2 = -p1;

theorem :: EUCLID:42
-(p1 + p2) = -p1 + -p2;

theorem :: EUCLID:43
-p = (-1)*p;

theorem :: EUCLID:44
-x*p = (-x)*p & -x*p = x*(-p);

definition let n,p1,p2;
func p1 - p2 -> Point of TOP-REAL n means
:: EUCLID:def 13
for p1',p2' being Element of REAL n st p1' = p1 & p2' = p2
holds it = p1' - p2';
end;

theorem :: EUCLID:45
p1 - p2 = p1 + -p2;

theorem :: EUCLID:46
p - p = 0.REAL n;

theorem :: EUCLID:47
p1 - p2 = 0.REAL n implies p1 = p2;

theorem :: EUCLID:48
-(p1 - p2) = p2 - p1 & -(p1 - p2) = -p1 + p2;

theorem :: EUCLID:49
p1 + (p2 - p3) = p1 + p2 - p3;

theorem :: EUCLID:50
p1 - (p2 + p3) = p1 - p2 - p3;

theorem :: EUCLID:51
p1 - (p2 - p3) = p1 - p2 + p3;

theorem :: EUCLID:52
p = p + p1 - p1 & p = p - p1 + p1;

theorem :: EUCLID:53
x*(p1 - p2) = x*p1 - x*p2;

theorem :: EUCLID:54
(x-y)*p = x*p - y*p;

reserve p,p1,p2 for Point of TOP-REAL 2;

theorem :: EUCLID:55
ex x,y being Real st p=<*x,y*>;

definition let p;
func p`1 -> Real means
:: EUCLID:def 14
for f being FinSequence st p = f holds it = f.1;
func p`2 -> Real means
:: EUCLID:def 15
for f being FinSequence st p = f holds it = f.2;
end;

definition let x,y be real number;
func |[ x,y ]| -> Point of TOP-REAL 2 equals
:: EUCLID:def 16
<*x,y*>;
end;

theorem :: EUCLID:56
|[x,y]|`1 = x & |[x,y]|`2 = y;

theorem :: EUCLID:57
p = |[p`1, p`2]|;

theorem :: EUCLID:58
0.REAL 2 = |[0,0]|;

theorem :: EUCLID:59
p1 + p2 = |[ p1`1 + p2`1, p1`2 + p2`2]|;

theorem :: EUCLID:60
|[x1, y1]| + |[x2, y2]| = |[ x1 + x2, y1 + y2]|;

theorem :: EUCLID:61
x*p = |[ x*p`1 ,x*p`2 ]|;

theorem :: EUCLID:62
x*|[x1,y1]| = |[ x*x1 ,x*y1 ]|;

theorem :: EUCLID:63
-p = |[ -p`1, -p`2]|;

theorem :: EUCLID:64
-|[x1,y1]| = |[ -x1, -y1]|;

theorem :: EUCLID:65
p1 - p2 = |[ p1`1 - p2`1, p1`2 - p2`2]|;

theorem :: EUCLID:66
|[x1, y1]| - |[x2, y2]| = |[ x1 - x2, y1 - y2]|;
```