let V be RealLinearSpace; :: thesis: for w, y, u, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st u = u1 # t1 & u = u2 # t2 & u = v1 # w1 & u = v2 # w2 & u1,u2,v1,v2 are_DTr_wrt w,y holds
t1,t2,w1,w2 are_DTr_wrt w,y
let w, y be VECTOR of V; :: thesis: for u, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st u = u1 # t1 & u = u2 # t2 & u = v1 # w1 & u = v2 # w2 & u1,u2,v1,v2 are_DTr_wrt w,y holds
t1,t2,w1,w2 are_DTr_wrt w,y
let u, u1, u2, v1, v2, t1, t2, w1, w2 be VECTOR of V; :: thesis: ( u = u1 # t1 & u = u2 # t2 & u = v1 # w1 & u = v2 # w2 & u1,u2,v1,v2 are_DTr_wrt w,y implies t1,t2,w1,w2 are_DTr_wrt w,y )
assume that
A1: ( u = u1 # t1 & u = u2 # t2 ) and
A2: ( u = v1 # w1 & u = v2 # w2 ) and
A3: u1,u2,v1,v2 are_DTr_wrt w,y ; :: thesis: t1,t2,w1,w2 are_DTr_wrt w,y
A4: u1,u2 // v1,v2 by A3;
set p = u1 # u2;
set q = v1 # v2;
set r = t1 # t2;
set s = w1 # w2;
A5: (v1 # v2) # (w1 # w2) = u # u by A2, Th6
.= u ;
(u1 # u2) # (t1 # t2) = u # u by A1, Th6
.= u ;
then A6: (w1 # w2) - (t1 # t2) = - ((v1 # v2) - (u1 # u2)) by A5, Lm3
.= (- 1) * ((v1 # v2) - (u1 # u2)) by RLVECT_1:16 ;
A7: ( u2 - u1 = - (t2 - t1) & v2 - v1 = - (w2 - w1) ) by A1, A2, Lm3;
A8: t1,t2 // w1,w2
proof
per cases ( u1 = u2 or v1 = v2 or ( u1 <> u2 & v1 <> v2 ) ) ;
suppose u1 = u2 ; :: thesis: t1,t2 // w1,w2
then t1 = t2 by A1, Th7;
hence t1,t2 // w1,w2 by ANALOAF:9; :: thesis: verum
end;
suppose v1 = v2 ; :: thesis: t1,t2 // w1,w2
then w1 = w2 by A2, Th7;
hence t1,t2 // w1,w2 by ANALOAF:9; :: thesis: verum
end;
suppose ( u1 <> u2 & v1 <> v2 ) ; :: thesis: t1,t2 // w1,w2
then consider a, b being Real such that
A9: ( 0 < a & 0 < b ) and
A10: a * (u2 - u1) = b * (v2 - v1) by A4, ANALOAF:def 1;
a * (t2 - t1) = a * (- (- (t2 - t1))) by RLVECT_1:17
.= - (b * (- (w2 - w1))) by A7, A10, RLVECT_1:25
.= b * (- (- (w2 - w1))) by RLVECT_1:25
.= b * (w2 - w1) by RLVECT_1:17 ;
hence t1,t2 // w1,w2 by A9, ANALOAF:def 1; :: thesis: verum
end;
end;
end;
w2 - w1 = - (v2 - v1) by A2, Lm3;
then A11: w2 - w1 = (- 1) * (v2 - v1) by RLVECT_1:16;
v1,v2,u1 # u2,v1 # v2 are_Ort_wrt w,y by A3;
then v2 - v1,(v1 # v2) - (u1 # u2) are_Ort_wrt w,y by ANALMETR:def 3;
then w2 - w1,(w1 # w2) - (t1 # t2) are_Ort_wrt w,y by A6, A11, ANALMETR:6;
then A12: w1,w2,t1 # t2,w1 # w2 are_Ort_wrt w,y by ANALMETR:def 3;
t2 - t1 = - (u2 - u1) by A1, Lm3;
then A13: t2 - t1 = (- 1) * (u2 - u1) by RLVECT_1:16;
u1,u2,u1 # u2,v1 # v2 are_Ort_wrt w,y by A3;
then u2 - u1,(v1 # v2) - (u1 # u2) are_Ort_wrt w,y by ANALMETR:def 3;
then t2 - t1,(w1 # w2) - (t1 # t2) are_Ort_wrt w,y by A6, A13, ANALMETR:6;
then t1,t2,t1 # t2,w1 # w2 are_Ort_wrt w,y by ANALMETR:def 3;
hence t1,t2,w1,w2 are_DTr_wrt w,y by A8, A12; :: thesis: verum