let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for p, p1 being Element of (AMSpace (V,w,y)) st Gen w,y & p <> p1 holds
for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
let w, y be VECTOR of V; :: thesis: for p, p1 being Element of (AMSpace (V,w,y)) st Gen w,y & p <> p1 holds
for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
let p, p1 be Element of (AMSpace (V,w,y)); :: thesis: ( Gen w,y & p <> p1 implies for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q ) )
assume that
A1: Gen w,y and
A2: p <> p1 ; :: thesis: for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
let q be Element of (AMSpace (V,w,y)); :: thesis: ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
reconsider u = p, v = q, u1 = p1 as Element of V ;
u1 - u <> 0. V by A2, RLVECT_1:21;
then consider a being Real such that
A3: (v - u) - (a * (u1 - u)),u1 - u are_Ort_wrt w,y by A1, Th13;
set v1 = u + (a * (u1 - u));
reconsider q1 = u + (a * (u1 - u)) as Element of (AMSpace (V,w,y)) ;
v - (u + (a * (u1 - u))) = (v - u) - (a * (u1 - u)) by RLVECT_1:27;
then u1 - u,v - (u + (a * (u1 - u))) are_Ort_wrt w,y by A3;
then u,u1,u + (a * (u1 - u)),v are_Ort_wrt w,y ;
then A4: p,p1 _|_ q1,q by Th21;
a * (u1 - u) = (a * (u1 - u)) + (0. V) by RLVECT_1:4
.= (a * (u1 - u)) + (u - u) by RLVECT_1:15
.= (u + (a * (u1 - u))) - u by RLVECT_1:def 3
.= 1 * ((u + (a * (u1 - u))) - u) by RLVECT_1:def 8 ;
then p,p1 // p,q1 by Th22;
hence ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q ) by A4; :: thesis: verum