let r, s be Real; :: thesis: for V being RealLinearSpace
for v1, v2, w being VECTOR of V
for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
let V be RealLinearSpace; :: thesis: for v1, v2, w being VECTOR of V
for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
let v1, v2, w be VECTOR of V; :: thesis: for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
let A be Subset of V; :: thesis: ( not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) implies ( r = s & v1 = v2 ) )
assume that
A1: ( not w in Affin A & v1 in A & v2 in A ) and
A2: r <> 1 and
A3: (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) ; :: thesis: ( r = s & v1 = v2 )
r * w = (r * w) + (0. V)
.= (r * w) + (((1 - r) * v1) - ((1 - r) * v1)) by RLVECT_1:15
.= ((s * w) + ((1 - s) * v2)) - ((1 - r) * v1) by A3, RLVECT_1:28
.= (((1 - s) * v2) - ((1 - r) * v1)) + (s * w) by RLVECT_1:28 ;
then (r * w) - (s * w) = ((1 - s) * v2) - ((1 - r) * v1) by RLVECT_4:1;
then A4: (r - s) * w = ((1 - s) * v2) - ((1 - r) * v1) by RLVECT_1:35;
A5: A c= Affin A by Lm7;
per cases ( r <> s or r = s ) ;
suppose r <> s ; :: thesis: ( r = s & v1 = v2 )
then A6: r - s <> 0 ;
A7: (1 / (r - s)) * (1 - s) = ((r - s) - (r - 1)) / (r - s) by XCMPLX_1:99
.= ((r - s) / (r - s)) - ((r - 1) / (r - s)) by XCMPLX_1:120
.= 1 - ((r - 1) / (r - s)) by A6, XCMPLX_1:60 ;
A8: - ((1 / (r - s)) * (1 - r)) = - ((1 - r) / (r - s)) by XCMPLX_1:99
.= (- (1 - r)) / (r - s) by XCMPLX_1:187 ;
1 = (r - s) * (1 / (r - s)) by A6, XCMPLX_1:106;
then w = ((1 / (r - s)) * (r - s)) * w by RLVECT_1:def 8
.= (1 / (r - s)) * ((r - s) * w) by RLVECT_1:def 7
.= ((1 / (r - s)) * ((1 - s) * v2)) - ((1 / (r - s)) * ((1 - r) * v1)) by A4, RLVECT_1:34
.= (((1 / (r - s)) * (1 - s)) * v2) - ((1 / (r - s)) * ((1 - r) * v1)) by RLVECT_1:def 7
.= (((1 / (r - s)) * (1 - s)) * v2) - (((1 / (r - s)) * (1 - r)) * v1) by RLVECT_1:def 7
.= (((1 / (r - s)) * (1 - s)) * v2) + (- (((1 / (r - s)) * (1 - r)) * v1)) by RLVECT_1:def 11
.= ((1 - ((r - 1) / (r - s))) * v2) + (((r - 1) / (r - s)) * v1) by A7, A8, RLVECT_4:3 ;
hence ( r = s & v1 = v2 ) by A1, A5, RUSUB_4:def 4; :: thesis: verum
end;
suppose A9: r = s ; :: thesis: ( r = s & v1 = v2 )
A10: 1 - r <> 0 by A2;
(1 - r) * v1 = (1 - r) * v2 by A3, A9, RLVECT_1:8;
hence ( r = s & v1 = v2 ) by A9, A10, RLVECT_1:36; :: thesis: verum
end;
end;