:: Analytical Ordered Affine Spaces
::  by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 11, 1990
:: Copyright (c) 1990-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, RLVECT_1, REAL_1, CARD_1, ARYTM_3, RELAT_1, ARYTM_1,
      SUPINF_2, STRUCT_0, ZFMISC_1, XBOOLE_0, SUBSET_1, ANALOAF;
 notations TARSKI, XBOOLE_0, ZFMISC_1, ORDINAL1, DOMAIN_1, XXREAL_0, XCMPLX_0,
      XREAL_0, REAL_1, RELSET_1, NUMBERS, STRUCT_0, RLVECT_1;
 constructors XXREAL_0, REAL_1, MEMBERED, DOMAIN_1, RLVECT_1;
 registrations SUBSET_1, RELSET_1, XXREAL_0, STRUCT_0, ZFMISC_1, XREAL_0,
      ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve V for RealLinearSpace;
reserve p,q,u,v,w,y for VECTOR of V;
reserve a,b,c,d for Real;

definition
  let V;
  let u,v,w,y;
  pred u,v // w,y means
:: ANALOAF:def 1

  u=v or w=y or ex a,b st 0<a & 0<b & a*(v-u)=b*( y-w);
end;

theorem :: ANALOAF:1
  (w-v)+(v-u) = w-u;

theorem :: ANALOAF:2
  y+u = v+w implies y-w = v-u;

theorem :: ANALOAF:3
  a*(u-v) = -(a*(v-u));

theorem :: ANALOAF:4
  (a-b)*(u-v) = (b-a)*(v-u);

theorem :: ANALOAF:5
  a<>0 & a*u=v implies u=a"*v;

theorem :: ANALOAF:6
  (a<>0 & a*u=v implies u=a"*v) & (a<>0 & u=a"*v implies a*u=v);

theorem :: ANALOAF:7
  u,v // w,y & u<>v & w<>y implies ex a,b st a*(v-u)=b*(y-w) & 0<a & 0<b;

theorem :: ANALOAF:8
  u,v // u,v;

theorem :: ANALOAF:9
  u,v // w,w & u,u // v,w;

theorem :: ANALOAF:10
  u,v // v,u implies u=v;

theorem :: ANALOAF:11
  p<>q & p,q // u,v & p,q // w,y implies u,v // w,y;

theorem :: ANALOAF:12
  u,v // w,y implies v,u // y,w & w,y // u,v;

theorem :: ANALOAF:13
  u,v // v,w implies u,v // u,w;

theorem :: ANALOAF:14
  u,v // u,w implies u,v // v,w or u,w // w,v;

theorem :: ANALOAF:15
  v-u=y-w implies u,v // w,y;

theorem :: ANALOAF:16
  y=(v+w)-u implies u,v // w,y & u,w // v,y;

theorem :: ANALOAF:17
  (ex p,q st p<>q) implies for u,v,w ex y st u,v // w,y & u,w // v ,y & v<>y;

theorem :: ANALOAF:18
  p<>v & v,p // p,w implies ex y st u,p // p,y & u,v // w,y;

theorem :: ANALOAF:19
  (for a,b st a*u + b*v=0.V holds a=0 & b=0) implies u<>v & u<>0.V & v<>0.V;

theorem :: ANALOAF:20
  (ex u,v st (for a,b st a*u + b*v=0.V holds a=0 & b=0)) implies
  ex u,v,w,y st not u,v // w,y & not u,v // y,w;

theorem :: ANALOAF:21
  (ex p,q st (for w ex a,b st a*p + b*q=w)) implies for u,v,w,y st
not u,v // w,y & not u,v // y,w ex z being VECTOR of V st (u,v // u,z or u,v //
  z,u) & (w,y // w,z or w,y // z,w);

definition
  struct(1-sorted) AffinStruct
  (#carrier -> set, CONGR -> Relation of [:the carrier,the carrier:]#);
end;

registration
  cluster non trivial strict for AffinStruct;
end;

reserve AS for non empty AffinStruct;
reserve a,b,c,d for Element of AS;
reserve x,z for object;

definition
  let AS,a,b,c,d;
  pred a,b // c,d means
:: ANALOAF:def 2

  [[a,b],[c,d]] in the CONGR of AS;
end;

definition
  let V;
  func DirPar(V) -> Relation of [:the carrier of V,the carrier of V:] means
:: ANALOAF:def 3
 [x,z] in it iff ex u,v,w,y st x=[u,v] & z=[w,y] & u,v // w,y;
end;

theorem :: ANALOAF:22
  [[u,v],[w,y]] in DirPar(V) iff u,v // w,y;

definition
  let V;
  func OASpace(V) -> strict AffinStruct equals
:: ANALOAF:def 4
  AffinStruct (#the carrier of V,
    DirPar(V)#);
end;

registration
  let V;
  cluster OASpace V -> non empty;
end;

theorem :: ANALOAF:23
  (ex u,v st for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0
  ) implies (ex a,b being Element of OASpace(V) st a<>b) & (for a,b,c,d,p,q,r,s
being Element of OASpace(V) holds a,b // c,c & (a,b // b,a implies a=b) & (a<>b
& a,b // p,q & a,b // r,s implies p,q // r,s) & (a,b // c,d implies b,a // d,c)
& (a,b // b,c implies a,b // a,c) & (a,b // a,c implies a,b // b,c or a,c // c,
b)) & (ex a,b,c,d being Element of OASpace(V) st not a,b // c,d & not a,b // d,
c) & (for a,b,c being Element of OASpace(V) ex d being Element of OASpace(V) st
a,b // c,d & a,c // b,d & b<>d) & for p,a,b,c being Element of OASpace(V) st p
  <>b & b,p // p,c ex d being Element of OASpace(V) st a,p // p,d & a,b // c,d;

theorem :: ANALOAF:24
  (ex p,q being VECTOR of V st (for w being VECTOR of V ex a,b
being Real st a*p + b*q=w)) implies
 for a,b,c,d being Element of OASpace(V) st
not a,b // c,d & not a,b // d,c ex t being Element of OASpace(V) st (a,b // a,t
  or a,b // t,a) & (c,d // c,t or c,d // t,c);

definition
  let IT be non empty AffinStruct;
  attr IT is OAffinSpace-like means
:: ANALOAF:def 5

  (for a,b,c,d,p,q,r,s being Element
of IT holds a,b // c,c & (a,b // b,a implies a=b) & (a<>b & a,b // p,q & a,b //
r,s implies p,q // r,s) & (a,b // c,d implies b,a // d,c) & (a,b // b,c implies
  a,b // a,c) & (a,b // a,c implies a,b // b,c or a,c // c,b)) & (ex a,b,c,d
  being Element of IT st not a,b // c,d & not a,b // d,c) & (for a,b,c being
Element of IT ex d being Element of IT st a,b // c,d & a,c // b,d & b<>d) & for
p,a,b,c being Element of IT st p<>b & b,p // p,c ex d being Element of IT st a,
  p // p,d & a,b // c,d;
end;

registration
  cluster strict OAffinSpace-like for non trivial AffinStruct;
end;

definition
  mode OAffinSpace is OAffinSpace-like non trivial AffinStruct;
end;

theorem :: ANALOAF:25
  (ex a,b being Element of AS st a<>b) & (for a,b,c,d,p,q,r,s being
Element of AS holds a,b // c,c & (a,b // b,a implies a=b) & (a<>b & a,b // p,q
& a,b // r,s implies p,q // r,s) & (a,b // c,d implies b,a // d,c) & (a,b // b,
c implies a,b // a,c) & (a,b // a,c implies a,b // b,c or a,c // c,b)) & (ex a,
  b,c,d being Element of AS st not a,b // c,d & not a,b // d,c) & (for a,b,c
being Element of AS ex d being Element of AS st a,b // c,d & a,c // b,d & b<>d)
  & (for p,a,b,c being Element of AS st p<>b & b,p // p,c ex d being Element of
  AS st a,p // p,d & a,b // c,d) iff AS is OAffinSpace;

theorem :: ANALOAF:26
  (ex u,v st for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0
  ) implies OASpace(V) is OAffinSpace;

definition
  let IT be OAffinSpace;
  attr IT is 2-dimensional means
:: ANALOAF:def 6

  for a,b,c,d being Element of IT st not
a,b // c,d & not a,b // d,c holds ex p being Element of IT st (a,b // a,p or a,
  b // p,a) & (c,d // c,p or c,d // p,c);
end;

registration
  cluster strict 2-dimensional for OAffinSpace;
end;

definition
  mode OAffinPlane is 2-dimensional OAffinSpace;
end;

theorem :: ANALOAF:27
  (ex a,b being Element of AS st a<>b) & (for a,b,c,d,p,q,r,s being
Element of AS holds a,b // c,c & (a,b // b,a implies a=b) & (a<>b & a,b // p,q
& a,b // r,s implies p,q // r,s) & (a,b // c,d implies b,a // d,c) & (a,b // b,
c implies a,b // a,c) & (a,b // a,c implies a,b // b,c or a,c // c,b)) & (ex a,
  b,c,d being Element of AS st not a,b // c,d & not a,b // d,c) & (for a,b,c
being Element of AS ex d being Element of AS st a,b // c,d & a,c // b,d & b<>d)
  & (for p,a,b,c being Element of AS st p<>b & b,p // p,c ex d being Element of
AS st a,p // p,d & a,b // c,d) & (for a,b,c,d being Element of AS st not a,b //
c,d & not a,b // d,c holds ex p being Element of AS st (a,b // a,p or a,b // p,
  a) & (c,d // c,p or c,d // p,c)) iff AS is OAffinPlane;

theorem :: ANALOAF:28
  (ex u,v st (for a,b being Real st a*u + b*v = 0.V holds a=0 & b=0) &
  (for w ex a,b being Real st w = a*u + b*v)) implies
   OASpace(V) is OAffinPlane;