let A, B, C, A1, B1, C1 be Point of (TOP-REAL 2); :: thesis: for lambda, mu, nu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) & lambda <> 1 & mu <> 1 & nu <> 1 holds
( A1,B1,C1 is_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 )
let lambda, mu, nu be Real; :: thesis: ( A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) & lambda <> 1 & mu <> 1 & nu <> 1 implies ( A1,B1,C1 is_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 ) )
assume that
A: A,B,C is_a_triangle and
B: A1 = ((1 - lambda) * B) + (lambda * C) and
C: B1 = ((1 - mu) * C) + (mu * A) and
D: C1 = ((1 - nu) * A) + (nu * B) and
E: ( lambda <> 1 & mu <> 1 & nu <> 1 ) ; :: thesis: ( A1,B1,C1 is_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 )
F: the_area_of_polygon3 (A,B,C) <> 0 by Th9, A;
set q = ((1 - lambda) * (1 - mu)) * (1 - nu);
G: ( 1 - lambda <> 0 & 1 - mu <> 0 & 1 - nu <> 0 ) by E;
( A1,B1,C1 is_collinear iff the_area_of_polygon3 (A1,B1,C1) = 0 ) by Th9;
then ( A1,B1,C1 is_collinear iff ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C)) = 0 ) by Th10, B, C, D;
then ( A1,B1,C1 is_collinear iff (1 * (((1 - lambda) * (1 - mu)) * (1 - nu))) + ((lambda * mu) * nu) = 0 ) by F;
then ( A1,B1,C1 is_collinear iff (((1 - lambda) * (1 - mu)) * (1 - nu)) * (1 + (((lambda * mu) * nu) / (((1 - lambda) * (1 - mu)) * (1 - nu)))) = 0 ) by XCMPLX_1:235, G;
then ( A1,B1,C1 is_collinear iff 1 + (((lambda * mu) * nu) / (((1 - lambda) * (1 - mu)) * (1 - nu))) = 0 ) by G;
then ( A1,B1,C1 is_collinear iff - 1 = (lambda * (mu * nu)) / ((1 - lambda) * ((1 - mu) * (1 - nu))) ) ;
then ( A1,B1,C1 is_collinear iff - 1 = ((lambda / (1 - lambda)) * (mu * nu)) / ((1 - mu) * (1 - nu)) ) by XCMPLX_1:83;
then ( A1,B1,C1 is_collinear iff - 1 = (lambda / (1 - lambda)) * ((mu * nu) / ((1 - mu) * (1 - nu))) ) by XCMPLX_1:74;
then ( A1,B1,C1 is_collinear iff - 1 = (lambda / (1 - lambda)) * (((mu / (1 - mu)) * nu) / (1 - nu)) ) by XCMPLX_1:83;
then ( A1,B1,C1 is_collinear iff - 1 = (lambda / (1 - lambda)) * ((mu / (1 - mu)) * (nu / (1 - nu))) ) by XCMPLX_1:74;
hence ( A1,B1,C1 is_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 ) ; :: thesis: verum