The abstract of the Mizar article:

Oriented Metric-Affine Plane --- Part II

by

Jaroslaw Zajkowski

Received June 19, 1992

MML identifier: DIRORT

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, ANALOAF, ANALMETR, ANALORT, SYMSP_1, DIRORT;
 notation STRUCT_0, RLVECT_1, ANALOAF, ANALMETR, ANALORT;
 constructors ANALMETR, ANALORT, XBOOLE_0;
 clusters ANALOAF, ANALORT, ZFMISC_1, XBOOLE_0;


begin

 reserve V for RealLinearSpace;

 reserve x,y for VECTOR of V;

definition let AS be non empty AffinStruct;
           let a,b,c,d be Element of AS;
  redefine pred a,b // c,d;
  synonym a,b '//' c,d;
end;

theorem :: DIRORT:1
Gen x,y implies (for u,u1,v,v1,w,w1,w2 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,w1,w2 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 AffinStruct;
  attr IT is Oriented_Orthogonality_Space-like means
:: DIRORT:def 1
   (for u,u1,v,v1,w,w1,w2 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;

definition
  cluster Oriented_Orthogonality_Space-like (non empty AffinStruct);
 end;

definition
  mode Oriented_Orthogonality_Space is Oriented_Orthogonality_Space-like
   (non empty AffinStruct);
end;

canceled;

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

theorem :: DIRORT:5
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:6
  for u,v,w being Element of AS holds
  ex u1 being Element of AS st
    u1,w '//' u,v & u1<>w;

canceled;

theorem :: DIRORT:8
  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:9
  u,u1 // w,w & w,w // u,u1;

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

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

theorem :: DIRORT:12
  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:13
 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:14
  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:15
 Gen x,y & AS=CESpace(V,x,y) implies AS is
Euclidean_like left_transitive right_transitive bach_transitive;

definition
  cluster Euclidean_like left_transitive right_transitive bach_transitive
          Oriented_Orthogonality_Space; end;

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

definition
  cluster Minkowskian_like left_transitive right_transitive bach_transitive
          Oriented_Orthogonality_Space;
end;

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

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

theorem :: DIRORT:19
  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:20
  AS is right_transitive & (AS is Euclidean_like or AS is Minkowskian_like)
implies AS is left_transitive;