The Mizar abstract of ANALMETR

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: Analytical Metric Affine Spaces and Planes
by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski
Received August 10, 1990
MML identifier: ANALMETR
[ Mizar article, MML identifier index ]
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;
The abstract of the Mizar article:

Analytical Metric Affine Spaces and Planes
