let V be RealLinearSpace; 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; 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; ( 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
; ( 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 )
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
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; verum