Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Lines in \$n\$-Dimensional Euclidean Spaces

by
Akihiro Kubo

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

```environ

vocabulary EUCLID, FINSEQ_1, FUNCT_1, PRE_TOPC, ARYTM_1, ARYTM_3, COMPLEX1,
ABSVALUE, ARYTM, INCSP_1, FINSEQ_2, AFF_1, EUCLID_2, BHSP_1, SQUARE_1,
SEQ_4, SEQ_2, EUCLID_4;
notation TARSKI, XBOOLE_0, FINSEQ_2, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, NAT_1, FUNCT_2, ABSVALUE, STRUCT_0, PRE_TOPC, FINSEQ_1,
RVSUM_1, EUCLID_2, SQUARE_1, EUCLID, SEQ_4;
constructors REAL_1, ABSVALUE, FINSEQOP, EUCLID_2, SEQ_4, SQUARE_1;
clusters RELSET_1, STRUCT_0, EUCLID, XREAL_0, NAT_1, MEMBERED;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;

begin

reserve a,b,r,s,t,u,v,lambda for Real, i,j,n for Nat;
reserve x,x1,x2,x3,y,y1,y2 for Element of REAL n;

theorem :: EUCLID_4:1   :: EUCLID:31
0 * x + x = x & x + 0*n = x;

theorem :: EUCLID_4:2  :: EUCLID:32
a*(0*n) = 0*n;

theorem :: EUCLID_4:3    :: EUCLID:33
1*x = x & 0 * x = 0*n;

theorem :: EUCLID_4:4  :: EUCLID:34
(a*b)*x = a*(b*x);

theorem :: EUCLID_4:5 :: EUCLID:35
a*x = 0*n implies a = 0 or x = 0*n;

theorem :: EUCLID_4:6  :: EUCLID:36
a*(x1 + x2) = a*x1 + a*x2;

theorem :: EUCLID_4:7  :: EUCLID:37
(a + b)*x = a*x + b*x;

theorem :: EUCLID_4:8 :: EUCLID:38
a*x1 = a*x2 implies a = 0 or x1 = x2;

definition let n; let x1,x2 be Element of REAL n;
func Line(x1,x2) -> Subset of REAL n equals
:: EUCLID_4:def 1
{ (1-lambda)*x1 + lambda*x2 : not contradiction };
end;

definition let n; let x1,x2 be Element of REAL n;
cluster Line(x1,x2) -> non empty;
end;

theorem :: EUCLID_4:9   :: AFF_1:25
Line(x1,x2)=Line(x2,x1);

definition let n;let x1,x2 be Element of REAL n;
redefine func Line(x1,x2);
commutativity;
end;

theorem :: EUCLID_4:10  :: AFF_1:26
x1 in Line(x1,x2) & x2 in Line(x1,x2);

theorem :: EUCLID_4:11  :: AFF_1:27
y1 in Line(x1,x2) & y2 in Line(x1,x2) implies
Line(y1,y2) c= Line(x1,x2);

theorem :: EUCLID_4:12  :: AFF_1:28
y1 in Line(x1,x2) & y2 in Line(x1,x2) & y1<>y2 implies
Line(x1,x2) c= Line(y1,y2);

definition let n; let A be Subset of REAL n;
attr A is being_line means
:: EUCLID_4:def 2       :: AFF_1:def 3
ex x1,x2 st x1<>x2 & A=Line(x1,x2);
synonym A is_line;
end;

theorem :: EUCLID_4:13 :: AFF_1:30
for A,C be Subset of REAL n,x1,x2 holds A is_line & C is_line &
x1 in A & x2 in A & x1 in C & x2 in C implies x1=x2 or A=C;

theorem :: EUCLID_4:14  ::AFF_1:31
for A be Subset of REAL n st
A is_line holds ex x1,x2 st x1 in A & x2 in A & x1<>x2;

theorem :: EUCLID_4:15 :: AFF_1:32
for A be Subset of REAL n st
A is_line holds ex x2 st x1<>x2 & x2 in A;

definition let n;let x be Element of REAL n;
func Rn2Fin (x) -> FinSequence of REAL equals
:: EUCLID_4:def 3
x;
end;

definition let n;let x be Element of REAL n;
func |. x .| -> Real equals
:: EUCLID_4:def 4
|. Rn2Fin(x) .|;
end;

definition let n;let x1,x2 be Element of REAL n;
func |( x1,x2 )| -> Real equals
:: EUCLID_4:def 5
|( Rn2Fin(x1),Rn2Fin(x2) )|;
commutativity;
end;

theorem :: EUCLID_4:16  :: EUCLID_2:10
for x1,x2 being Element of REAL n
holds |(x1,x2)|=1/4*((|.(x1+x2).|)^2-(|.(x1-x2).|)^2);

theorem :: EUCLID_4:17 :: EUCLID_2:11
for x being Element of REAL n holds |(x,x)| >= 0;

theorem :: EUCLID_4:18  :: EUCLID_2:12
for x being Element of REAL n holds (|.x.|)^2=|(x,x)|;

theorem :: EUCLID_4:19  :: EUCLID_2:14
for x being Element of REAL n holds 0 <= |.x.|;

theorem :: EUCLID_4:20 :: EUCLID_2:13
for x being Element of REAL n holds |.x.| = sqrt |(x,x)|;

theorem :: EUCLID_4:21  :: EUCLID_2:16
for x being Element of REAL n holds |(x,x)| = 0 iff |.x.| = 0;

theorem :: EUCLID_4:22  :: EUCLID_2:15
for x being Element of REAL n holds |(x,x)|=0 iff x=0*n;

theorem :: EUCLID_4:23  :: EUCLID_2:17
for x being Element of REAL n holds |(x, 0*n)| = 0;

theorem :: EUCLID_4:24 :: EUCLID_2:18
for x being Element of REAL n holds |(0*n,x)| = 0;

theorem :: EUCLID_4:25  :: EUCLID_2:19
for x1,x2,x3 being Element of REAL n holds
|((x1+x2),x3)| = |(x1,x3)| + |(x2,x3)|;

theorem :: EUCLID_4:26  ::EUCLID_2:20
for x1,x2 being Element of REAL n,a being real number
holds |(a*x1,x2)| = a*|(x1,x2)|;

theorem :: EUCLID_4:27 :: EUCLID_2:21
for x1,x2 being Element of REAL n,a being real number
holds |(x1,a*x2)| = a*|(x1,x2)|;

theorem :: EUCLID_4:28  :: EUCLID_2:22
for x1,x2 being Element of REAL n holds
|(-x1, x2)| = - |(x1, x2)|;

theorem :: EUCLID_4:29 :: EUCLID_2:23
for x1,x2 being Element of REAL n holds
|(x1, -x2)| = - |(x1, x2)|;

theorem :: EUCLID_4:30 :: EUCLID_2:24
for x1,x2 being Element of REAL n holds
|(-x1, -x2)| = |(x1, x2)|;

theorem :: EUCLID_4:31  :: EUCLID_2:25
for x1,x2,x3 being Element of REAL n
holds |(x1-x2, x3)| = |(x1, x3)| - |(x2, x3)|;

theorem :: EUCLID_4:32 :: EUCLID_2:26
for a,b being real number,x1,x2,x3 being Element of REAL n
holds
|( (a*x1+b*x2), x3 )| = a*|(x1,x3)| + b*|(x2,x3)|;

theorem :: EUCLID_4:33 :: EUCLID_2:27
for x1,y1,y2 being Element of REAL n holds
|(x1, y1+y2)| = |(x1, y1)| + |(x1, y2)|;

theorem :: EUCLID_4:34 :: EUCLID_2:28
for x1,y1,y2 being Element of REAL n holds
|(x1, y1-y2)| = |(x1, y1)| - |(x1, y2)|;

theorem :: EUCLID_4:35  :: EUCLID_2:29
for x1,x2,y1,y2 being Element of REAL n holds
|(x1+x2, y1+y2)| = |(x1, y1)| + |(x1, y2)| + |(x2, y1)| + |(x2, y2)|;

theorem :: EUCLID_4:36  :: EUCLID_2:30
for x1,x2,y1,y2 being Element of REAL n holds
|(x1-x2, y1-y2)| = |(x1, y1)| - |(x1, y2)| - |(x2, y1)| + |(x2, y2)|;

theorem :: EUCLID_4:37  :: EUCLID_2:31
for x,y being Element of REAL n holds
|(x+y, x+y)| = |(x, x)| + 2*|(x, y)| + |(y, y)|;

theorem :: EUCLID_4:38  :: EUCLID_2:32
for x,y being Element of REAL n holds
|(x-y, x-y)| = |(x, x)| - 2*|(x, y)| + |(y, y)|;

theorem :: EUCLID_4:39 :: EUCLID_2:33
for x,y being Element of REAL n holds
|.x+y.|^2 = |.x.|^2 + 2*|(x, y)| + |.y.|^2;

theorem :: EUCLID_4:40 :: EUCLID_2:34
for x,y being Element of REAL n holds
|.x-y.|^2 = |.x.|^2 - 2*|(x, y)| + |.y.|^2;

theorem :: EUCLID_4:41 :: EUCLID_2:35
for x,y being Element of REAL n holds
|.x+y.|^2 + |.x-y.|^2 = 2*(|.x.|^2 + |.y.|^2);

theorem :: EUCLID_4:42 :: EUCLID_2:36
for x,y being Element of REAL n holds
|.x+y.|^2 - |.x-y.|^2 = 4* |(x,y)|;

theorem :: EUCLID_4:43 :: EUCLID_2:37  :: Schwartz
for x,y being Element of REAL n holds
abs |(x,y)| <= |.x.|*|.y.|;

theorem :: EUCLID_4:44 :: EUCLID_2:38 :: Triangle
for x,y being Element of REAL n holds
|.x+y.| <= |.x.| + |.y.|;

definition let n;let x1, x2 be Element of REAL n;
pred x1,x2 are_orthogonal means
:: EUCLID_4:def 6
:: EUCLID_2:def 3
|(x1,x2)| = 0;
symmetry;
end;

theorem :: EUCLID_4:45
for R being Subset of REAL,x1,x2,y1 being Element of REAL n st
R={|.y1-x.| where x is Element of REAL n: x in Line(x1,x2)}
holds ex y2 being Element of REAL n st y2 in Line(x1,x2) &
|.y1-y2.|=lower_bound R & x1-x2,y1-y2 are_orthogonal;

definition let n; let p1,p2 be Point of TOP-REAL n;
func Line(p1,p2) -> Subset of TOP-REAL n equals
:: EUCLID_4:def 7
{ (1-lambda)*p1 + lambda*p2 : not contradiction };
end;

definition let n; let p1,p2 be Point of TOP-REAL n;
cluster Line(p1,p2) -> non empty;
end;

reserve p,p1,p2,q1,q2 for Point of TOP-REAL n;

theorem :: EUCLID_4:46  :: AFF_1:25
Line(p1,p2)=Line(p2,p1);

definition let n;let p1,p2 be Point of TOP-REAL n;
redefine func Line(p1,p2);
commutativity;
end;

theorem :: EUCLID_4:47  :: AFF_1:26
p1 in Line(p1,p2) & p2 in Line(p1,p2);

theorem :: EUCLID_4:48  :: AFF_1:27
q1 in Line(p1,p2) & q2 in Line(p1,p2) implies
Line(q1,q2) c= Line(p1,p2);

theorem :: EUCLID_4:49  :: AFF_1:28
q1 in Line(p1,p2) & q2 in Line(p1,p2) & q1<>q2 implies
Line(p1,p2) c= Line(q1,q2);

definition let n; let A be Subset of TOP-REAL n;
attr A is being_line means
:: EUCLID_4:def 8
:: AFF_1:def 3
ex p1,p2 st p1<>p2 & A=Line(p1,p2);
synonym A is_line;
end;

theorem :: EUCLID_4:50 :: AFF_1:30
for A,C being Subset of TOP-REAL n holds A is_line & C is_line &
p1 in A & p2 in A & p1 in C & p2 in C implies p1=p2 or A=C;

theorem :: EUCLID_4:51  :: AFF_1:31
for A being Subset of TOP-REAL n st
A is_line holds ex p1,p2 st p1 in A & p2 in A & p1<>p2;

theorem :: EUCLID_4:52 :: AFF_1:32
for A being Subset of TOP-REAL n st
A is_line holds ex p2 st p1<>p2 & p2 in A;

definition let n;let p be Point of TOP-REAL n;
func TPn2Rn (p) -> Element of REAL n
equals
:: EUCLID_4:def 9
p;
end;

definition let n;let p be Point of TOP-REAL n;
func |. p .| -> Real equals
:: EUCLID_4:def 10
|. TPn2Rn(p) .|;
end;

definition let n;let p1,p2 be Point of TOP-REAL n;
func |( p1,p2 )| -> Real equals
:: EUCLID_4:def 11
|( TPn2Rn(p1),TPn2Rn(p2) )|;
commutativity;
end;

definition let n;let p1, p2 be Point of TOP-REAL n;
pred p1,p2 are_orthogonal means
:: EUCLID_4:def 12    :: EUCLID_2:def 3
|(p1,p2)| = 0;
symmetry;
end;

theorem :: EUCLID_4:53
for R being Subset of REAL,p1,p2,q1 being Point of TOP-REAL n
st R={|. q1-p .| where p is Point of TOP-REAL n: p in Line(p1,p2)}
holds ex q2 being Point of TOP-REAL n st q2 in Line(p1,p2) &
|. q1-q2 .| =lower_bound R & p1-p2,q1-q2 are_orthogonal;
```