:: Directed Geometrical Bundles and Their Analytical Representation
::  by Grzegorz Lewandowski, Krzysztof Pra\.zmowski and Bo\.zena Lewandowska
::
:: Received September 24, 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 XBOOLE_0, ANALOAF, SUBSET_1, STRUCT_0, ZFMISC_1, TDGROUP, DIRAF,
      BINOP_1, FUNCT_1, ALGSTR_0, SUPINF_2, ARYTM_3, RLVECT_1, ARYTM_1,
      VECTSP_1, MCART_1, PBOOLE, RELAT_1, TARSKI, AFVECT0;
 notations TARSKI, ZFMISC_1, SUBSET_1, STRUCT_0, ALGSTR_0, ANALOAF, TDGROUP,
      FUNCT_1, FUNCT_2, XTUPLE_0, MCART_1, BINOP_1, RELAT_1, VECTSP_1,
      RLVECT_1;
 constructors BINOP_1, DOMAIN_1, TDGROUP, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1, TDGROUP,
      RELAT_1, XTUPLE_0;
 requirements SUBSET, BOOLE;


begin

definition
  let IT be non empty AffinStruct;
  attr IT is WeakAffVect-like means
:: AFVECT0:def 1

  (for a,b,c being Element of IT st a
,b // c,c holds a=b) & (for a,b,c,d,p,q being Element of IT st a,b // p,q & c,d
// p,q holds a,b // c,d) & (for a,b,c being Element of IT ex d being Element of
IT st a,b // c,d) & (for a,b,c,a9,b9,c9 being Element of IT st a,b // a9,b9 & a
  ,c // a9,c9 holds b,c // b9,c9) & (for a,c being Element of IT ex b being
  Element of IT st a,b // b,c) & for a,b,c,d being Element of IT st a,b // c,d
  holds a,c // b,d;
end;

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

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

registration
  cluster AffVect-like -> WeakAffVect-like for non empty AffinStruct;
end;

reserve AFV for WeakAffVect;
reserve a,b,c,d,e,f,a9,b9,c9,d9,f9,p,q,r,o,x99 for Element of AFV;

::
::          Properties of Relation of Congruence of Vectors
::

theorem :: AFVECT0:1
  a,b // a,b;

theorem :: AFVECT0:2
  a,a // a,a;

theorem :: AFVECT0:3
  a,b // c,d implies c,d // a,b;

theorem :: AFVECT0:4
  a,b // a,c implies b = c;

theorem :: AFVECT0:5
  a,b // c,d & a,b // c,d9 implies d = d9;

theorem :: AFVECT0:6
  for a,b holds a,a // b,b;

theorem :: AFVECT0:7
  a,b // c,d implies b,a // d,c;

theorem :: AFVECT0:8
  a,b // c,d & a,c // b9,d implies b = b9;

theorem :: AFVECT0:9
  b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 implies d = d9;

theorem :: AFVECT0:10
  a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 implies d = d9;

theorem :: AFVECT0:11
  a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 implies a,f
  // a9,f9;

theorem :: AFVECT0:12
  a,b // a9,b9 & a,c // c9,b9 implies b,c // c9,a9;

::
::                  Relation of Maximal Distance
::

definition
  let AFV;
  let a,b;
  pred MDist a,b means
:: AFVECT0:def 2

  a,b // b,a & a <> b;
  irreflexivity;
  symmetry;
end;

theorem :: AFVECT0:13
  ex a,b st a<>b & not MDist a,b;

theorem :: AFVECT0:14
  MDist a,b & MDist a,c implies b = c or MDist b,c;

theorem :: AFVECT0:15
  MDist a,b & a,b // c,d implies MDist c,d;

::
::                        Midpoint Relation
::

definition
  let AFV;
  let a,b,c;
  pred Mid a,b,c means
:: AFVECT0:def 3

  a,b // b,c;
end;

theorem :: AFVECT0:16
  Mid a,b,c implies Mid c,b,a;

theorem :: AFVECT0:17
  Mid a,b,b iff a = b;

theorem :: AFVECT0:18
  Mid a,b,a iff a = b or MDist a,b;

theorem :: AFVECT0:19
  ex b st Mid a,b,c;

theorem :: AFVECT0:20
  Mid a,b,c & Mid a,b9,c implies b =b9 or MDist b,b9;

theorem :: AFVECT0:21
  ex c st Mid a,b,c;

theorem :: AFVECT0:22
  Mid a,b,c & Mid a,b,c9 implies c = c9;

theorem :: AFVECT0:23
  Mid a,b,c & MDist b,b9 implies Mid a,b9,c;

theorem :: AFVECT0:24
  Mid a,b,c & Mid a,b9,c9 & MDist b,b9 implies c = c9;

theorem :: AFVECT0:25
  Mid a,p,a9 & Mid b,p,b9 implies a,b // b9,a9;

theorem :: AFVECT0:26
  Mid a,p,a9 & Mid b,q,b9 & MDist p,q implies a,b // b9,a9;

::
::                         Point Symmetry
::

definition
  let AFV;
  let a,b;
  func PSym(a,b) -> Element of AFV means
:: AFVECT0:def 4

  Mid b,a,it;
end;

theorem :: AFVECT0:27
  PSym(p,a) = b iff a,p // p,b;

theorem :: AFVECT0:28
  PSym(p,a) = a iff a = p or MDist a,p;

theorem :: AFVECT0:29
  PSym(p,PSym(p,a)) = a;

theorem :: AFVECT0:30
  PSym(p,a) = PSym(p,b) implies a = b;

theorem :: AFVECT0:31
  ex a st PSym(p,a) = b;

theorem :: AFVECT0:32
  a,b // PSym(p,b),PSym(p,a);

theorem :: AFVECT0:33
  a,b // c,d iff PSym(p,a),PSym(p,b) // PSym(p,c),PSym(p,d);

theorem :: AFVECT0:34
  MDist a,b iff MDist PSym(p,a),PSym(p,b);

theorem :: AFVECT0:35
  Mid a,b,c iff Mid PSym(p,a),PSym(p,b),PSym(p,c);

theorem :: AFVECT0:36
  PSym(p,a) = PSym(q,a) iff p = q or MDist p,q;

theorem :: AFVECT0:37
  PSym(q,PSym(p,PSym(q,a))) = PSym(PSym(q,p),a);

theorem :: AFVECT0:38
  PSym(p,PSym(q,a)) = PSym(q,PSym(p,a)) iff p = q or MDist p,q or MDist
  q,PSym(p,q);

theorem :: AFVECT0:39
  PSym(p,PSym(q,PSym(r,a))) = PSym(r,PSym(q,PSym(p,a)));

theorem :: AFVECT0:40
  ex d st PSym(a,PSym(b,PSym(c,p))) = PSym(d,p);

theorem :: AFVECT0:41
  ex c st PSym(a,PSym(c,p)) = PSym(c,PSym(b,p));

::
::                     Addition on the carrier
::

definition
  let AFV,o;
  let a,b;
  func Padd(o,a,b) -> Element of AFV means
:: AFVECT0:def 5

  o,a // b,it;
end;

notation
  let AFV,o;
  let a;
  synonym Pcom(o,a) for PSym(o,a);
end;

definition
  let AFV,o;

  func Padd(o) -> BinOp of the carrier of AFV means
:: AFVECT0:def 6

  for a,b holds it.(a ,b) = Padd(o,a,b);
end;

definition
  let AFV,o;
  func Pcom(o) -> UnOp of the carrier of AFV means
:: AFVECT0:def 7

  for a holds it.a = Pcom(o,a);
end;

definition
  let AFV,o;
  func GroupVect(AFV,o) -> strict addLoopStr equals
:: AFVECT0:def 8
  addLoopStr(#the carrier of
    AFV,Padd(o),o#);
end;

registration
  let AFV,o;
  cluster GroupVect(AFV,o) -> non empty;
end;

theorem :: AFVECT0:42
  the carrier of GroupVect(AFV,o) = the carrier of AFV & the addF of
  GroupVect(AFV,o) = Padd(o) & 0.GroupVect(AFV,o) = o;

reserve a,b,c for Element of GroupVect(AFV,o);

theorem :: AFVECT0:43
  for a,b being Element of GroupVect(AFV,o), a9,b9 being Element of AFV
  st a=a9 & b=b9 holds a + b = (Padd(o)).(a9,b9);

registration
  let AFV,o;
  cluster GroupVect(AFV,o) -> Abelian add-associative right_zeroed
    right_complementable;
end;

theorem :: AFVECT0:44
  for a being Element of GroupVect(AFV,o), a9 being Element of AFV
  st a=a9 holds -a = (Pcom(o)).a9;

theorem :: AFVECT0:45
  0.GroupVect(AFV,o) = o;

reserve a,b for Element of GroupVect(AFV,o);

theorem :: AFVECT0:46
  for a ex b st b + b = a;

registration
  let AFV,o;
  cluster GroupVect(AFV,o) -> Two_Divisible;
end;

::
::        Representation Theorem for Directed Geometrical Bundles
::

reserve AFV for AffVect,
  o for Element of AFV;

theorem :: AFVECT0:47
  for a being Element of GroupVect(AFV,o) st a + a = 0.(GroupVect(
  AFV,o)) holds a = 0.(GroupVect(AFV,o));

registration
  let AFV,o;
  cluster GroupVect(AFV,o) -> Fanoian;
end;

registration
  cluster strict non trivial for Uniquely_Two_Divisible_Group;
end;

definition
  mode Proper_Uniquely_Two_Divisible_Group is non trivial
    Uniquely_Two_Divisible_Group;
end;

theorem :: AFVECT0:48
  GroupVect(AFV,o) is Proper_Uniquely_Two_Divisible_Group;

registration
  let AFV,o;
  cluster GroupVect(AFV,o) -> non trivial;
end;

theorem :: AFVECT0:49
  for ADG being Proper_Uniquely_Two_Divisible_Group holds AV(ADG) is AffVect;

registration
  let ADG be Proper_Uniquely_Two_Divisible_Group;
  cluster AV(ADG) -> AffVect-like non trivial;
end;

theorem :: AFVECT0:50
  for AFV being strict AffVect holds for o being Element of AFV
  holds AFV = AV(GroupVect(AFV,o));

theorem :: AFVECT0:51
  for AS being strict AffinStruct holds (AS is AffVect iff ex ADG being
  Proper_Uniquely_Two_Divisible_Group st AS = AV(ADG) );

definition
  let X,Y be non empty addLoopStr;
  let f be Function of the carrier of X,the carrier of Y;
  pred f is_Iso_of X,Y means
:: AFVECT0:def 9

  f is one-to-one & rng(f) = the carrier of
Y & for a,b being Element of X holds f.(a+b) = (f.a)+(f.b) & f.(0.X) = 0.Y & f.
  (-a) = -(f.a);
end;

definition
  let X,Y be non empty addLoopStr;
  pred X,Y are_Iso means
:: AFVECT0:def 10

  ex f being Function of the carrier of X,the carrier of Y st f is_Iso_of X,Y;
end;

reserve ADG for Proper_Uniquely_Two_Divisible_Group;
reserve f for Function of the carrier of ADG,the carrier of ADG;

theorem :: AFVECT0:52
  for o9 being Element of ADG, o being Element of AV(ADG) st (for
x being Element of ADG holds f.x = o9+x) & o=o9 holds for a,b being Element of
ADG holds f.(a+b) =(Padd(o)).(f.a,f.b) & f.(0.ADG) = 0.(GroupVect(AV(ADG),o)) &
  f.(-a) = (Pcom(o)).(f.a);

theorem :: AFVECT0:53
  for o9 being Element of ADG st (for b being Element of ADG holds
  f.b = o9+b) holds f is one-to-one;

theorem :: AFVECT0:54
  for o9 being Element of ADG, o being Element of AV(ADG) st (for
  b being Element of ADG holds f.b = o9+b) holds rng(f) = the carrier of
  GroupVect(AV(ADG),o);

theorem :: AFVECT0:55
  for ADG being Proper_Uniquely_Two_Divisible_Group, o9 being Element of
ADG, o being Element of AV(ADG) st o=o9 holds ADG,GroupVect(AV(ADG),o) are_Iso;