:: Lines on Planes in $n$-Dimensional Euclidean Spaces :: by Akihiro Kubo :: :: Received May 24, 2005 :: Copyright (c) 2005-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 NUMBERS, REAL_1, SUBSET_1, ARYTM_3, RELAT_1, ARYTM_1, EUCLID, COMPLEX1, CARD_1, RVSUM_1, XXREAL_0, JORDAN2C, FINSEQ_1, FINSEQ_2, FUNCT_1, AFF_1, INCSP_1, TARSKI, ANALOAF, EUCLID_3, SQUARE_1, SYMSP_1, SETFAM_1, ZFMISC_1, XBOOLE_0, METRIC_1, SEQ_4, XXREAL_2, AFF_4, EUCLIDLP, NAT_1; notations ORDINAL1, ZFMISC_1, FUNCT_1, SEQ_4, TARSKI, SETFAM_1, XBOOLE_0, XXREAL_0, XXREAL_2, XCMPLX_0, XREAL_0, NUMBERS, REAL_1, SUBSET_1, FINSEQ_1, FINSEQ_2, SQUARE_1, RVSUM_1, EUCLID, EUCLID_4; constructors REAL_1, SQUARE_1, SEQ_4, FINSEQOP, EUCLID_4, RVSUM_1, BINOP_2; registrations SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, EUCLID, VALUED_0, SQUARE_1, ORDINAL1; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin reserve a,a1,a2,a3,b,b1,b2,b3,r,s,t,u for Real; reserve n for Nat; reserve x0,x,x1,x2,x3,y0,y,y1,y2,y3 for Element of REAL n; :: Preliminaries theorem :: EUCLIDLP:1 (s/t)*(u*x)=(s*u)/t*x & (1/t)*(u*x)= u/t*x; theorem :: EUCLIDLP:2 x - x = 0*n & x + -x = 0*n; theorem :: EUCLIDLP:3 -a*x = (-a)*x & -a*x = a*(-x); theorem :: EUCLIDLP:4 x1 - (x2 - x3) = x1 - x2 + x3; theorem :: EUCLIDLP:5 x1 + (x2 - x3) = x1 + x2 - x3; theorem :: EUCLIDLP:6 x1 = x2 + x3 iff x2 = x1 - x3; theorem :: EUCLIDLP:7 x=x1+x2+x3 iff x-x1=x2+x3; theorem :: EUCLIDLP:8 -(x1 + x2 + x3) = -x1 + -x2 + -x3; theorem :: EUCLIDLP:9 x1=x2 iff x1-x2=0*n; theorem :: EUCLIDLP:10 x1 - x0 = t*x & x1 <> x0 implies t <> 0; theorem :: EUCLIDLP:11 (a - b)*x = a*x + (-b)*x & (a - b)*x = a*x + -b*x & (a - b)*x = a*x - b*x; theorem :: EUCLIDLP:12 a*(x - y) = a*x + -a*y & a*(x - y) = a*x + (-a)*y & a*(x - y) = a*x - a*y; theorem :: EUCLIDLP:13 (s - t - u)*x = s*x - t*x - u*x; theorem :: EUCLIDLP:14 x - (a1*x1+a2*x2+a3*x3) = x + ((-a1)*x1 + (-a2)*x2 + (-a3)*x3); theorem :: EUCLIDLP:15 x - (s+t+u)*y = x + (-s)*y + (-t)*y + (-u)*y; theorem :: EUCLIDLP:16 (x1+x2)+(y1+y2)=(x1+y1)+(x2+y2); theorem :: EUCLIDLP:17 (x1+x2+x3)+(y1+y2+y3)=(x1+y1)+(x2+y2)+(x3+y3); theorem :: EUCLIDLP:18 (x1+x2)-(y1+y2)=(x1-y1)+(x2-y2); theorem :: EUCLIDLP:19 (x1+x2+x3)-(y1+y2+y3)=(x1-y1)+(x2-y2)+(x3-y3); theorem :: EUCLIDLP:20 a*(x1+x2+x3)=a*x1+a*x2+a*x3; theorem :: EUCLIDLP:21 a*(b1*x1+b2*x2) = (a*b1)*x1+(a*b2)*x2; theorem :: EUCLIDLP:22 a*(b1*x1+b2*x2+b3*x3) = (a*b1)*x1+(a*b2)*x2+(a*b3)*x3; theorem :: EUCLIDLP:23 (a1*x1+a2*x2)+(b1*x1+b2*x2)=(a1+b1)*x1+(a2+b2)*x2; theorem :: EUCLIDLP:24 (a1*x1+a2*x2+a3*x3)+(b1*x1+b2*x2+b3*x3)=(a1+b1)*x1+(a2+b2)*x2+( a3+b3)*x3; theorem :: EUCLIDLP:25 (a1*x1+a2*x2)-(b1*x1+b2*x2)=(a1-b1)*x1+(a2-b2)*x2; theorem :: EUCLIDLP:26 (a1*x1+a2*x2+a3*x3)-(b1*x1+b2*x2+b3*x3)=(a1-b1)*x1+(a2-b2)*x2+( a3-b3)*x3; theorem :: EUCLIDLP:27 a1+a2+a3=1 implies a1*x1+a2*x2+a3*x3=x1+a2*(x2-x1)+a3*(x3-x1); theorem :: EUCLIDLP:28 x=x1+a2*(x2-x1)+a3*(x3-x1) implies ex a1 be Real st x=a1*x1+a2* x2+a3*x3 & a1+a2+a3=1; theorem :: EUCLIDLP:29 for n being Nat st n >= 1 holds 1*n <> 0*n; :: Lines theorem :: EUCLIDLP:30 for A be Subset of REAL n,x1,x2 holds A is being_line & x1 in A & x2 in A & x1<>x2 implies A=Line(x1,x2); theorem :: EUCLIDLP:31 for x1, x2 being Element of REAL n holds y1 in Line(x1,x2) & y2 in Line(x1,x2) implies ex a st y2 - y1 =a*(x2 - x1); definition let n; let x1,x2 be Element of REAL n; pred x1 // x2 means :: EUCLIDLP:def 1 x1 <> 0*n & x2 <> 0*n & ex r st x1 = r*x2; end; theorem :: EUCLIDLP:32 for x1,x2 be Element of REAL n st x1 // x2 holds ex a st a <> 0 & x1 = a*x2; definition let n; let x1,x2 be Element of REAL n; redefine pred x1 // x2; symmetry; end; theorem :: EUCLIDLP:33 x1 // x2 & x2 // x3 implies x1 // x3; definition let n be Nat,x1,x2 be Element of REAL n; pred x1,x2 are_lindependent2 means :: EUCLIDLP:def 2 for a1,a2 being Real st a1*x1+a2* x2=0*n holds a1=0 & a2=0; symmetry; end; notation let n; let x1,x2 be Element of REAL n; antonym x1,x2 are_ldependent2 for x1,x2 are_lindependent2; end; theorem :: EUCLIDLP:34 x1,x2 are_lindependent2 implies x1<>0*n & x2<>0*n; theorem :: EUCLIDLP:35 for x1,x2 st x1,x2 are_lindependent2 holds a1*x1+a2*x2=b1*x1+b2* x2 implies a1=b1 & a2=b2; theorem :: EUCLIDLP:36 for x1,x2,y1,y1 st y1,y2 are_lindependent2 & y1 = a1*x1+a2* x2 & y2=b1*x1+b2*x2 ex c1,c2,d1,d2 be Real st x1=c1*y1+c2*y2 & x2=d1*y1 +d2*y2; theorem :: EUCLIDLP:37 x1,x2 are_lindependent2 implies x1 <> x2; theorem :: EUCLIDLP:38 x2 - x1,x3 - x1 are_lindependent2 implies x2 <> x3; theorem :: EUCLIDLP:39 x1,x2 are_lindependent2 implies x1+t*x2,x2 are_lindependent2; theorem :: EUCLIDLP:40 x1 - x0, x3 - x2 are_lindependent2 & y0 in Line(x0,x1) & y1 in Line(x0,x1) & y0 <> y1 & y2 in Line(x2,x3) & y3 in Line(x2,x3) & y2 <> y3 implies y1 - y0, y3 - y2 are_lindependent2; theorem :: EUCLIDLP:41 x1 // x2 implies x1,x2 are_ldependent2 & x1 <> 0*n & x2 <> 0*n; theorem :: EUCLIDLP:42 x1, x2 are_ldependent2 implies x1 = 0*n or x2 = 0*n or x1 // x2; theorem :: EUCLIDLP:43 for x1,x2,y1 being Element of REAL n ex y2 being Element of REAL n st y2 in Line(x1,x2) & x1-x2,y1-y2 are_orthogonal; definition let n; let x1,x2 be Element of REAL n; pred x1 _|_ x2 means :: EUCLIDLP:def 3 x1 <> 0*n & x2 <> 0*n & x1, x2 are_orthogonal; symmetry; end; theorem :: EUCLIDLP:44 x _|_ y0 & y0 // y1 implies x _|_ y1; theorem :: EUCLIDLP:45 x _|_ y implies x, y are_lindependent2; theorem :: EUCLIDLP:46 x1 // x2 implies not x1 _|_ x2; definition let n; func line_of_REAL n -> Subset-Family of REAL n equals :: EUCLIDLP:def 4 the set of all Line(x1,x2) where x1,x2 is Element of REAL n; end; registration let n; cluster line_of_REAL n -> non empty; end; theorem :: EUCLIDLP:47 Line(x1,x2) in line_of_REAL n; reserve L,L0,L1,L2 for Element of line_of_REAL n; theorem :: EUCLIDLP:48 x1 in L & x2 in L implies Line(x1,x2) c= L; theorem :: EUCLIDLP:49 L1 meets L2 iff ex x st x in L1 & x in L2; theorem :: EUCLIDLP:50 L0 misses L1 & x in L0 implies not x in L1; theorem :: EUCLIDLP:51 ex x1,x2 st L = Line(x1,x2); theorem :: EUCLIDLP:52 ex x st x in L; theorem :: EUCLIDLP:53 L is being_line implies ex x1 st x1 <> x0 & x1 in L; theorem :: EUCLIDLP:54 (not x in L) & L is being_line implies ex x1,x2 st L = Line(x1, x2) & x - x1 _|_ x2 - x1; theorem :: EUCLIDLP:55 (not x in L) & L is being_line implies ex x1,x2 st L = Line(x1, x2) & x - x1,x2 - x1 are_lindependent2; definition let n be Nat,x be Element of REAL n, L be Element of line_of_REAL n; func dist_v(x,L) -> Subset of REAL equals :: EUCLIDLP:def 5 {|.x-x0.| where x0 is Element of REAL n : x0 in L}; end; definition let n be Nat,x be Element of REAL n, L be Element of line_of_REAL n; func dist(x,L) -> Real equals :: EUCLIDLP:def 6 lower_bound dist_v(x,L); end; theorem :: EUCLIDLP:56 L = Line(x1,x2) implies {|.x-x0.| where x0 is Element of REAL n : x0 in Line(x1,x2)} = dist_v(x,L); theorem :: EUCLIDLP:57 ex x0 st x0 in L & |.x-x0.|=dist(x,L); theorem :: EUCLIDLP:58 dist(x,L) >= 0; theorem :: EUCLIDLP:59 x in L iff dist(x,L) = 0; definition let n; let L1,L2; pred L1 // L2 means :: EUCLIDLP:def 7 ex x1, x2, y1, y2 being Element of REAL n st L1 = Line(x1,x2) & L2 = Line(y1,y2) & (x2 - x1) // (y2 - y1); symmetry; end; theorem :: EUCLIDLP:60 L0 // L1 & L1 // L2 implies L0 // L2; definition let n; let L1,L2; pred L1 _|_ L2 means :: EUCLIDLP:def 8 ex x1, x2, y1, y2 being Element of REAL n st L1 = Line(x1,x2) & L2 = Line(y1,y2) & (x2 - x1) _|_ (y2 - y1); symmetry; end; theorem :: EUCLIDLP:61 L0 _|_ L1 & L1 // L2 implies L0 _|_ L2; theorem :: EUCLIDLP:62 (not x in L) & L is being_line implies ex L0 st x in L0 & L0 _|_ L & L0 meets L; theorem :: EUCLIDLP:63 L1 misses L2 implies ex x st x in L1 & not x in L2; theorem :: EUCLIDLP:64 x1 in L & x2 in L & x1 <> x2 implies Line(x1,x2) = L & L is being_line; theorem :: EUCLIDLP:65 L1 is being_line & L1 = L2 implies L1 // L2; theorem :: EUCLIDLP:66 L1 // L2 implies L1 is being_line & L2 is being_line; theorem :: EUCLIDLP:67 L1 _|_ L2 implies L1 is being_line & L2 is being_line; theorem :: EUCLIDLP:68 x in L & a<>1 & a*x in L implies 0*n in L; theorem :: EUCLIDLP:69 x1 in L & x2 in L implies ex x3 st x3 in L & x3 - x1 = a*(x2 - x1); theorem :: EUCLIDLP:70 x1 in L & x2 in L & x3 in L & x1 <> x2 implies ex a st x3 - x1 = a*(x2 - x1); theorem :: EUCLIDLP:71 L1 // L2 & L1<>L2 implies L1 misses L2; theorem :: EUCLIDLP:72 L is being_line implies ex L0 st x in L0 & L0 // L; theorem :: EUCLIDLP:73 for x,L st (not x in L) & L is being_line holds ex L0 st x in L0 & L0 // L & L0 <> L; theorem :: EUCLIDLP:74 for x0,x1,y0,y1,L1,L2 st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 holds x1 - x0 _|_ y1 - y0; theorem :: EUCLIDLP:75 for L1,L2 st L1 _|_ L2 holds L1 <> L2; theorem :: EUCLIDLP:76 for x1,x2,L st L is being_line & L = Line(x1,x2) holds x1 <> x2; theorem :: EUCLIDLP:77 x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 // L2 implies x1 - x0 // y1 - y0; theorem :: EUCLIDLP:78 x2 - x1,x3 - x1 are_lindependent2 & y2 in Line(x1,x2) & y3 in Line(x1, x3) & L1 = Line(x2,x3) & L2 = Line(y2,y3) implies (L1 // L2 iff ex a st a <> 0 & y2 - x1 = a*(x2 - x1) & y3 - x1 = a*(x3 - x1)); theorem :: EUCLIDLP:79 for L1,L2 st L1 is being_line & L2 is being_line & L1 <> L2 holds ex x st x in L1 & not x in L2; theorem :: EUCLIDLP:80 for x,L1,L2 st L1 _|_ L2 holds ex L0 st x in L0 & L0 _|_ L2 & L0 // L1; theorem :: EUCLIDLP:81 for x,L1,L2 st x in L2 & L1 _|_ L2 holds ex x0 st x <> x0 & x0 in L1 & not x0 in L2; :: Planes definition let n be Nat,x1,x2,x3 be Element of REAL n; func plane(x1,x2,x3) -> Subset of REAL n equals :: EUCLIDLP:def 9 {x where x is Element of REAL n: ex a1,a2,a3 being Real st a1+a2+a3=1 & x=a1*x1+a2*x2+a3*x3}; end; registration let n be Nat,x1,x2,x3 be Element of REAL n; cluster plane(x1,x2,x3) -> non empty; end; definition let n; let A be Subset of REAL n; attr A is being_plane means :: EUCLIDLP:def 10 ex x1,x2,x3 st x2 - x1, x3 - x1 are_lindependent2 & A = plane(x1,x2,x3); end; theorem :: EUCLIDLP:82 x1 in plane(x1,x2,x3) & x2 in plane(x1,x2,x3) & x3 in plane(x1, x2,x3); theorem :: EUCLIDLP:83 x1 in plane(y1,y2,y3) & x2 in plane(y1,y2,y3) & x3 in plane(y1, y2,y3) implies plane(x1,x2,x3) c= plane(y1,y2,y3); theorem :: EUCLIDLP:84 for A being Subset of REAL n,x,x1,x2,x3 st x in plane(x1,x2,x3) & ex c1,c2,c3 being Real st c1 + c2 + c3 = 0 & x = c1*x1 + c2*x2 + c3*x3 holds 0*n in plane(x1,x2,x3); theorem :: EUCLIDLP:85 y1 in plane(x1,x2,x3) & y2 in plane(x1,x2,x3) implies Line(y1,y2 ) c= plane(x1,x2,x3); theorem :: EUCLIDLP:86 for A being Subset of REAL n,x st A is being_plane & x in A & ex a st a<>1 & a*x in A holds 0*n in A; theorem :: EUCLIDLP:87 x in plane(x1,x2,x3) & x = a1*x1+a2*x2+a3* x3 implies a1 + a2 + a3 = 1 or 0*n in plane(x1,x2,x3); theorem :: EUCLIDLP:88 x in plane(x1,x2,x3) iff ex a1,a2,a3 st a1+a2+a3=1 & x = a1*x1+ a2*x2+a3*x3; theorem :: EUCLIDLP:89 x2-x1,x3-x1 are_lindependent2 & a1 + a2 + a3 = 1 & x = a1*x1+a2*x2+a3* x3 & b1 + b2 + b3 = 1 & x = b1*x1+b2*x2+b3*x3 implies a1 = b1 & a2 = b2 & a3 = b3; definition let n; func plane_of_REAL n -> Subset-Family of REAL n equals :: EUCLIDLP:def 11 {P where P is Subset of REAL n: ex x1,x2,x3 being Element of REAL n st P = plane(x1,x2,x3)}; end; registration let n; cluster plane_of_REAL n -> non empty; end; theorem :: EUCLIDLP:90 plane(x1,x2,x3) in plane_of_REAL n; reserve P,P0,P1,P2 for Element of plane_of_REAL n; theorem :: EUCLIDLP:91 x1 in P & x2 in P & x3 in P implies plane(x1,x2,x3) c= P; theorem :: EUCLIDLP:92 x1 in P & x2 in P & x3 in P & x2 - x1, x3 - x1 are_lindependent2 implies P = plane(x1,x2,x3); theorem :: EUCLIDLP:93 P1 is being_plane & P1 c= P2 implies P1 = P2; :: Lines in the planes theorem :: EUCLIDLP:94 Line(x1,x2) c= plane(x1,x2,x3) & Line(x2,x3) c= plane(x1,x2,x3) & Line (x3,x1) c= plane(x1,x2,x3); theorem :: EUCLIDLP:95 x1 in P & x2 in P implies Line(x1,x2) c= P; definition let n be Nat,L1,L2 be Element of line_of_REAL n; pred L1,L2 are_coplane means :: EUCLIDLP:def 12 ex x1,x2,x3 being Element of REAL n st L1 c= plane(x1,x2,x3) & L2 c= plane(x1,x2,x3); end; theorem :: EUCLIDLP:96 L1,L2 are_coplane iff ex P st L1 c= P & L2 c= P; theorem :: EUCLIDLP:97 L1 // L2 implies L1,L2 are_coplane; theorem :: EUCLIDLP:98 L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 misses L2 implies ex P st L1 c= P & L2 c= P & P is being_plane; theorem :: EUCLIDLP:99 ex P st x in P & L c= P; theorem :: EUCLIDLP:100 (not x in L) & L is being_line implies ex P st x in P & L c= P & P is being_plane; theorem :: EUCLIDLP:101 x in P & L c= P & (not x in L) & L is being_line implies P is being_plane; theorem :: EUCLIDLP:102 (not x in L) & L is being_line & x in P0 & L c= P0 & x in P1 & L c= P1 implies P0 = P1; theorem :: EUCLIDLP:103 L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 <> L2 implies ex P st L1 c= P & L2 c= P & P is being_plane; theorem :: EUCLIDLP:104 for L1,L2 st L1 is being_line & L2 is being_line & L1 <> L2 & L1 meets L2 holds ex P st L1 c= P & L2 c= P & P is being_plane; theorem :: EUCLIDLP:105 L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 implies P1 = P2; theorem :: EUCLIDLP:106 L1 // L2 & L1 <> L2 implies ex P st L1 c= P & L2 c= P & P is being_plane; theorem :: EUCLIDLP:107 L1 _|_ L2 & L1 meets L2 implies ex P st P is being_plane & L1 c= P & L2 c= P; theorem :: EUCLIDLP:108 L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 implies L0 = L1; theorem :: EUCLIDLP:109 L1,L2 are_coplane & L1 _|_ L2 implies L1 meets L2; theorem :: EUCLIDLP:110 L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 implies L0 c= P & L0 _|_ L1; theorem :: EUCLIDLP:111 L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 implies L1 // L2; theorem :: EUCLIDLP:112 L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 implies L meets L2; theorem :: EUCLIDLP:113 L1,L2 are_coplane & L1 is being_line & L2 is being_line & L1 misses L2 implies L1 // L2; theorem :: EUCLIDLP:114 x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1, y2 - y1 are_lindependent2 implies Line(x1,x2) meets Line(y1,y2);