let n be Nat; :: thesis: for lambda, mu being Real
for x1, x2 being Element of REAL n
for An, Bn being Point of (TOP-REAL n) st An = ((1 - lambda) * x1) + (lambda * x2) & Bn = ((1 - mu) * x1) + (mu * x2) holds
Bn - An = (mu - lambda) * (x2 - x1)
let lambda, mu be Real; :: thesis: for x1, x2 being Element of REAL n
for An, Bn being Point of (TOP-REAL n) st An = ((1 - lambda) * x1) + (lambda * x2) & Bn = ((1 - mu) * x1) + (mu * x2) holds
Bn - An = (mu - lambda) * (x2 - x1)
let x1, x2 be Element of REAL n; :: thesis: for An, Bn being Point of (TOP-REAL n) st An = ((1 - lambda) * x1) + (lambda * x2) & Bn = ((1 - mu) * x1) + (mu * x2) holds
Bn - An = (mu - lambda) * (x2 - x1)
let An, Bn be Point of (TOP-REAL n); :: thesis: ( An = ((1 - lambda) * x1) + (lambda * x2) & Bn = ((1 - mu) * x1) + (mu * x2) implies Bn - An = (mu - lambda) * (x2 - x1) )
assume that
A1: An = ((1 - lambda) * x1) + (lambda * x2) and
A2: Bn = ((1 - mu) * x1) + (mu * x2) ; :: thesis: Bn - An = (mu - lambda) * (x2 - x1)
A3: (1 - lambda) * x1 = x1 - (lambda * x1) by Lm1;
Bn - An = ((((1 - mu) * x1) + (mu * x2)) - ((1 - lambda) * x1)) - (lambda * x2) by A1, A2, RVSUM_1:39
.= (((x1 - (mu * x1)) + (mu * x2)) - (x1 - (lambda * x1))) - (lambda * x2) by A3, Lm1
.= ((((x1 - (mu * x1)) + (mu * x2)) - x1) + (lambda * x1)) - (lambda * x2) by RVSUM_1:41
.= (((x1 - ((mu * x1) - (mu * x2))) + (- x1)) + (lambda * x1)) - (lambda * x2) by RVSUM_1:41
.= ((((- ((mu * x1) - (mu * x2))) + x1) - x1) + (lambda * x1)) - (lambda * x2)
.= ((- ((mu * x1) - (mu * x2))) + (lambda * x1)) - (lambda * x2) by RVSUM_1:42
.= (((mu * x2) - (mu * x1)) + (lambda * x1)) - (lambda * x2) by RVSUM_1:35
.= ((mu * x2) + ((- (mu * x1)) + (lambda * x1))) + (- (lambda * x2)) by RVSUM_1:15
.= ((mu * x2) + ((((- 1) * mu) * x1) + (lambda * x1))) + (- (lambda * x2)) by RVSUM_1:49
.= ((mu * x2) + (((- mu) + lambda) * x1)) + (- (lambda * x2)) by RVSUM_1:50
.= (((- mu) + lambda) * x1) + ((mu * x2) + (- (lambda * x2))) by RVSUM_1:15
.= ((- (mu - lambda)) * x1) + ((mu - lambda) * x2) by EUCLIDLP:11
.= (mu - lambda) * (x2 - x1) by EUCLIDLP:12 ;
hence Bn - An = (mu - lambda) * (x2 - x1) ; :: thesis: verum