let r, s be Real; for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
let V be RealLinearSpace; for v being VECTOR of V
for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
let v be VECTOR of V; for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
let L1, L2 be Linear_Combination of V; ( L1 . v <> L2 . v implies ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ) )
set u1 = L1 . v;
set u2 = L2 . v;
A1: ((r * L1) + ((1 - r) * L2)) . v =
((r * L1) . v) + (((1 - r) * L2) . v)
by RLVECT_2:def 10
.=
(r * (L1 . v)) + (((1 - r) * L2) . v)
by RLVECT_2:def 11
.=
(r * (L1 . v)) + (((- r) + 1) * (L2 . v))
by RLVECT_2:def 11
.=
(r * ((L1 . v) - (L2 . v))) + (L2 . v)
;
assume A2:
L1 . v <> L2 . v
; ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
then A3:
(L1 . v) - (L2 . v) <> 0
;
A4:
(L2 . v) - (L1 . v) <> 0
by A2;
hereby ( r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) implies ((r * L1) + ((1 - r) * L2)) . v = s )
assume
((r * L1) + ((1 - r) * L2)) . v = s
;
r = ((L2 . v) - s) / ((L2 . v) - (L1 . v))then
r * ((L2 . v) - (L1 . v)) = ((L2 . v) - s) * 1
by A1;
then
r / 1
= ((L2 . v) - s) / ((L2 . v) - (L1 . v))
by A4, XCMPLX_1:94;
hence
r = ((L2 . v) - s) / ((L2 . v) - (L1 . v))
;
verum
end;
assume
r = ((L2 . v) - s) / ((L2 . v) - (L1 . v))
; ((r * L1) + ((1 - r) * L2)) . v = s
hence ((r * L1) + ((1 - r) * L2)) . v =
((((L2 . v) - s) / (- ((L1 . v) - (L2 . v)))) * ((L1 . v) - (L2 . v))) + (L2 . v)
by A1
.=
(((- ((L2 . v) - s)) / ((L1 . v) - (L2 . v))) * ((L1 . v) - (L2 . v))) + (L2 . v)
by XCMPLX_1:192
.=
(- ((L2 . v) - s)) + (L2 . v)
by A3, XCMPLX_1:87
.=
s
;
verum