:: Lines in $n$-Dimensional Euclidean Spaces :: by Akihiro Kubo :: :: Received August 8, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies REAL_1, NAT_1, SUBSET_1, NUMBERS, CARD_1, RELAT_1, ARYTM_3, EUCLID, FINSEQ_2, COMPLEX1, ARYTM_1, INCSP_1, TARSKI, XBOOLE_0, AFF_1, SQUARE_1, RVSUM_1, FINSEQ_1, XXREAL_0, PRE_TOPC, SEQ_4, XXREAL_2, STRUCT_0; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_2, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, STRUCT_0, PRE_TOPC, FINSEQ_1, FINSEQ_2, RVSUM_1, SQUARE_1, RLVECT_1, EUCLID, SEQ_4, XXREAL_0, RLTOPSP1; constructors REAL_1, SQUARE_1, BINOP_2, COMPLEX1, SEQ_4, FINSEQOP, MONOID_0, EUCLID, RELSET_1, BINOP_1; registrations RELSET_1, NUMBERS, XREAL_0, BINOP_2, MEMBERED, MONOID_0, EUCLID, VALUED_0, VALUED_1, SQUARE_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve a,b,s,t,u,lambda for Real, n for Nat; reserve x,x1,x2,x3,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 the set of all (1-lambda)*x1 + lambda*x2 ; end; registration let n; let x1,x2 be Element of REAL n; cluster Line(x1,x2) -> non empty; end; definition let n; let x1,x2 be Element of REAL n; redefine func Line(x1,x2); commutativity; end; theorem :: EUCLID_4:9 :: AFF_1:26 x1 in Line(x1,x2) & x2 in Line(x1,x2); theorem :: EUCLID_4:10 :: AFF_1:27 y1 in Line(x1,x2) & y2 in Line(x1,x2) implies Line(y1,y2) c= Line(x1,x2); theorem :: EUCLID_4:11 :: 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); end; theorem :: EUCLID_4:12 :: AFF_1:30 for A,C be Subset of REAL n,x1,x2 holds A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C implies x1=x2 or A=C; theorem :: EUCLID_4:13 ::AFF_1:31 for A be Subset of REAL n st A is being_line holds ex x1,x2 st x1 in A & x2 in A & x1<>x2; theorem :: EUCLID_4:14 :: AFF_1:32 for A be Subset of REAL n st A is being_line holds ex x2 st x1<>x2 & x2 in A; theorem :: EUCLID_4:15 :: EUCLID_2:13 for x being Element of REAL n holds |.x.| = sqrt |(x,x)|; theorem :: EUCLID_4:16 :: EUCLID_2:16 for x being Element of REAL n holds |(x,x)| = 0 iff |.x.| = 0; theorem :: EUCLID_4:17 :: EUCLID_2:15 for x being Element of REAL n holds |(x,x)|=0 iff x=0*n; theorem :: EUCLID_4:18 :: EUCLID_2:17 for x being Element of REAL n holds |(x, 0*n)| = 0; theorem :: EUCLID_4:19 :: EUCLID_2:18 for x being Element of REAL n holds |(0*n,x)| = 0; theorem :: EUCLID_4:20 :: EUCLID_2:19 for x1,x2,x3 being Element of REAL n holds |((x1+x2),x3)| = |(x1 ,x3)| + |(x2,x3)|; theorem :: EUCLID_4:21 ::EUCLID_2:20 for x1,x2 being Element of REAL n,a being Real holds |(a* x1,x2)| = a*|(x1,x2)|; theorem :: EUCLID_4:22 :: EUCLID_2:21 for x1,x2 being Element of REAL n,a being Real holds |(x1,a*x2 )| = a*|(x1,x2)|; theorem :: EUCLID_4:23 :: EUCLID_2:22 for x1,x2 being Element of REAL n holds |(-x1, x2)| = - |(x1, x2 )|; theorem :: EUCLID_4:24 :: EUCLID_2:23 for x1,x2 being Element of REAL n holds |(x1, -x2)| = - |(x1, x2)|; theorem :: EUCLID_4:25 :: EUCLID_2:24 for x1,x2 being Element of REAL n holds |(-x1, -x2)| = |(x1, x2)|; theorem :: EUCLID_4:26 :: EUCLID_2:25 for x1,x2,x3 being Element of REAL n holds |(x1-x2, x3)| = |(x1, x3)| - |(x2, x3)|; theorem :: EUCLID_4:27 :: EUCLID_2:26 for a,b being Real,x1,x2,x3 being Element of REAL n holds |( (a *x1+b*x2), x3 )| = a*|(x1,x3)| + b*|(x2,x3)|; theorem :: EUCLID_4:28 :: EUCLID_2:27 for x1,y1,y2 being Element of REAL n holds |(x1, y1+y2)| = |(x1, y1)| + |(x1, y2)|; theorem :: EUCLID_4:29 :: EUCLID_2:28 for x1,y1,y2 being Element of REAL n holds |(x1, y1-y2)| = |(x1, y1)| - |(x1, y2)|; theorem :: EUCLID_4:30 :: 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:31 :: 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:32 :: 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:33 :: 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:34 :: 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:35 :: 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:36 :: 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:37 :: EUCLID_2:36 for x,y being Element of REAL n holds |.x+y.|^2 - |.x-y.|^2 = 4* |(x,y )|; theorem :: EUCLID_4:38 :: EUCLID_2:37 :: Schwartz for x,y being Element of REAL n holds |.|(x,y)|.| <= |.x.|*|.y.|; ::$CT theorem :: EUCLID_4:40 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)} 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 ::$CD end; reserve p1,p2,q1,q2 for Point of TOP-REAL n; theorem :: EUCLID_4:41 :::Th40: :: AFF_1:26 p1 in Line(p1,p2) & p2 in Line(p1,p2); theorem :: EUCLID_4:42 :::Th41: :: AFF_1:27 q1 in Line(p1,p2) & q2 in Line(p1,p2) implies Line(q1,q2) c= Line(p1,p2); theorem :: EUCLID_4:43 :::Th42: :: 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 4 :: AFF_1:def 3 ex p1,p2 st p1<>p2 & A=Line(p1,p2); end; theorem :: EUCLID_4:44 :: AFF_1:30 for A,C being Subset of TOP-REAL n holds A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C implies p1=p2 or A=C; theorem :: EUCLID_4:45 :: AFF_1:31 for A being Subset of TOP-REAL n st A is being_line holds ex p1, p2 st p1 in A & p2 in A & p1<>p2; theorem :: EUCLID_4:46 :: AFF_1:32 for A being Subset of TOP-REAL n st A is being_line holds ex p2 st p1 <>p2 & p2 in A; theorem :: EUCLID_4:47 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)} 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;