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

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