let V be RealLinearSpace; for u, u1, v, v1 being VECTOR of V st u,v // u1,v1 holds
u,v '||' u # v1,v # u1
let u, u1, v, v1 be VECTOR of V; ( u,v // u1,v1 implies u,v '||' u # v1,v # u1 )
assume A1:
u,v // u1,v1
; u,v '||' u # v1,v # u1
per cases
( u = v or u1 = v1 or ( u <> v & u1 <> v1 ) )
;
suppose
(
u <> v &
u1 <> v1 )
;
u,v '||' u # v1,v # u1then consider a,
b being
Real such that
0 < a
and A2:
0 < b
and A3:
a * (v - u) = b * (v1 - u1)
by A1, ANALOAF:def 1;
A4:
b * (u1 - v1) =
b * (- (v1 - u1))
by RLVECT_1:33
.=
- (a * (v - u))
by A3, RLVECT_1:25
.=
a * (- (v - u))
by RLVECT_1:25
.=
(- a) * (v - u)
by RLVECT_1:24
;
set p =
u # v1;
set q =
v # u1;
set A =
b * 2;
set D =
b - a;
A5:
b * 2
<> 0
by A2;
(b * 2) * ((v # u1) - (u # v1)) =
b * (2 * ((v # u1) - (u # v1)))
by RLVECT_1:def 7
.=
b * (((1 + 1) * (v # u1)) - (2 * (u # v1)))
by RLVECT_1:34
.=
b * (((1 * (v # u1)) + (1 * (v # u1))) - (2 * (u # v1)))
by RLVECT_1:def 6
.=
b * (((v # u1) + (1 * (v # u1))) - (2 * (u # v1)))
by RLVECT_1:def 8
.=
b * (((v # u1) + (v # u1)) - (2 * (u # v1)))
by RLVECT_1:def 8
.=
b * ((v + u1) - (2 * (u # v1)))
by Def2
.=
b * (v + (u1 - ((1 + 1) * (u # v1))))
by RLVECT_1:def 3
.=
b * (v + (u1 - ((1 * (u # v1)) + (1 * (u # v1)))))
by RLVECT_1:def 6
.=
b * (v + (u1 - ((u # v1) + (1 * (u # v1)))))
by RLVECT_1:def 8
.=
b * (v + (u1 - ((u # v1) + (u # v1))))
by RLVECT_1:def 8
.=
b * (v + (u1 - (u + v1)))
by Def2
.=
b * (v + ((u1 - v1) - u))
by RLVECT_1:27
.=
b * ((v + (u1 - v1)) - u)
by RLVECT_1:def 3
.=
b * ((u1 - v1) + (v - u))
by RLVECT_1:def 3
.=
((- a) * (v - u)) + (b * (v - u))
by A4, RLVECT_1:def 5
.=
(b + (- a)) * (v - u)
by RLVECT_1:def 6
.=
(b - a) * (v - u)
;
then
(
u,
v // u # v1,
v # u1 or
u,
v // v # u1,
u # v1 )
by A5, ANALMETR:14;
hence
u,
v '||' u # v1,
v # u1
;
verum end;