The Mizar abstract of EUCLID

Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users
The abstract of the Mizar article:: Lines in $n$-Dimensional Euclidean Spaces
by
Akihiro Kubo
Received August 8, 2003
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;
The abstract of the Mizar article:

Lines in $n$-Dimensional Euclidean Spaces
