let V be RealLinearSpace; :: thesis: for x, y being VECTOR of V
for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CESpace (V,x,y) holds
( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
let x, y be VECTOR of V; :: thesis: for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CESpace (V,x,y) holds
( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
let AS be Oriented_Orthogonality_Space; :: thesis: ( Gen x,y & AS = CESpace (V,x,y) implies ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) )
assume that
A1: Gen x,y and
A2: AS = CESpace (V,x,y) ; :: thesis: ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
A3: CESpace (V,x,y) = OrtStr(# the carrier of V,(CORTE (V,x,y)) #) by ANALORT:def 7;
A4: now :: thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; :: thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
thus ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) :: thesis: verum
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 & not w9 = w19 & not v9 = v19 implies u9,u19,u29,v29 are_COrte_wrt x,y ) by A1, ANALORT:44;
hence ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A2, ANALORT:54; :: thesis: verum
end;
end;
A5: now :: thesis: for u, u1, v, v1 being Element of AS st u,u1 '//' v,v1 holds
v,v1 '//' u1,u
let u, u1, v, v1 be Element of AS; :: thesis: ( u,u1 '//' v,v1 implies v,v1 '//' u1,u )
thus ( u,u1 '//' v,v1 implies v,v1 '//' u1,u ) :: thesis: verum
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 ( u,u1 '//' v,v1 implies v,v1 '//' u1,u ) by A2, ANALORT:54; :: thesis: verum
end;
end;
A6: now :: thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; :: thesis: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 )
thus ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 ) :: thesis: verum
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 & not u9 = u19 & not v9 = v19 implies u29,v29,w9,w19 are_COrte_wrt x,y ) by A1, ANALORT:46;
hence ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 ) by A2, ANALORT:54; :: thesis: verum
end;
end;
now :: thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; :: thesis: ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
thus ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) :: thesis: verum
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 & not w9 = w19 & not v9 = v19 implies u9,u19,u29,v29 are_COrte_wrt x,y ) by A1, ANALORT:42;
hence ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A2, ANALORT:54; :: thesis: verum
end;
end;
hence ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) by A4, A6, A5; :: thesis: verum