let r, s be Real; for V being RealLinearSpace
for v, u being VECTOR of V
for I being affinely-independent Subset of V
for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds
( w1 = w2 & r = s )
let V be RealLinearSpace; for v, u being VECTOR of V
for I being affinely-independent Subset of V
for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds
( w1 = w2 & r = s )
let v, u be VECTOR of V; for I being affinely-independent Subset of V
for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds
( w1 = w2 & r = s )
let I be affinely-independent Subset of V; for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds
( w1 = w2 & r = s )
let p1, p2, w1, w2 be Element of V; ( v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 implies ( w1 = w2 & r = s ) )
assume that
A1:
v in conv I
and
A2:
u in conv I
and
A3:
not u in conv (I \ {p1})
and
A4:
not u in conv (I \ {p2})
and
A5:
w1 in conv (I \ {p1})
and
A6:
w2 in conv (I \ {p2})
and
A7:
(r * u) + ((1 - r) * w1) = v
and
A8:
(s * u) + ((1 - s) * w2) = v
and
A9:
r < 1
and
A10:
s < 1
; ( w1 = w2 & r = s )
set Lu = u |-- I;
set Lv = v |-- I;
set Lw1 = w1 |-- I;
set Lw2 = w2 |-- I;
A11:
conv I c= Affin I
by RLAFFIN1:65;
A12:
(u |-- I) . p2 > 0
conv (I \ {p2}) c= Affin (I \ {p2})
by RLAFFIN1:65;
then
w2 |-- I = w2 |-- (I \ {p2})
by A6, RLAFFIN1:77, XBOOLE_1:36;
then
Carrier (w2 |-- I) c= I \ {p2}
by RLVECT_2:def 6;
then
not p2 in Carrier (w2 |-- I)
by ZFMISC_1:56;
then A14:
(w2 |-- I) . p2 = 0
;
A15:
(u |-- I) . p1 > 0
conv (I \ {p1}) c= Affin (I \ {p1})
by RLAFFIN1:65;
then
w1 |-- I = w1 |-- (I \ {p1})
by A5, RLAFFIN1:77, XBOOLE_1:36;
then
Carrier (w1 |-- I) c= I \ {p1}
by RLVECT_2:def 6;
then
not p1 in Carrier (w1 |-- I)
by ZFMISC_1:56;
then A17:
(w1 |-- I) . p1 = 0
;
A18:
conv (I \ {p2}) c= conv I
by RLAFFIN1:3, XBOOLE_1:36;
then
w2 in conv I
by A6;
then
(s * (u |-- I)) + ((1 - s) * (w2 |-- I)) = v |-- I
by A2, A8, A11, RLAFFIN1:70;
then (v |-- I) . p2 =
((s * (u |-- I)) . p2) + (((1 - s) * (w2 |-- I)) . p2)
by RLVECT_2:def 10
.=
(s * ((u |-- I) . p2)) + (((1 - s) * (w2 |-- I)) . p2)
by RLVECT_2:def 11
.=
(s * ((u |-- I) . p2)) + ((1 - s) * ((w2 |-- I) . p2))
by RLVECT_2:def 11
.=
s * ((u |-- I) . p2)
by A14
;
then A19:
(v |-- I) . p2 < 1 * ((u |-- I) . p2)
by A10, A12, XREAL_1:68;
then A20:
((u |-- I) . p2) - ((v |-- I) . p2) >= ((v |-- I) . p2) - ((v |-- I) . p2)
by XREAL_1:9;
A21:
conv (I \ {p1}) c= conv I
by RLAFFIN1:3, XBOOLE_1:36;
then
(w1 |-- I) . p2 >= 0
by A5, RLAFFIN1:71;
then A22:
(1 / (1 - s)) - 0 >= (1 / (1 - s)) - (((w1 |-- I) . p2) / (((u |-- I) . p2) - ((v |-- I) . p2)))
by A20, XREAL_1:10;
w1 in conv I
by A5, A21;
then
v |-- I = (r * (u |-- I)) + ((1 - r) * (w1 |-- I))
by A2, A7, A11, RLAFFIN1:70;
then (v |-- I) . p1 =
((r * (u |-- I)) . p1) + (((1 - r) * (w1 |-- I)) . p1)
by RLVECT_2:def 10
.=
(r * ((u |-- I) . p1)) + (((1 - r) * (w1 |-- I)) . p1)
by RLVECT_2:def 11
.=
(r * ((u |-- I) . p1)) + ((1 - r) * ((w1 |-- I) . p1))
by RLVECT_2:def 11
.=
r * ((u |-- I) . p1)
by A17
;
then A23:
(v |-- I) . p1 < 1 * ((u |-- I) . p1)
by A9, A15, XREAL_1:68;
then A24:
((u |-- I) . p1) - ((v |-- I) . p1) >= ((v |-- I) . p1) - ((v |-- I) . p1)
by XREAL_1:9;
w2 = ((1 / (1 - s)) * v) + ((1 - (1 / (1 - s))) * u)
by A8, A10, Lm1;
then A25:
w2 |-- I = ((1 / (1 - s)) * (v |-- I)) + ((1 - (1 / (1 - s))) * (u |-- I))
by A1, A2, A11, RLAFFIN1:70;
then A26:
1 / (1 - s) = (((u |-- I) . p2) - 0) / (((u |-- I) . p2) - ((v |-- I) . p2))
by A14, A19, RLAFFIN1:81;
A27:
w1 = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u)
by A7, A9, Lm1;
then A28:
w1 |-- I = ((1 / (1 - r)) * (v |-- I)) + ((1 - (1 / (1 - r))) * (u |-- I))
by A1, A2, A11, RLAFFIN1:70;
then A29: 1 / (1 - r) =
(((u |-- I) . p2) - ((w1 |-- I) . p2)) / (((u |-- I) . p2) - ((v |-- I) . p2))
by A19, RLAFFIN1:81
.=
(1 / (1 - s)) - (((w1 |-- I) . p2) / (((u |-- I) . p2) - ((v |-- I) . p2)))
by A26, XCMPLX_1:120
;
(w2 |-- I) . p1 >= 0
by A6, A18, RLAFFIN1:71;
then A30:
(1 / (1 - r)) - 0 >= (1 / (1 - r)) - (((w2 |-- I) . p1) / (((u |-- I) . p1) - ((v |-- I) . p1)))
by A24, XREAL_1:10;
A31:
1 / (1 - r) = (((u |-- I) . p1) - 0) / (((u |-- I) . p1) - ((v |-- I) . p1))
by A17, A23, A28, RLAFFIN1:81;
1 / (1 - s) =
(((u |-- I) . p1) - ((w2 |-- I) . p1)) / (((u |-- I) . p1) - ((v |-- I) . p1))
by A23, A25, RLAFFIN1:81
.=
(1 / (1 - r)) - (((w2 |-- I) . p1) / (((u |-- I) . p1) - ((v |-- I) . p1)))
by A31, XCMPLX_1:120
;
then
1 - r = 1 - s
by A30, A22, A29, XCMPLX_1:59, XXREAL_0:1;
hence
( w1 = w2 & r = s )
by A8, A10, A27, Lm1; verum