let r be Real; :: thesis: for V being RealLinearSpace
for v, w, p being VECTOR of V
for I being affinely-independent Subset of V st v in I & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) holds
r = (w |-- I) . v
let V be RealLinearSpace; :: thesis: for v, w, p being VECTOR of V
for I being affinely-independent Subset of V st v in I & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) holds
r = (w |-- I) . v
let v, w, p be VECTOR of V; :: thesis: for I being affinely-independent Subset of V st v in I & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) holds
r = (w |-- I) . v
let I be affinely-independent Subset of V; :: thesis: ( v in I & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) implies r = (w |-- I) . v )
assume that
A1: v in I and
w in Affin I and
A2: p in Affin (I \ {v}) and
A3: w = (r * v) + ((1 - r) * p) ; :: thesis: r = (w |-- I) . v
A4: I c= conv I by CONVEX1:41;
Carrier (p |-- (I \ {v})) c= I \ {v} by RLVECT_2:def 6;
then not v in Carrier (p |-- (I \ {v})) by ZFMISC_1:56;
then A5: (p |-- (I \ {v})) . v = 0 ;
I \ {v} c= I by XBOOLE_1:36;
then ( Affin (I \ {v}) c= Affin I & I c= Affin I ) by Lm7, Th52;
hence (w |-- I) . v = (((1 - r) * (p |-- I)) + (r * (v |-- I))) . v by A1, A2, A3, Th70
.= (((1 - r) * (p |-- I)) . v) + ((r * (v |-- I)) . v) by RLVECT_2:def 10
.= (((1 - r) * (p |-- I)) . v) + (r * ((v |-- I) . v)) by RLVECT_2:def 11
.= ((1 - r) * ((p |-- I) . v)) + (r * ((v |-- I) . v)) by RLVECT_2:def 11
.= ((1 - r) * ((p |-- I) . v)) + (r * 1) by A1, A4, Th72
.= ((1 - r) * ((p |-- (I \ {v})) . v)) + (r * 1) by A2, Th77, XBOOLE_1:36
.= r by A5 ;
:: thesis: verum