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}))

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

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

Carrier (p |-- (I \ {v})) c= I \ {v}
by RLVECT_2:def 6;
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;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

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