let n be Nat; :: thesis: for u, v being Element of (TOP-REAL n)
for a, b being Real st ((1 - a) * u) + (a * v) = ((1 - b) * v) + (b * u) holds
(1 - (a + b)) * u = (1 - (a + b)) * v
let u, v be Element of (TOP-REAL n); :: thesis: for a, b being Real st ((1 - a) * u) + (a * v) = ((1 - b) * v) + (b * u) holds
(1 - (a + b)) * u = (1 - (a + b)) * v
let a, b be Real; :: thesis: ( ((1 - a) * u) + (a * v) = ((1 - b) * v) + (b * u) implies (1 - (a + b)) * u = (1 - (a + b)) * v )
assume A1: ((1 - a) * u) + (a * v) = ((1 - b) * v) + (b * u) ; :: thesis: (1 - (a + b)) * u = (1 - (a + b)) * v
reconsider ru = u, rv = v as Element of REAL n by EUCLID:22;
A2: (((1 - a) * ru) + (a * rv)) - (a * rv) = (1 - a) * ru
proof
( (1 - a) * ru in REAL n & a * rv in REAL n ) ;
then reconsider t1 = (1 - a) * u, t2 = a * v as Element of n -tuples_on REAL by EUCLID:def 1;
(((1 - a) * ru) + (a * rv)) - (a * rv) = (t1 + t2) - t2
.= t1 by RVSUM_1:42 ;
hence (((1 - a) * ru) + (a * rv)) - (a * rv) = (1 - a) * ru ; :: thesis: verum
end;
A3: ((((1 - b) * rv) - (a * rv)) + (b * ru)) - (b * ru) = ((1 - b) * rv) - (a * rv)
proof
reconsider t1 = ((1 - b) * rv) - (a * rv), t2 = b * ru as Element of n -tuples_on REAL by EUCLID:def 1;
((((1 - b) * rv) - (a * rv)) + (b * ru)) - (b * ru) = (t1 + t2) - t2
.= t1 by RVSUM_1:42 ;
hence ((((1 - b) * rv) - (a * rv)) + (b * ru)) - (b * ru) = ((1 - b) * rv) - (a * rv) ; :: thesis: verum
end;
(1 - a) * ru = (((1 - b) * rv) + (b * ru)) + (- (a * rv)) by A1, A2, RVSUM_1:31
.= (((1 - b) * rv) + (- (a * rv))) + (b * ru) by RVSUM_1:15 ;
then ((1 - a) * ru) - (b * ru) = ((1 - b) * rv) - (a * rv) by A3, RVSUM_1:31;
then ((1 - a) * ru) + (- (b * ru)) = ((1 - b) * rv) - (a * rv) by RVSUM_1:31
.= ((1 - b) * rv) + (- (a * rv)) by RVSUM_1:31 ;
then ((1 - a) * ru) + ((- 1) * (b * ru)) = ((1 - b) * rv) + (- (a * rv)) by RVSUM_1:54;
then ((1 - a) * ru) + (((- 1) * b) * ru) = ((1 - b) * rv) + (- (a * rv)) by RVSUM_1:49;
then ((1 - a) + ((- 1) * b)) * ru = ((1 - b) * rv) + (- (a * rv)) by RVSUM_1:50;
then ((1 - a) - b) * ru = ((1 - b) * rv) + ((- 1) * (a * rv)) by RVSUM_1:54
.= ((1 - b) * rv) + (((- 1) * a) * rv) by RVSUM_1:49
.= ((1 - b) + ((- 1) * a)) * rv by RVSUM_1:50 ;
hence (1 - (a + b)) * u = (1 - (a + b)) * v ; :: thesis: verum