Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Oriented Metric-Affine Plane --- Part II

by
Jaroslaw Zajkowski

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;
```