:: Oriented Metric-Affine Plane - Part II
:: by Jaros{\l}aw Zajkowski
::
:: Received June 19, 1992
:: Copyright (c) 1992-2026 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;
theorems ANALMETR, ANALORT;
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 Th1:
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
proof
assume
A1: Gen x,y;
set S=CESpace(V,x,y);
A2: S= OrtStr (# the carrier of V,CORTE(V,x,y) #) by ANALORT:def 7;
thus for u,u1,v,v1,w being Element of S 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)
proof
let u,u1,v,v1,w be Element of S;
reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1 as Element of V by A2;
u9,u9,v9,w9 are_COrte_wrt x,y by ANALORT:20;
hence u,u '//' v,w by ANALORT:54;
u9,v9,w9,w9 are_COrte_wrt x,y by ANALORT:22;
hence u,v '//' w,w by ANALORT:54;
u9,v9,u19,v19 are_COrte_wrt x,y & u9,v9,v19,u19 are_COrte_wrt x,y
implies u9=v9 or u19=v19 by A1,ANALORT:30;
hence u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1 by ANALORT:54;
u9,v9,u19,v19 are_COrte_wrt x,y & u9,v9,u19,w9 are_COrte_wrt x,y
implies u9,v9,v19,w9 are_COrte_wrt x,y or u9,v9,w9,v19 are_COrte_wrt x,y by A1,
ANALORT:32;
hence
u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1
by ANALORT:54;
u9,v9,u19,v19 are_COrte_wrt x,y implies v9,u9,v19,u19 are_COrte_wrt x
,y by ANALORT:34;
hence u,v '//' u1,v1 implies v,u '//' v1,u1 by ANALORT:54;
u9,v9,u19,v19 are_COrte_wrt x,y & u9,v9,v19,w9 are_COrte_wrt x,y
implies u9,v9,u19,w9 are_COrte_wrt x,y by A1,ANALORT:36;
hence u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w by ANALORT:54;
u9,u19,v9,v19 are_COrte_wrt x,y implies v9,v19,u9,u19 are_COrte_wrt x
,y or v9,v19,u19,u9 are_COrte_wrt x,y by A1,ANALORT:18;
hence u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u by ANALORT:54
;
end;
thus for u,v,w being Element of S holds ex u1 being Element of S st w<>u1 &
w,u1 '//' u,v
proof
let u,v,w be Element of S;
reconsider u9=u,v9=v,w9=w as Element of V by A2;
consider u19 being Element of V such that
A3: w9<>u19 and
A4: w9,u19,u9,v9 are_COrte_wrt x,y by A1,ANALORT:38;
reconsider u1=u19 as Element of S by A2;
w,u1 '//' u,v by A4,ANALORT:54;
hence thesis by A3;
end;
let u,v,w be Element of S;
reconsider u9=u,v9=v,w9=w as Element of V by A2;
consider u19 being Element of V such that
A5: w9<>u19 and
A6: u9,v9,w9,u19 are_COrte_wrt x,y by A1,ANALORT:40;
reconsider u1=u19 as Element of S by A2;
u,v '//' w,u1 by A6,ANALORT:54;
hence thesis by A5;
end;
theorem Th2:
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
proof
assume
A1: Gen x,y;
set S=CMSpace(V,x,y);
A2: S= OrtStr(# the carrier of V,CORTM(V,x,y) #) by ANALORT:def 8;
thus for u,u1,v,v1,w being Element of S 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)
proof
let u,u1,v,v1,w be Element of S;
reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1 as Element of V by A2;
u9,u9,v9,w9 are_COrtm_wrt x,y by ANALORT:21;
hence u,u '//' v,w by ANALORT:55;
u9,v9,w9,w9 are_COrtm_wrt x,y by ANALORT:23;
hence u,v '//' w,w by ANALORT:55;
u9,v9,u19,v19 are_COrtm_wrt x,y & u9,v9,v19,u19 are_COrtm_wrt x,y
implies u9=v9 or u19=v19 by A1,ANALORT:31;
hence u,v '//' u1,v1 & u,v '//' v1,u1 implies u=v or u1=v1 by ANALORT:55;
u9,v9,u19,v19 are_COrtm_wrt x,y & u9,v9,u19,w9 are_COrtm_wrt x,y
implies u9,v9,v19,w9 are_COrtm_wrt x,y or u9,v9,w9,v19 are_COrtm_wrt x,y by A1,
ANALORT:33;
hence
u,v '//' u1,v1 & u,v '//' u1,w implies u,v '//' v1,w or u,v '//' w,v1
by ANALORT:55;
u9,v9,u19,v19 are_COrtm_wrt x,y implies v9,u9,v19,u19 are_COrtm_wrt x
,y by ANALORT:35;
hence u,v '//' u1,v1 implies v,u '//' v1,u1 by ANALORT:55;
u9,v9,u19,v19 are_COrtm_wrt x,y & u9,v9,v19,w9 are_COrtm_wrt x,y
implies u9,v9,u19,w9 are_COrtm_wrt x,y by A1,ANALORT:37;
hence u,v '//' u1,v1 & u,v '//' v1,w implies u,v '//' u1,w by ANALORT:55;
u9,u19,v9,v19 are_COrtm_wrt x,y implies v9,v19,u9,u19 are_COrtm_wrt x
, y or v9,v19,u19,u9 are_COrtm_wrt x,y by A1,ANALORT:19;
hence u,u1 '//' v,v1 implies v,v1 '//' u,u1 or v,v1 '//' u1,u by ANALORT:55
;
end;
thus for u,v,w being Element of S holds ex u1 being Element of S st w<>u1 &
w,u1 '//' u,v
proof
let u,v,w be Element of S;
reconsider u9=u,v9=v,w9=w as Element of V by A2;
consider u19 being Element of V such that
A3: w9<>u19 and
A4: w9,u19,u9,v9 are_COrtm_wrt x,y by A1,ANALORT:39;
reconsider u1=u19 as Element of S by A2;
w,u1 '//' u,v by A4,ANALORT:55;
hence thesis by A3;
end;
let u,v,w be Element of S;
reconsider u9=u,v9=v,w9=w as Element of V by A2;
consider u19 being Element of V such that
A5: w9<>u19 and
A6: u9,v9,w9,u19 are_COrtm_wrt x,y by A1,ANALORT:41;
reconsider u1=u19 as Element of S by A2;
u,v '//' w,u1 by A6,ANALORT:55;
hence thesis by A5;
end;
definition
let IT be non empty OrtStr;
attr IT is Oriented_Orthogonality_Space-like means
:Def1:
(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;
existence
proof
consider V,x,y such that
A1: Gen x,y by ANALMETR:3;
take C = CESpace(V,x,y);
thus (for u,u1,v,v1,w being Element of C 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 C holds ex u1 being Element of C st w<>u1 & w,u1 '//' u,v ) &
for u,v,w being Element of C holds ex u1 being Element of C st w<>u1 & u,v '//'
w,u1 by A1,Th1;
end;
end;
definition
mode Oriented_Orthogonality_Space is Oriented_Orthogonality_Space-like non
empty OrtStr;
end;
theorem Th3:
Gen x,y implies CMSpace(V,x,y) is Oriented_Orthogonality_Space
proof
assume
A1: Gen x,y;
then
A2: 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 by Th2;
A3: 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 by A1,Th2;
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) by A1
,Th2;
hence thesis by A2,A3,Def1;
end;
theorem Th4:
Gen x,y implies CESpace(V,x,y) is Oriented_Orthogonality_Space
proof
assume
A1: Gen x,y;
then
A2: 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 by Th1;
A3: 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 by A1,Th1;
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) by A1
,Th1;
hence thesis by A2,A3,Def1;
end;
reserve AS for Oriented_Orthogonality_Space;
reserve u,u1,u2,u3,v,v1,v2,v3,w,w1 for Element of AS;
theorem
for u,v,w being Element of AS holds ex u1 being Element of AS st u1,w
'//' u,v & u1<>w
proof
let u,v,w;
consider u1 such that
A1: u1<>w and
A2: w,u1 '//' v,u by Def1;
u1,w '//' u,v by A2,Def1;
hence thesis by A1;
end;
theorem
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)
proof
let u,v,w;
consider u1 such that
A1: u<>u1 and
A2: u,u1 '//' v,w by Def1;
v,w '//' u,u1 or v,w '//' u1,u by A2,Def1;
hence thesis by A1;
end;
definition
let AS be Oriented_Orthogonality_Space;
let a,b,c,d be Element of AS;
pred a,b _|_ c,d means
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
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
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
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
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
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
for u,u1,v,v1 being Element of IT
holds (u,u1 '//' v,v1 implies v,v1 '//' u,u1 );
end;
theorem
u,u1 // w,w & w,w // u,u1
proof
set v = the Element of AS;
consider v1 such that
A1: v1<>v and
A2: v,v1 '//' u,u1 by Def1;
v,v1 '//' w,w by Def1;
hence thesis by A1,A2;
end;
theorem
u,u1 // v,v1 implies v,v1 // u,u1;
theorem
u,u1 // v,v1 implies u1,u // v1,v
proof
assume u,u1 // v,v1;
then consider w,w1 such that
A1: w<>w1 and
A2: w,w1 '//' u,u1 and
A3: w,w1 '//' v,v1;
A4: w1,w '//' v1,v by A3,Def1;
w1,w '//' u1,u by A2,Def1;
hence thesis by A1,A4;
end;
theorem
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)
proof
A1: (for v,v1,w,w1,u2,v2 holds (v,v1 // u2,v2 & v,v1 '//' w,w1 & v<>v1
implies u2,v2 '//' w,w1)) implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS
holds ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=v1
or u2,v2 '//' w,w1) )
proof
assume
A2: for v,v1,w,w1,u2,v2 holds (v,v1 // u2,v2 & v,v1 '//' w,w1 & v<>v1
implies u2,v2 '//' w,w1);
let u,u1,u2,v,v1,v2,w,w1;
assume that
A3: u,u1 '//' v,v1 and
A4: v,v1 '//' w,w1 and
A5: u,u1 '//' u2,v2;
now
assume that
A6: u<>u1 and
v<>v1;
v,v1 // u2,v2 by A3,A5,A6;
hence thesis by A2,A4;
end;
hence thesis;
end;
thus thesis by A1;
end;
theorem
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)
proof
A1: (for u,u1,u2,v,v1,v2 holds (u,u1 '//' v,v1 & v,v1 // u2,v2 & v<>v1
implies u,u1 '//' u2,v2)) implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS
holds ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 implies (w=w1 or v=v1
or u,u1 '//' u2,v2) )
proof
assume
A2: for u,u1,u2,v,v1,v2 holds (u,u1 '//' v,v1 & v,v1 // u2,v2 & v<>v1
implies u,u1 '//' u2,v2);
let u,u1,u2,v,v1,v2,w,w1;
assume that
A3: u,u1 '//' v,v1 and
A4: w,w1 '//' v,v1 and
A5: w,w1 '//' u2,v2;
now
assume that
A6: w<>w1 and
v<>v1;
v,v1 // u2,v2 by A4,A5,A6;
hence thesis by A2,A3;
end;
hence thesis;
end;
thus thesis by A1;
end;
theorem
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)
proof
assume
A1: AS is bach_transitive;
let u,u1,v,v1,w,w1;
assume that
A2: u,u1 // v,v1 and
A3: v,v1 // w,w1 and
A4: v<>v1;
consider v2,v3 such that
A5: v2<>v3 and
A6: v2,v3 '//' u,u1 and
A7: v2,v3 '//' v,v1 by A2;
v2,v3 '//' w,w1 by A1,A3,A4,A7;
hence thesis by A5,A6;
end;
theorem Th13:
Gen x,y & AS=CESpace(V,x,y) implies AS is Euclidean_like
left_transitive right_transitive bach_transitive
proof
assume that
A1: Gen x,y and
A2: AS=CESpace(V,x,y);
A3: CESpace(V,x,y)=OrtStr (# the carrier of V,CORTE(V,x,y) #) by
ANALORT:def 7;
A4: now
let u,u1,u2,v,v1,v2,w,w1 be Element of AS;
thus u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v=
v1 or u,u1 '//' u2,v2 )
proof
reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element
of V by A2,A3;
u9,u19,v9,v19 are_COrte_wrt x,y & v9,v19,w9,w19 are_COrte_wrt x,y &
u29,v29,w9,w19 are_COrte_wrt x,y implies (w9=w19 or v9=v19 or u9,u19,u29,v29
are_COrte_wrt x,y) by A1,ANALORT:44;
hence thesis by A2,ANALORT:54;
end;
end;
A5: now
let u,u1,v,v1 be Element of AS;
thus u,u1 '//' v,v1 implies v,v1 '//' u1,u
proof
reconsider u9=u,v9=v,u19=u1,v19=v1 as Element of V by A2,A3;
u9,u19,v9,v19 are_COrte_wrt x,y implies v9,v19,u19,u9 are_COrte_wrt
x,y by A1,ANALORT:18;
hence thesis by A2,ANALORT:54;
end;
end;
A6: now
let u,u1,u2,v,v1,v2,w,w1 be Element of AS;
thus u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=
v1 or u2,v2 '//' w,w1 )
proof
reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element
of V by A2,A3;
u9,u19,v9,v19 are_COrte_wrt x,y & v9,v19,w9,w19 are_COrte_wrt x,y &
u9,u19,u29,v29 are_COrte_wrt x,y implies (u9=u19 or v9=v19 or u29,v29,w9,w19
are_COrte_wrt x,y) by A1,ANALORT:46;
hence thesis by A2,ANALORT:54;
end;
end;
now
let u,u1,u2,v,v1,v2,w,w1 be Element of AS;
thus u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 implies (w=w1 or v=
v1 or u,u1 '//' u2,v2 )
proof
reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element
of V by A2,A3;
u9,u19,v9,v19 are_COrte_wrt x,y & w9,w19,v9,v19 are_COrte_wrt x,y &
w9,w19,u29,v29 are_COrte_wrt x,y implies (w9=w19 or v9=v19 or u9,u19,u29,v29
are_COrte_wrt x,y) by A1,ANALORT:42;
hence thesis by A2,ANALORT:54;
end;
end;
hence thesis by A4,A6,A5;
end;
registration
cluster Euclidean_like left_transitive right_transitive bach_transitive
for Oriented_Orthogonality_Space;
existence
proof
consider V,x,y such that
A1: Gen x,y by ANALMETR:3;
reconsider AS=CESpace(V,x,y) as Oriented_Orthogonality_Space by A1,Th4;
take AS;
thus thesis by A1,Th13;
end;
end;
theorem Th14:
Gen x,y & AS=CMSpace(V,x,y) implies AS is Minkowskian_like
left_transitive right_transitive bach_transitive
proof
assume that
A1: Gen x,y and
A2: AS=CMSpace(V,x,y);
A3: CMSpace(V,x,y)=OrtStr (# the carrier of V,CORTM(V,x,y) #) by
ANALORT:def 8;
A4: now
let u,u1,u2,v,v1,v2,w,w1 be Element of AS;
thus u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v=
v1 or u,u1 '//' u2,v2 )
proof
reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element
of V by A2,A3;
u9,u19,v9,v19 are_COrtm_wrt x,y & v9,v19,w9,w19 are_COrtm_wrt x,y &
u29,v29,w9,w19 are_COrtm_wrt x,y implies (w9=w19 or v9=v19 or u9,u19,u29,v29
are_COrtm_wrt x,y) by A1,ANALORT:45;
hence thesis by A2,ANALORT:55;
end;
end;
A5: now
let u,u1,v,v1 be Element of AS;
thus u,u1 '//' v,v1 implies v,v1 '//' u,u1
proof
reconsider u9=u,v9=v,u19=u1,v19=v1 as Element of V by A2,A3;
u9,u19,v9,v19 are_COrtm_wrt x,y implies v9,v19,u9,u19 are_COrtm_wrt
x,y by A1,ANALORT:19;
hence thesis by A2,ANALORT:55;
end;
end;
A6: now
let u,u1,u2,v,v1,v2,w,w1 be Element of AS;
thus u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=
v1 or u2,v2 '//' w,w1 )
proof
reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element
of V by A2,A3;
u9,u19,v9,v19 are_COrtm_wrt x,y & v9,v19,w9,w19 are_COrtm_wrt x,y &
u9,u19,u29,v29 are_COrtm_wrt x,y implies (u9=u19 or v9=v19 or u29,v29,w9,w19
are_COrtm_wrt x,y) by A1,ANALORT:47;
hence thesis by A2,ANALORT:55;
end;
end;
now
let u,u1,u2,v,v1,v2,w,w1 be Element of AS;
thus u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 implies (w=w1 or v=
v1 or u,u1 '//' u2,v2 )
proof
reconsider u9=u,v9=v,w9=w,u19=u1,v19=v1,w19=w1,u29=u2,v29=v2 as Element
of V by A2,A3;
u9,u19,v9,v19 are_COrtm_wrt x,y & w9,w19,v9,v19 are_COrtm_wrt x,y &
w9,w19,u29,v29 are_COrtm_wrt x,y implies (w9=w19 or v9=v19 or u9,u19,u29,v29
are_COrtm_wrt x,y) by A1,ANALORT:43;
hence thesis by A2,ANALORT:55;
end;
end;
hence thesis by A4,A6,A5;
end;
registration
cluster Minkowskian_like left_transitive right_transitive bach_transitive
for Oriented_Orthogonality_Space;
existence
proof
consider V,x,y such that
A1: Gen x,y by ANALMETR:3;
reconsider AS=CMSpace(V,x,y) as Oriented_Orthogonality_Space by A1,Th3;
take AS;
thus thesis by A1,Th14;
end;
end;
theorem Th15:
AS is left_transitive implies AS is right_transitive
proof
(for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( (u,u1 '//' v,v1 &
v,v1 '//' w,w1 & u,u1 '//' u2,v2 ) implies (u=u1 or v=v1 or u2,v2 '//' w,w1 )))
implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v,v1 & v
,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v=v1 or u,u1 '//' u2,v2 ))
proof
assume
A1: for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v,
v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=v1 or u2,v2 '//' w,w1
));
let u,u1,u2,v,v1,v2,w,w1;
assume that
A2: u,u1 '//' v,v1 and
A3: v,v1 '//' w,w1 and
A4: u2,v2 '//' w,w1;
A5: ( w=w1 or v=v1 or u,u1 '//' u2,v2 or u,u1 '//' v2,u2 ) implies (w=w1
or v=v1 or u,u1 '//' u2,v2 )
proof
now
A6: now
assume v2,u2 '//' w,w1;
then u2,v2 '//' w1,w by Def1;
then u2=v2 or w=w1 by A4,Def1;
hence thesis;
end;
u=u1 implies thesis by Def1;
hence thesis by A1,A2,A3,A6;
end;
hence thesis;
end;
A7: now
assume that
A8: w,w1 '//' v,v1 and
A9: v,v1 '//' u,u1 and
A10: w,w1 '//' v2,u2;
w=w1 or v=v1 or v2,u2 '//' u,u1 by A1,A8,A9,A10;
hence thesis by A5,Def1;
end;
A11: now
assume that
A12: w,w1 '//' v1,v and
A13: v,v1 '//' u,u1 and
A14: w,w1 '//' v2,u2;
v1,v '//' u1,u by A13,Def1;
then w=w1 or v=v1 or v2,u2 '//' u1,u by A1,A12,A14;
then w=w1 or v=v1 or u2,v2 '//' u,u1 by Def1;
hence thesis by A5,Def1;
end;
A15: now
assume that
A16: w,w1 '//' v1,v and
A17: v,v1 '//' u,u1 and
A18: w,w1 '//' u2,v2;
v1,v '//' u1,u by A17,Def1;
then w=w1 or v=v1 or u2,v2 '//' u1,u by A1,A16,A18;
then w=w1 or v=v1 or v2,u2 '//' u,u1 by Def1;
hence thesis by A5,Def1;
end;
A19: now
assume that
A20: w,w1 '//' v1,v and
A21: v,v1 '//' u1,u and
A22: w,w1 '//' v2,u2;
v1,v '//' u,u1 by A21,Def1;
then w=w1 or v=v1 or v2,u2 '//' u,u1 by A1,A20,A22;
hence thesis by A5,Def1;
end;
A23: now
assume that
A24: w,w1 '//' v1,v and
A25: v,v1 '//' u1,u and
A26: w,w1 '//' u2,v2;
v1,v '//' u,u1 by A25,Def1;
then w=w1 or v1=v or u2,v2 '//' u,u1 by A1,A24,A26;
hence thesis by A5,Def1;
end;
A27: now
assume that
A28: w,w1 '//' v,v1 and
A29: v,v1 '//' u1,u and
A30: w,w1 '//' v2,u2;
w=w1 or v=v1 or v2,u2 '//' u1,u by A1,A28,A29,A30;
then w=w1 or v=v1 or u1,u '//' u2,v2 or u1,u '//' v2,u2 by Def1;
hence thesis by A5,Def1;
end;
A31: now
assume that
A32: w,w1 '//' v,v1 and
A33: v,v1 '//' u1,u and
A34: w,w1 '//' u2,v2;
w=w1 or v=v1 or u2,v2 '//' u1,u by A1,A32,A33,A34;
then w=w1 or v=v1 or u1,u '//' u2,v2 or u1,u '//' v2,u2 by Def1;
hence thesis by A5,Def1;
end;
now
assume that
A35: w,w1 '//' v,v1 and
A36: v,v1 '//' u,u1 and
A37: w,w1 '//' u2,v2;
w=w1 or v=v1 or u2,v2 '//' u,u1 by A1,A35,A36,A37;
hence thesis by A5,Def1;
end;
hence thesis by A2,A3,A4,A7,A31,A27,A15,A11,A23,A19,Def1;
end;
hence thesis;
end;
theorem
AS is left_transitive implies AS is bach_transitive
proof
(for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( (u,u1 '//' v,v1 &
v,v1 '//' w,w1 & u,u1 '//' u2,v2 ) implies (u=u1 or v=v1 or u2,v2 '//' w,w1 )))
implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v,v1 & w
,w1 '//' v,v1 & w,w1 '//' u2,v2 implies (w=w1 or v=v1 or u,u1 '//' u2,v2))
proof
assume
A1: for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ( u,u1 '//' v,
v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=v1 or u2,v2 '//' w,w1
));
let u,u1,u2,v,v1,v2,w,w1;
A2: AS is left_transitive implies AS is right_transitive by Th15;
then
A3: u,u1 '//' v,v1 & v,v1 '//' w1,w & u2,v2 '//' w1,w implies thesis by A1;
assume that
A4: u,u1 '//' v,v1 and
A5: w,w1 '//' v,v1 and
A6: w,w1 '//' u2,v2;
A7: ( v=v1 or w=w1 or u,u1 '//' u2,v2 or u,u1 '//' v2,u2) implies (w=w1 or
v=v1 or u,u1 '//' u2,v2)
proof
A8: now
assume that
A9: u,u1 '//' v2,u2 and
A10: u<>u1 and
A11: v<>v1 and
w<>w1;
A12: now
assume
A13: u2,v2 '//' u,u1;
then
A14: u2,v2 '//' w,w1 by A2,A1,A4,A5,A10,A11;
A15: now
assume u2,v2 '//' w1,w;
then w=w1 or u2=v2 by A14,Def1;
hence thesis;
end;
w1,w '//' v2,u2 by A6,Def1;
then u2,v2 '//' w1,w or u2=v2 by A2,A1,A9,A10,A13;
hence thesis by A15;
end;
A16: now
A17: w1,w '//' v1,v by A5,Def1;
assume
A18: u2,v2 '//' u1,u;
u1,u '//' v1,v by A4,Def1;
then
A19: u2,v2 '//' w1,w by A2,A1,A10,A11,A18,A17;
A20: now
assume u2,v2 '//' w,w1;
then w=w1 or u2=v2 by A19,Def1;
hence thesis;
end;
u1,u '//' u2,v2 by A9,Def1;
then u2,v2 '//' w,w1 or u2=v2 by A2,A1,A6,A10,A18;
hence thesis by A20;
end;
v2,u2 '//' u,u1 or v2,u2 '//' u1,u by A9,Def1;
hence thesis by A16,A12,Def1;
end;
assume v=v1 or w=w1 or u,u1 '//' u2,v2 or u,u1 '//' v2,u2;
hence thesis by A8,Def1;
end;
A21: now
assume that
A22: u,u1 '//' v,v1 and
A23: v,v1 '//' w,w1 and
A24: u2,v2 '//' w1,w;
v2,u2 '//' w,w1 by A24,Def1;
hence thesis by A2,A1,A7,A22,A23;
end;
A25: now
assume that
A26: u,u1 '//' v,v1 and
A27: v,v1 '//' w1,w and
A28: u2,v2 '//' w,w1;
v2,u2 '//' w1,w by A28,Def1;
hence thesis by A2,A1,A7,A26,A27;
end;
u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies thesis by A2,A1;
hence thesis by A4,A5,A6,A21,A3,A25,Def1;
end;
hence thesis;
end;
theorem
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) )
proof
A1: (for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds ((u,u1 '//' v,v1 & v
,v1 '//' w,w1 & u2,v2 '//' w,w1 ) implies (w=w1 or v=v1 or u,u1 '//' u2,v2 )))
implies for u,u1,v,v1,u2,v2 holds ( u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2<>v2
implies u,u1 // v,v1)
proof
set w = the Element of AS;
assume
A2: for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds u,u1 '//' v,v1
& v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v=v1 or u,u1 '//' u2,v2 );
let u,u1,v,v1,u2,v2;
assume that
A3: u,u1 '//' u2,v2 and
A4: v,v1 '//' u2,v2 and
A5: u2<>v2;
consider w1 such that
A6: w<>w1 and
A7: w,w1 '//' u,u1 by Def1;
A8: now
set w = the Element of AS;
assume
A9: u=u1;
consider w1 such that
A10: w<>w1 and
A11: w,w1 '//' v,v1 by Def1;
w,w1 '//' u,u by Def1;
hence thesis by A9,A10,A11;
end;
now
assume u<>u1;
then w,w1 '//' v,v1 by A2,A3,A4,A5,A7;
hence thesis by A6,A7;
end;
hence thesis by A8;
end;
assume
A12: AS is bach_transitive;
(for u,u1,v,v1,u2,v2 holds ((u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2<>v2
) implies u,u1 // v,v1)) implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS
holds ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 implies (w=w1 or v=v1
or u,u1 '//' u2,v2 ))
proof
assume
A13: for u,u1,v,v1,u2,v2 holds u,u1 '//' u2,v2 & v,v1 '//' u2,v2 & u2
<>v2 implies u,u1 // v,v1;
let u,u1,u2,v,v1,v2,w,w1;
assume that
A14: u,u1 '//' v,v1 and
A15: v,v1 '//' w,w1 and
A16: u2,v2 '//' w,w1;
now
assume that
A17: w<>w1 and
v<>v1;
v,v1 // u2,v2 by A13,A15,A16,A17;
then ex u3,v3 st u3<>v3 & u3,v3 '//' v,v1 & u3,v3 '//' u2,v2;
hence thesis by A12,A14;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem
AS is right_transitive & (AS is Euclidean_like or AS is
Minkowskian_like) implies AS is left_transitive
proof
assume
A1: AS is right_transitive;
(for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies v,v1
'//' u,u1 ) or for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies
v,v1 '//' u1,u )) implies for u,u1,u2,v,v1,v2,w,w1 being Element of AS holds (
u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 implies (u=u1 or v=v1 or u2,
v2 '//' w,w1 ))
proof
assume
A2: for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies v,
v1 '//' u,u1 ) or for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1
implies v,v1 '//' u1,u );
let u,u1,u2,v,v1,v2,w,w1;
assume that
A3: u,u1 '//' v,v1 and
A4: v,v1 '//' w,w1 and
A5: u,u1 '//' u2,v2;
A6: now
assume
A7: for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies
v,v1 '//' u1,u );
now
w,w1 '//' v1,v by A4,A7;
then
A8: w1,w '//' v,v1 by Def1;
A9: u2,v2 '//' u1,u by A5,A7;
assume that
A10: u<>u1 and
A11: v<>v1;
v,v1 '//' u1,u by A3,A7;
then w1,w '//' u2,v2 by A1,A10,A11,A8,A9;
hence thesis by A7;
end;
hence thesis;
end;
now
assume
A12: for u,u1,v,v1 being Element of AS holds (u,u1 '//' v,v1 implies
v,v1 '//' u,u1 );
now
A13: u2,v2 '//' u,u1 by A5,A12;
A14: w,w1 '//' v,v1 by A4,A12;
assume that
A15: u<>u1 and
A16: v<>v1;
v,v1 '//' u,u1 by A3,A12;
then w,w1 '//' u2,v2 by A1,A15,A16,A14,A13;
hence thesis by A12;
end;
hence thesis;
end;
hence thesis by A2,A6;
end;
hence thesis;
end;