let a, b, c be Element of TarskiEuclid2Space; :: thesis: ( ex jj being Real st
( 0 <= jj & jj <= 1 & (Tn2TR b) - (Tn2TR a) = jj * ((Tn2TR c) - (Tn2TR a)) ) implies Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c)) )
given jj being Real such that G2: ( 0 <= jj & jj <= 1 & (Tn2TR b) - (Tn2TR a) = jj * ((Tn2TR c) - (Tn2TR a)) ) ; :: thesis: Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c))
set v = Tn2TR a;
set w = Tn2TR c;
SS: (Tn2TR b) + ((Tn2TR a) - (Tn2TR a)) = (Tn2TR b) + (0. (TOP-REAL 2)) by RLVECT_1:5
.= Tn2TR b ;
G3: Tn2TR a = 1 * (Tn2TR a) by RVSUM_1:52;
(Tn2TR b) + ((- (Tn2TR a)) + (Tn2TR a)) = (jj * ((Tn2TR c) - (Tn2TR a))) + (Tn2TR a) by G2, RVSUM_1:15;
then Tn2TR b = ((jj * (Tn2TR c)) + (jj * (- (Tn2TR a)))) + (Tn2TR a) by RVSUM_1:51, SS
.= ((jj * (Tn2TR c)) + ((jj * (- 1)) * (Tn2TR a))) + (Tn2TR a) by RVSUM_1:49
.= ((jj * (Tn2TR c)) + ((- 1) * (jj * (Tn2TR a)))) + (Tn2TR a) by RVSUM_1:49
.= (jj * (Tn2TR c)) + ((- (jj * (Tn2TR a))) + (1 * (Tn2TR a))) by RVSUM_1:15, G3
.= (jj * (Tn2TR c)) + ((((- 1) * jj) * (Tn2TR a)) + (1 * (Tn2TR a))) by RVSUM_1:49
.= ((1 - jj) * (Tn2TR a)) + (jj * (Tn2TR c)) by RVSUM_1:50 ;
then Tn2TR b in { (((1 - r) * (Tn2TR a)) + (r * (Tn2TR c))) where r is Real : ( 0 <= r & r <= 1 ) } by G2;
hence Tn2TR b in LSeg ((Tn2TR a),(Tn2TR c)) by RLTOPSP1:def 2; :: thesis: verum