let r be Real; :: thesis: for V being RealLinearSpace
for v1, v2 being VECTOR of V
for I being affinely-independent Subset of V st v1 in Affin I & v2 in Affin I holds
(((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
let V be RealLinearSpace; :: thesis: for v1, v2 being VECTOR of V
for I being affinely-independent Subset of V st v1 in Affin I & v2 in Affin I holds
(((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
let v1, v2 be VECTOR of V; :: thesis: for I being affinely-independent Subset of V st v1 in Affin I & v2 in Affin I holds
(((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
let I be affinely-independent Subset of V; :: thesis: ( v1 in Affin I & v2 in Affin I implies (((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I)) )
assume that
A1: v1 in Affin I and
A2: v2 in Affin I ; :: thesis: (((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
set rv12 = ((1 - r) * v1) + (r * v2);
A3: ((1 - r) * v1) + (r * v2) in Affin I by A1, A2, RUSUB_4:def 4;
( (1 - r) * (v1 |-- I) is Linear_Combination of I & r * (v2 |-- I) is Linear_Combination of I ) by RLVECT_2:44;
then A4: ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I)) is Linear_Combination of I by RLVECT_2:38;
A5: Sum (((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))) = (Sum ((1 - r) * (v1 |-- I))) + (Sum (r * (v2 |-- I))) by RLVECT_3:1
.= ((1 - r) * (Sum (v1 |-- I))) + (Sum (r * (v2 |-- I))) by RLVECT_3:2
.= ((1 - r) * (Sum (v1 |-- I))) + (r * (Sum (v2 |-- I))) by RLVECT_3:2
.= ((1 - r) * v1) + (r * (Sum (v2 |-- I))) by A1, Def7
.= ((1 - r) * v1) + (r * v2) by A2, Def7 ;
sum (((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))) = (sum ((1 - r) * (v1 |-- I))) + (sum (r * (v2 |-- I))) by Th34
.= ((1 - r) * (sum (v1 |-- I))) + (sum (r * (v2 |-- I))) by Th35
.= ((1 - r) * (sum (v1 |-- I))) + (r * (sum (v2 |-- I))) by Th35
.= ((1 - r) * 1) + (r * (sum (v2 |-- I))) by A1, Def7
.= ((1 - r) * 1) + (r * 1) by A2, Def7
.= 1 ;
hence (((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I)) by A3, A4, A5, Def7; :: thesis: verum