:: Oriented Metric-Affine Plane - Part II
::  by Jaros{\l}aw Zajkowski
::
:: Received June 19, 1992
:: Copyright (c) 1992-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 RLVECT_1, XBOOLE_0, ANALOAF, SUBSET_1, ANALMETR, ANALORT,
      STRUCT_0, SYMSP_1, DIRORT;
 notations STRUCT_0, RLVECT_1, ANALOAF, ANALMETR, ANALORT;
 constructors ANALMETR, ANALORT;
 registrations ANALORT, ANALMETR;


begin

reserve V for RealLinearSpace;
reserve x,y for VECTOR of V;

notation
  let AS be non empty OrtStr;
  let a,b,c,d be Element of AS;
  synonym a,b '//' c,d for a,b _|_ c,d;
end;

theorem :: DIRORT:1
  Gen x,y implies (for u,u1,v,v1,w being Element of CESpace(V,x,y)
  holds ((u,u '//' v,w) & (u,v '//' w,w) & (u,v '//' u1,v1 & u,v '//' v1,u1
  implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w
or u,v '//' w,v1) & (u,v '//' u1,v1 implies v,u '//' v1,u1) & (u,v '//' u1,v1 &
  u,v '//' v1,w implies u,v '//' u1,w) & (u,u1 '//' v,v1 implies v,v1 '//' u,u1
  or v,v1 '//' u1,u))) & (for u,v,w being Element of CESpace(V,x,y) holds ex u1
  being Element of CESpace(V,x,y) st w<>u1 & w,u1 '//' u,v ) & for u,v,w being
Element of CESpace(V,x,y) holds ex u1 being Element of CESpace(V,x,y) st w<>u1
  & u,v '//' w,u1;

theorem :: DIRORT:2
  Gen x,y implies (for u,u1,v,v1,w being Element of CMSpace(V,x,y)
  holds ((u,u '//' v,w) & (u,v '//' w,w) & (u,v '//' u1,v1 & u,v '//' v1,u1
  implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w
or u,v '//' w,v1) & (u,v '//' u1,v1 implies v,u '//' v1,u1) & (u,v '//' u1,v1 &
  u,v '//' v1,w implies u,v '//' u1,w) & (u,u1 '//' v,v1 implies v,v1 '//' u,u1
  or v,v1 '//' u1,u))) & (for u,v,w being Element of CMSpace(V,x,y) holds ex u1
  being Element of CMSpace(V,x,y) st w<>u1 & w,u1 '//' u,v ) & for u,v,w being
Element of CMSpace(V,x,y) holds ex u1 being Element of CMSpace(V,x,y) st w<>u1
  & u,v '//' w,u1;

definition
  let IT be non empty OrtStr;
  attr IT is Oriented_Orthogonality_Space-like means
:: DIRORT:def 1

  (for u,u1,v,v1,w
being Element of IT holds ((u,u '//' v,w) & (u,v '//' w,w) & (u,v '//' u1,v1 &
u,v '//' v1,u1 implies u=v or u1=v1) & (u,v '//' u1,v1 & u,v '//' u1,w implies
u,v '//' v1,w or u,v '//' w,v1) & (u,v '//' u1,v1 implies v,u '//' v1,u1) & (u,
v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w) & (u,u1 '//' v,v1 implies v
,v1 '//' u,u1 or v,v1 '//' u1,u))) & (for u,v,w being Element of IT holds ex u1
being Element of IT st w<>u1 & w,u1 '//' u,v ) & for u,v,w being Element of IT
  holds ex u1 being Element of IT st w<>u1 & u,v '//' w,u1;
end;

registration
  cluster Oriented_Orthogonality_Space-like for non empty OrtStr;
end;

definition
  mode Oriented_Orthogonality_Space is Oriented_Orthogonality_Space-like non
    empty OrtStr;
end;

theorem :: DIRORT:3
  Gen x,y implies CMSpace(V,x,y) is Oriented_Orthogonality_Space;

theorem :: DIRORT:4
  Gen x,y implies CESpace(V,x,y) is Oriented_Orthogonality_Space;

reserve AS for Oriented_Orthogonality_Space;
reserve u,u1,u2,u3,v,v1,v2,v3,w,w1 for Element of AS;

theorem :: DIRORT:5
  for u,v,w being Element of AS holds ex u1 being Element of AS st u1,w
  '//' u,v & u1<>w;

theorem :: DIRORT:6
  for u,v,w being Element of AS holds ex u1 being Element of AS st u<>u1
  & (v,w '//' u,u1 or v,w '//' u1,u);

definition
  let AS be Oriented_Orthogonality_Space;
  let a,b,c,d be Element of AS;
  pred a,b _|_ c,d means
:: DIRORT:def 2
  a,b '//' c,d or a,b '//' d,c;
end;

definition
  let AS be Oriented_Orthogonality_Space;
  let a,b,c,d be Element of AS;
  pred a,b // c,d means
:: DIRORT:def 3

  ex e,f being Element of AS st e<>f & e,f '//' a ,b & e,f '//' c,d;
end;

definition
  let IT be Oriented_Orthogonality_Space;
  attr IT is bach_transitive means
:: DIRORT:def 4

  for u,u1,u2,v,v1,v2,w,w1 being
Element of IT holds ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 implies
  (w=w1 or v=v1 or u,u1 '//' u2,v2) );
end;

definition
  let IT be Oriented_Orthogonality_Space;
  attr IT is right_transitive means
:: DIRORT:def 5

  for u,u1,u2,v,v1,v2,w,w1 being
Element of IT holds ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies
  (w=w1 or v=v1 or u,u1 '//' u2,v2) );
end;

definition
  let IT be Oriented_Orthogonality_Space;
  attr IT is left_transitive means
:: DIRORT:def 6

  for u,u1,u2,v,v1,v2,w,w1 being
Element of IT holds ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies
  (u=u1 or v=v1 or u2,v2 '//' w,w1) );
end;

definition
  let IT be Oriented_Orthogonality_Space;
  attr IT is Euclidean_like means
:: DIRORT:def 7

  for u,u1,v,v1 being Element of IT
  holds (u,u1 '//' v,v1 implies v,v1 '//' u1,u );
end;

definition
  let IT be Oriented_Orthogonality_Space;
  attr IT is Minkowskian_like means
:: DIRORT:def 8

  for u,u1,v,v1 being Element of IT
  holds (u,u1 '//' v,v1 implies v,v1 '//' u,u1 );
end;

theorem :: DIRORT:7
  u,u1 // w,w & w,w // u,u1;

theorem :: DIRORT:8
  u,u1 // v,v1 implies v,v1 // u,u1;

theorem :: DIRORT:9
  u,u1 // v,v1 implies u1,u // v1,v;

theorem :: DIRORT:10
  AS is left_transitive iff for v,v1,w,w1,u2,v2 holds (v,v1 // u2,v2 & v
  ,v1 '//' w,w1 & v<>v1 implies u2,v2 '//' w,w1);

theorem :: DIRORT:11
  AS is bach_transitive iff for u,u1,u2,v,v1,v2 holds (u,u1 '//' v
  ,v1 & v,v1 // u2,v2 & v<>v1 implies u,u1 '//' u2,v2);

theorem :: DIRORT:12
  AS is bach_transitive implies for u,u1,v,v1,w,w1 holds (u,u1 // v,v1 &
  v,v1 // w,w1 & v<>v1 implies u,u1 // w,w1);

theorem :: DIRORT:13
  Gen x,y & AS=CESpace(V,x,y) implies AS is Euclidean_like
  left_transitive right_transitive bach_transitive;

registration
  cluster Euclidean_like left_transitive right_transitive bach_transitive
    for Oriented_Orthogonality_Space;
end;

theorem :: DIRORT:14
  Gen x,y & AS=CMSpace(V,x,y) implies AS is Minkowskian_like
  left_transitive right_transitive bach_transitive;

registration
  cluster Minkowskian_like left_transitive right_transitive bach_transitive
    for Oriented_Orthogonality_Space;
end;

theorem :: DIRORT:15
  AS is left_transitive implies AS is right_transitive;

theorem :: DIRORT:16
  AS is left_transitive implies AS is bach_transitive;

theorem :: DIRORT:17
  AS is bach_transitive implies (AS is right_transitive iff for u,u1,v,
v1,u2,v2 holds ( u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2<>v2 implies u,u1 // v,
  v1) );

theorem :: DIRORT:18
  AS is right_transitive & (AS is Euclidean_like or AS is
  Minkowskian_like) implies AS is left_transitive;