let V be RealLinearSpace; :: thesis: for o, u, v, u1, v1 being VECTOR of V
for r being Real st o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 holds
( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) )
let o, u, v, u1, v1 be VECTOR of V; :: thesis: for r being Real st o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 holds
( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) )
let r be Real; :: thesis: ( o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 implies ( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) ) )
assume that
A1: o - u = r * (u1 - o) and
A2: r <> 0 and
A3: o,v '||' o,v1 and
A4: not o,u '||' o,v and
A5: u,v '||' u1,v1 ; :: thesis: ( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) )
A6: - r <> 0 by A2;
for r1, r2 being Real st (r1 * (u - o)) + (r2 * (v - o)) = 0. V holds
( r1 = 0 & r2 = 0 )
proof
let r1, r2 be Real; :: thesis: ( (r1 * (u - o)) + (r2 * (v - o)) = 0. V implies ( r1 = 0 & r2 = 0 ) )
assume (r1 * (u - o)) + (r2 * (v - o)) = 0. V ; :: thesis: ( r1 = 0 & r2 = 0 )
then A7: r1 * (u - o) = - (r2 * (v - o)) by RLVECT_1:6
.= r2 * (- (v - o)) by RLVECT_1:25
.= (- r2) * (v - o) by RLVECT_1:24 ;
assume ( r1 <> 0 or r2 <> 0 ) ; :: thesis: contradiction
then ( r1 <> 0 or - r2 <> 0 ) ;
then ( o,u // o,v or o,u // v,o ) by A7, ANALMETR:14;
hence contradiction by A4, GEOMTRAP:def 1; :: thesis: verum
end;
then reconsider X = OASpace V as OAffinSpace by ANALOAF:26;
set w = u1 + (((- r) ") * (v - u));
reconsider p = o, a = u, a1 = u1, b = v, b1 = v1, q = u1 + (((- r) ") * (v - u)) as Element of X by Th3;
a,b '||' a1,b1 by A5, Th4;
then A8: b,a '||' a1,b1 by DIRAF:22;
p,b '||' p,b1 by A3, Th4;
then A9: p,b,b1 are_collinear by DIRAF:def 5;
A10: (- r) * ((u1 + (((- r) ") * (v - u))) - u1) = (- r) * (((- r) ") * (v - u)) by RLSUB_2:61
.= ((- r) * ((- r) ")) * (v - u) by RLVECT_1:def 7
.= 1 * (v - u) by A6, XCMPLX_0:def 7 ;
then A11: v - u = (- r) * ((u1 + (((- r) ") * (v - u))) - u1) by RLVECT_1:def 8;
( u,v // u1,u1 + (((- r) ") * (v - u)) or u,v // u1 + (((- r) ") * (v - u)),u1 ) by A10, ANALMETR:14;
then u,v '||' u1,u1 + (((- r) ") * (v - u)) by GEOMTRAP:def 1;
then a,b '||' a1,q by Th4;
then A12: b,a '||' a1,q by DIRAF:22;
A13: (- r) * (o - (u1 + (((- r) ") * (v - u)))) = ((- r) * o) - ((- r) * (u1 + (((- r) ") * (v - u)))) by RLVECT_1:34
.= ((- r) * o) - (((- r) * u1) + ((- r) * (((- r) ") * (v - u)))) by RLVECT_1:def 5
.= ((- r) * o) - (((- r) * u1) + (((- r) * ((- r) ")) * (v - u))) by RLVECT_1:def 7
.= ((- r) * o) - (((- r) * u1) + (1 * (v - u))) by A6, XCMPLX_0:def 7
.= ((- r) * o) - (((- r) * u1) + (v - u)) by RLVECT_1:def 8
.= (((- r) * o) - ((- r) * u1)) - (v - u) by RLVECT_1:27
.= ((- r) * (o - u1)) - (v - u) by RLVECT_1:34
.= (r * (- (o - u1))) - (v - u) by RLVECT_1:24
.= (o - u) - (v - u) by A1, RLVECT_1:33
.= o - ((v - u) + u) by RLVECT_1:27
.= o - v by RLSUB_2:61
.= 1 * (o - v) by RLVECT_1:def 8 ;
then ( v,o // u1 + (((- r) ") * (v - u)),o or v,o // o,u1 + (((- r) ") * (v - u)) ) by ANALMETR:14;
then ( o,v // u1 + (((- r) ") * (v - u)),o or o,v // o,u1 + (((- r) ") * (v - u)) ) by ANALOAF:12;
then o,v '||' o,u1 + (((- r) ") * (v - u)) by GEOMTRAP:def 1;
then p,b '||' p,q by Th4;
then A14: p,b,q are_collinear by DIRAF:def 5;
1 * (u - o) = (- 1) * (- (u - o)) by RLVECT_1:26
.= (- 1) * (r * (u1 - o)) by A1, RLVECT_1:33
.= ((- 1) * r) * (u1 - o) by RLVECT_1:def 7
.= (- r) * (u1 - o) ;
then ( o,u // o,u1 or o,u // u1,o ) by ANALMETR:14;
then o,u '||' o,u1 by GEOMTRAP:def 1;
then p,a '||' p,a1 by Th4;
then A15: p,a,a1 are_collinear by DIRAF:def 5;
A16: not p,b,a are_collinear
proof
assume p,b,a are_collinear ; :: thesis: contradiction
then p,b '||' p,a by DIRAF:def 5;
then p,a '||' p,b by DIRAF:22;
hence contradiction by A4, Th4; :: thesis: verum
end;
A17: (- r) * ((u1 + (((- r) ") * (v - u))) - o) = r * (- ((u1 + (((- r) ") * (v - u))) - o)) by RLVECT_1:24
.= r * (o - (u1 + (((- r) ") * (v - u)))) by RLVECT_1:33
.= - (- (r * (o - (u1 + (((- r) ") * (v - u)))))) by RLVECT_1:17
.= - (r * (- (o - (u1 + (((- r) ") * (v - u)))))) by RLVECT_1:25
.= - (1 * (o - v)) by A13, RLVECT_1:24
.= - (o - v) by RLVECT_1:def 8
.= v - o by RLVECT_1:33 ;
u1 + (((- r) ") * (v - u)) = o + ((u1 + (((- r) ") * (v - u))) - o) by RLSUB_2:61
.= o + (((- r) ") * (v - o)) by A6, A17, ANALOAF:6 ;
hence ( v1 = u1 + (((- r) ") * (v - u)) & v1 = o + (((- r) ") * (v - o)) & v - u = (- r) * (v1 - u1) ) by A11, A16, A9, A14, A15, A12, A8, PASCH:4; :: thesis: verum