let r be Real; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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}))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in I \ {v} or x in Carrier (p |-- (I \ {v})) )
assume A16: x in I \ {v} ; :: thesis: x in Carrier (p |-- (I \ {v}))
then reconsider w = x as Element of V ;
A17: w in I by A16, ZFMISC_1:56;
w <> v by A16, ZFMISC_1:56;
then not w in Carrier (v |-- {v}) by A8, TARSKI:def 1;
then A18: (v |-- I) . w = 0 by A12;
(u |-- I) . w = (((1 - r) * (p |-- I)) . w) + ((r * (v |-- I)) . w) by A7, RLVECT_2:def 10
.= (((1 - r) * (p |-- I)) . w) + (r * ((v |-- I) . w)) by RLVECT_2:def 11
.= (1 - r) * ((p |-- I) . w) by A18, RLVECT_2:def 11 ;
then (p |-- I) . w <> 0 by A10, A17, RLVECT_2:19;
hence x in Carrier (p |-- (I \ {v})) by A14; :: thesis: verum
end;
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; :: thesis: verum