environ vocabulary RLVECT_1, ARYTM_1, RELAT_1, ANALOAF, DIRAF, SYMSP_1, REALSET1, INCSP_1, AFF_1, ANALMETR; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, DOMAIN_1, REAL_1, STRUCT_0, DIRAF, RELSET_1, RLVECT_1, AFF_1, ANALOAF, REALSET1; constructors DOMAIN_1, REAL_1, AFF_1, XREAL_0, MEMBERED, XBOOLE_0; clusters DIRAF, ANALOAF, RELSET_1, STRUCT_0, SUBSET_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve V for RealLinearSpace; reserve u,u1,u2,v,v1,v2,w,w1,y for VECTOR of V; reserve a,a1,a2,b,b1,b2,c1,c2 for Real; reserve x,z for set; definition let V; let w,y; pred Gen w,y means :: ANALMETR:def 1 (for u ex a1,a2 st u = a1*w + a2*y) & (for a1,a2 st a1*w + a2*y = 0.V holds a1=0 & a2=0); end; definition let V; let u,v,w,y; pred u,v are_Ort_wrt w,y means :: ANALMETR:def 2 ex a1,a2,b1,b2 st (u = a1*w + a2*y & v = b1*w + b2*y & a1*b1 + a2*b2 = 0); end; canceled 4; theorem :: ANALMETR:5 for w,y st Gen w,y holds (u,v are_Ort_wrt w,y iff (for a1,a2,b1,b2 st u = a1*w + a2*y & v = b1*w + b2*y holds a1*b1 + a2*b2 = 0)); theorem :: ANALMETR:6 w,y are_Ort_wrt w,y; theorem :: ANALMETR:7 ex V st ex w,y st Gen w,y; theorem :: ANALMETR:8 u,v are_Ort_wrt w,y implies v,u are_Ort_wrt w,y; theorem :: ANALMETR:9 Gen w,y implies (for u,v holds u,0.V are_Ort_wrt w,y & 0.V,v are_Ort_wrt w,y); theorem :: ANALMETR:10 u,v are_Ort_wrt w,y implies a*u,b*v are_Ort_wrt w,y; theorem :: ANALMETR:11 u,v are_Ort_wrt w,y implies a*u,v are_Ort_wrt w,y & u,b*v are_Ort_wrt w,y; theorem :: ANALMETR:12 Gen w,y implies (for u ex v st (u,v are_Ort_wrt w,y & v<>0.V)); theorem :: ANALMETR:13 Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v<>0.V implies ( ex a,b st a*u1 = b*u2 & (a<>0 or b<>0) ); theorem :: ANALMETR:14 Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y implies u,v1+v2 are_Ort_wrt w,y & u,v1-v2 are_Ort_wrt w,y; theorem :: ANALMETR:15 Gen w,y & u,u are_Ort_wrt w,y implies u = 0.V; theorem :: ANALMETR:16 Gen w,y & u,u1-u2 are_Ort_wrt w,y & u1,u2-u are_Ort_wrt w,y implies u2,u-u1 are_Ort_wrt w,y; theorem :: ANALMETR:17 (Gen w,y & u <> 0.V) implies ex a st v - a*u,u are_Ort_wrt w,y; theorem :: ANALMETR:18 (u,v // u1,v1 or u,v // v1,u1) iff (ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0)); theorem :: ANALMETR:19 [[u,v],[u1,v1]] in lambda(DirPar(V)) iff (ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0)); definition let V; let u,u1,v,v1,w,y; pred u,u1,v,v1 are_Ort_wrt w,y means :: ANALMETR:def 3 u1-u,v1-v are_Ort_wrt w,y; end; definition let V; let w,y; func Orthogonality(V,w,y) -> Relation of [:the carrier of V,the carrier of V:] means :: ANALMETR:def 4 [x,z] in it iff ex u,u1,v,v1 st x=[u,u1] & z=[v,v1] & u,u1,v,v1 are_Ort_wrt w,y; end; reserve p,p1,q,q1 for Element of Lambda(OASpace(V)); canceled 2; theorem :: ANALMETR:22 the carrier of Lambda(OASpace(V)) = the carrier of V; theorem :: ANALMETR:23 the CONGR of Lambda(OASpace(V)) = lambda(DirPar(V)); theorem :: ANALMETR:24 p=u & q=v & p1=u1 & q1=v1 implies (p,q // p1,q1 iff (ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0))); definition struct(AffinStruct) ParOrtStr (# carrier -> set, CONGR -> (Relation of [:the carrier,the carrier:]), orthogonality -> Relation of [:the carrier,the carrier:] #); end; definition cluster non empty ParOrtStr; end; reserve POS for non empty ParOrtStr; definition let POS; let a,b,c,d be Element of POS; pred a,b // c,d means :: ANALMETR:def 5 [[a,b],[c,d]] in the CONGR of POS; pred a,b _|_ c,d means :: ANALMETR:def 6 [[a,b],[c,d]] in the orthogonality of POS; end; definition let V,w,y; func AMSpace(V,w,y) -> strict ParOrtStr equals :: ANALMETR:def 7 ParOrtStr(#the carrier of V,lambda(DirPar(V)),Orthogonality(V,w,y)#); end; definition let V,w,y; cluster AMSpace(V,w,y) -> non empty; end; canceled 3; theorem :: ANALMETR:28 (the carrier of AMSpace(V,w,y) = the carrier of V & the CONGR of AMSpace(V,w,y) = lambda(DirPar(V)) & the orthogonality of AMSpace(V,w,y) = Orthogonality(V,w,y)); definition let POS; func Af(POS) -> strict AffinStruct equals :: ANALMETR:def 8 AffinStruct (# the carrier of POS, the CONGR of POS #); end; definition let POS; cluster Af POS -> non empty; end; canceled; theorem :: ANALMETR:30 Af(AMSpace(V,w,y)) = Lambda(OASpace(V)); reserve p,p1,p2,q,q1,r,r1,r2 for Element of AMSpace(V,w,y); theorem :: ANALMETR:31 p=u & p1=u1 & q=v & q1=v1 implies (p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y); theorem :: ANALMETR:32 p=u & q=v & p1=u1 & q1=v1 implies (p,q // p1,q1 iff (ex a,b st a*(v-u) = b*(v1-u1) & (a<>0 or b<>0))); theorem :: ANALMETR:33 p,q _|_ p1,q1 implies p1,q1 _|_ p,q; theorem :: ANALMETR:34 p,q _|_ p1,q1 implies p,q _|_ q1,p1; theorem :: ANALMETR:35 Gen w,y implies for p,q,r holds p,q _|_ r,r; theorem :: ANALMETR:36 p,p1 _|_ q,q1 & p,p1 // r,r1 implies p=p1 or q,q1 _|_ r,r1; theorem :: ANALMETR:37 Gen w,y implies (for p,q,r ex r1 st p,q _|_ r,r1 & r<>r1); theorem :: ANALMETR:38 Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 implies p=p1 or q,q1 // r,r1; theorem :: ANALMETR:39 Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 implies p,q _|_ r1,r2; theorem :: ANALMETR:40 Gen w,y & p,q _|_ p,q implies p = q; theorem :: ANALMETR:41 Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p implies p2,q _|_ p,p1; theorem :: ANALMETR:42 Gen w,y & p<>p1 implies for q ex q1 st p,p1 // p,q1 & p,p1 _|_ q1,q; definition let IT be non empty ParOrtStr; attr IT is OrtAfSp-like means :: ANALMETR:def 9 AffinStruct(#the carrier of IT,the CONGR of IT#) is AffinSpace & (for a,b,c,d,p,q,r,s being Element of IT holds (a,b _|_ a,b implies a=b) & a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b) & (a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s)) & (for a,b,c being Element of IT st a<>b ex x being Element of IT st a,b // a,x & a,b _|_ x,c) & (for a,b,c being Element of IT ex x being Element of IT st a,b _|_ c,x & c <>x); end; definition cluster strict OrtAfSp-like (non empty ParOrtStr); end; definition mode OrtAfSp is OrtAfSp-like (non empty ParOrtStr); end; canceled; theorem :: ANALMETR:44 Gen w,y implies AMSpace(V,w,y) is OrtAfSp; definition let IT be non empty ParOrtStr; attr IT is OrtAfPl-like means :: ANALMETR:def 10 AffinStruct(#the carrier of IT,the CONGR of IT#) is AffinPlane & (for a,b,c,d,p,q,r,s being Element of IT holds (a,b _|_ a,b implies a=b) & a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b) & (a,b _|_ p,q & a,b _|_ r,s implies p,q // r,s or a=b)) & (for a,b,c being Element of IT ex x being Element of IT st a,b _|_ c,x & c <>x); end; definition cluster strict OrtAfPl-like (non empty ParOrtStr); end; definition mode OrtAfPl is OrtAfPl-like (non empty ParOrtStr); end; canceled; theorem :: ANALMETR:46 Gen w,y implies AMSpace(V,w,y) is OrtAfPl; theorem :: ANALMETR:47 for x being set holds (x is Element of POS iff x is Element of Af(POS)); theorem :: ANALMETR:48 for a,b,c,d being Element of POS, a',b',c',d' being Element of Af(POS) st a=a'& b=b' & c = c' & d=d' holds (a,b // c,d iff a',b' // c',d'); definition let POS be OrtAfSp; cluster Af(POS) -> AffinSpace-like non trivial; end; definition let POS be OrtAfPl; cluster Af(POS) -> 2-dimensional AffinSpace-like non trivial; end; theorem :: ANALMETR:49 for POS being OrtAfPl holds POS is OrtAfSp; definition cluster OrtAfPl-like -> OrtAfSp-like (non empty ParOrtStr); end; theorem :: ANALMETR:50 for POS being OrtAfSp st Af(POS) is AffinPlane holds POS is OrtAfPl; theorem :: ANALMETR:51 for POS being non empty ParOrtStr holds POS is OrtAfPl-like iff ( (ex a,b being Element of POS st a<>b) & (for a,b,c,d,p,q,r,s being Element of POS holds (a,b // b,a & a,b // c,c & (a,b // p,q & a,b // r,s implies p,q // r,s or a=b) & (a,b // a,c implies b,a // b,c) & (ex x being Element of POS st a,b // c,x & a,c // b,x) & (ex x,y,z being Element of POS st not x,y // x,z ) & (ex x being Element of POS st a,b // c,x & c <>x) & (a,b // b,d & b<>a implies ex x being Element of POS st c,b // b,x & c,a // d,x) & (a,b _|_ a,b implies a=b) & a,b _|_ c,c & (a,b _|_ c,d implies a,b _|_ d,c & c,d _|_ a,b) & (a,b _|_ p,q & a,b // r,s implies p,q _|_ r,s or a=b) & (a,b _|_ p,q & a,b _|_ r,s implies p,q // r,s or a=b) & (ex x being Element of POS st a,b _|_ c,x & c <>x) & (not a,b // c,d implies ex x being Element of POS st a,b // a,x & c,d // c,x )))); reserve x,a,b,c,d,p,q,y for Element of POS; definition let POS; let a,b,c; pred LIN a,b,c means :: ANALMETR:def 11 a,b // a,c; end; definition let POS,a,b; func Line(a,b) -> Subset of POS means :: ANALMETR:def 12 for x being Element of POS holds x in it iff LIN a,b,x; end; reserve A,K,M for Subset of POS; definition let POS; let A; attr A is being_line means :: ANALMETR:def 13 ex a,b st a<>b & A=Line(a,b); synonym A is_line; end; canceled 3; theorem :: ANALMETR:55 for POS being OrtAfSp for a,b,c being Element of POS, a',b',c' being Element of Af(POS) st a=a'& b=b' & c = c' holds (LIN a,b,c iff LIN a',b',c'); theorem :: ANALMETR:56 for POS being OrtAfSp for a,b being Element of POS, a',b' being Element of Af(POS) st a=a' & b=b' holds Line(a,b) = Line(a',b'); theorem :: ANALMETR:57 for X being set holds ( X is Subset of POS iff X is Subset of Af(POS)); theorem :: ANALMETR:58 for POS being OrtAfSp for X being Subset of POS, Y being Subset of Af(POS) st X=Y holds ( X is_line iff Y is_line); definition let POS; let a,b,K; pred a,b _|_ K means :: ANALMETR:def 14 ex p,q st p<>q & K = Line(p,q) & a,b _|_ p,q; end; definition let POS; let K,M; pred K _|_ M means :: ANALMETR:def 15 ex p,q st p<>q & K = Line(p,q) & p,q _|_ M; end; definition let POS; let K,M; pred K // M means :: ANALMETR:def 16 ex a,b,c,d st a<>b & c <>d & K = Line(a,b) & M = Line(c,d) & a,b // c,d; end; canceled 3; theorem :: ANALMETR:62 (a,b _|_ K implies K is_line) & (K _|_ M implies (K is_line & M is_line)); theorem :: ANALMETR:63 K _|_ M iff ex a,b,c,d st (a<>b & c <>d & K = Line(a,b) & M = Line(c,d) & a,b _|_ c,d); theorem :: ANALMETR:64 for POS being OrtAfSp for M,N being Subset of POS, M',N' being Subset of Af(POS) st M = M' & N = N' holds (M // N iff M' // N'); reserve POS for OrtAfSp; reserve A,K,M,N for Subset of POS; reserve a,b,c,d,p,q,r,s for Element of POS; theorem :: ANALMETR:65 K is_line implies a,a _|_ K; theorem :: ANALMETR:66 a,b _|_ K & (a,b // c,d or c,d // a,b) & a<>b implies c,d _|_ K; theorem :: ANALMETR:67 a,b _|_ K implies b,a _|_ K; theorem :: ANALMETR:68 K // M implies M // K; theorem :: ANALMETR:69 r,s _|_ K & (K // M or M // K) implies r,s _|_ M; theorem :: ANALMETR:70 K _|_ M implies M _|_ K; definition let POS be OrtAfSp; let K,M be Subset of POS; redefine pred K // M; symmetry; redefine pred K _|_ M; symmetry; end; theorem :: ANALMETR:71 a in K & b in K & a,b _|_ K implies a=b; theorem :: ANALMETR:72 not K _|_ K; theorem :: ANALMETR:73 (K _|_ M or M _|_ K) & (K // N or N // K) implies (M _|_ N & N _|_ M); theorem :: ANALMETR:74 K // N implies not K _|_ N; theorem :: ANALMETR:75 a in K & b in K & c,d _|_ K implies (c,d _|_ a,b & a,b _|_ c,d); theorem :: ANALMETR:76 a in K & b in K & a<>b & K is_line implies K =Line(a,b); theorem :: ANALMETR:77 a in K & b in K & a<>b & K is_line & (a,b _|_ c,d or c,d _|_ a,b) implies c,d _|_ K; theorem :: ANALMETR:78 a in M & b in M & c in N & d in N & M _|_ N implies a,b _|_ c,d; theorem :: ANALMETR:79 p in M & p in N & a in M & b in N & a<>b & a in K & b in K & A _|_ M & A _|_ N & K is_line implies A _|_ K; theorem :: ANALMETR:80 b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c; theorem :: ANALMETR:81 a,b // c,d implies a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a; theorem :: ANALMETR:82 p<>q & ((p,q // a,b & p,q // c,d) or (p,q // a,b & c,d // p,q) or (a,b // p,q & c,d // p,q) or (a,b // p,q & p,q // c,d)) implies a,b // c,d; theorem :: ANALMETR:83 a,b _|_ c,d implies a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a; theorem :: ANALMETR:84 p<>q & ((p,q // a,b & p,q _|_ c,d) or (p,q // c,d & p,q _|_ a,b) or (p,q // a,b & c,d _|_ p,q) or (p,q // c,d & a,b _|_ p,q) or (a,b // p,q & c,d _|_ p,q) or (c,d // p,q & a,b _|_ p,q) or (a,b // p,q & p,q _|_ c,d) or (c,d // p,q & p,q _|_ a,b)) implies a,b _|_ c,d; reserve POS for OrtAfPl; reserve K,M,N for Subset of POS; reserve x,a,b,c,d,p,q for Element of POS; theorem :: ANALMETR:85 p<>q & ((p,q _|_ a,b & p,q _|_ c,d) or (p,q _|_ a,b & c,d _|_ p,q) or (a,b _|_ p,q & c,d _|_ p,q) or (a,b _|_ p,q & p,q _|_ c,d)) implies a,b // c,d ; theorem :: ANALMETR:86 a in M & b in M & a<>b & M is_line & c in N & d in N & c <>d & N is_line & a,b // c,d implies M // N; theorem :: ANALMETR:87 (K _|_ M or M _|_ K) & (K _|_ N or N _|_ K) implies (M // N & N // M ); theorem :: ANALMETR:88 M _|_ N implies ex p st p in M & p in N; theorem :: ANALMETR:89 a,b _|_ c,d implies ex p st LIN a,b,p & LIN c,d,p; theorem :: ANALMETR:90 a,b _|_ K implies ex p st LIN a,b,p & p in K; theorem :: ANALMETR:91 ex x st a,x _|_ p,q & LIN p,q,x; theorem :: ANALMETR:92 K is_line implies ex x st a,x _|_ K & x in K;