let r be Real; for V being RealLinearSpace
for v, u, p being VECTOR of V
for I being affinely-independent Subset of V st v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u holds
p in Int (I \ {v})
let V be RealLinearSpace; for v, u, p being VECTOR of V
for I being affinely-independent Subset of V st v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u holds
p in Int (I \ {v})
let v, u, p be VECTOR of V; for I being affinely-independent Subset of V st v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u holds
p in Int (I \ {v})
let I be affinely-independent Subset of V; ( v in I & u in Int I & p in conv (I \ {v}) & (r * v) + ((1 - r) * p) = u implies p in Int (I \ {v}) )
assume that
A1:
v in I
and
A2:
u in Int I
and
A3:
p in conv (I \ {v})
and
A4:
(r * v) + ((1 - r) * p) = u
; p in Int (I \ {v})
A5:
conv I c= Affin I
by RLAFFIN1:65;
I c= conv I
by RLAFFIN1:2;
then A6:
v in conv I
by A1;
conv (I \ {v}) c= conv I
by RLAFFIN1:3, XBOOLE_1:36;
then
p in conv I
by A3;
then A7:
u |-- I = ((1 - r) * (p |-- I)) + (r * (v |-- I))
by A4, A5, A6, RLAFFIN1:70;
A8:
Carrier (v |-- {v}) c= {v}
by RLVECT_2:def 6;
A9:
u in conv I
by A2, Def1;
then
Sum (u |-- I) = u
by A5, RLAFFIN1:def 7;
then A10:
Carrier (u |-- I) = I
by A2, A9, Th11, RLAFFIN1:71;
A11:
( {v} c= Affin {v} & v in {v} )
by RLAFFIN1:49, TARSKI:def 1;
{v} c= I
by A1, ZFMISC_1:31;
then A12:
v |-- I = v |-- {v}
by A11, RLAFFIN1:77;
A13:
conv (I \ {v}) c= Affin (I \ {v})
by RLAFFIN1:65;
then A14:
p |-- I = p |-- (I \ {v})
by A3, RLAFFIN1:77, XBOOLE_1:36;
A15:
I \ {v} c= Carrier (p |-- (I \ {v}))
Carrier (p |-- (I \ {v})) c= I \ {v}
by RLVECT_2:def 6;
then A19:
I \ {v} = Carrier (p |-- (I \ {v}))
by A15;
A20:
I \ {v} is affinely-independent
by RLAFFIN1:43, XBOOLE_1:36;
then
Sum (p |-- (I \ {v})) = p
by A3, A13, RLAFFIN1:def 7;
hence
p in Int (I \ {v})
by A3, A19, A20, Th12, RLAFFIN1:71; verum