let T be RealLinearSpace; :: thesis: ( T = TOP-REAL 1 implies for x, y, z being Element of T st z <> x & y <> x holds
ex a, b, c being Real st
( x = <*a*> & y = <*b*> & z = <*c*> & affine-ratio (x,y,z) = (b - a) / (c - a) ) )
assume A1: T = TOP-REAL 1 ; :: thesis: for x, y, z being Element of T st z <> x & y <> x holds
ex a, b, c being Real st
( x = <*a*> & y = <*b*> & z = <*c*> & affine-ratio (x,y,z) = (b - a) / (c - a) )
let x, y, z be Element of T; :: thesis: ( z <> x & y <> x implies ex a, b, c being Real st
( x = <*a*> & y = <*b*> & z = <*c*> & affine-ratio (x,y,z) = (b - a) / (c - a) ) )
assume that
A2: z <> x and
A3: y <> x ; :: thesis: ex a, b, c being Real st
( x = <*a*> & y = <*b*> & z = <*c*> & affine-ratio (x,y,z) = (b - a) / (c - a) )
reconsider p9 = x, q9 = y, r9 = z as Element of REAL 1 by A1, EUCLID:22;
reconsider p = p9, q = q9, r = r9 as Tuple of 1, REAL ;
set ma = affine-ratio (x,y,z);
reconsider yx = y - x, zx = z - x as Element of T ;
( q9 - p9 is Element of 1 -tuples_on REAL & r9 - p9 is Element of 1 -tuples_on REAL ) ;
then reconsider qp = q - p, rp = r - p as Tuple of 1, REAL ;
A4: ( qp = yx & rp = zx ) by A1, Th18;
consider r1 being Element of REAL such that
A5: q = <*r1*> by FINSEQ_2:97;
consider r2 being Element of REAL such that
A6: p = <*r2*> by FINSEQ_2:97;
consider r3 being Element of REAL such that
A7: r = <*r3*> by FINSEQ_2:97;
A8: ( qp = <*(r1 - r2)*> & rp = <*(r3 - r2)*> ) by A5, A6, A7, RVSUM_1:29;
now :: thesis: ( qp = (affine-ratio (x,y,z)) * rp & qp <> <*0*> )
x,y,z are_collinear by A1, Th25;
then y - x = (affine-ratio (x,y,z)) * (z - x) by A2, Def02;
hence qp = (affine-ratio (x,y,z)) * rp by A4, A1, Th23; :: thesis: qp <> <*0*>
thus qp <> <*0*> :: thesis: verum
proof
assume qp = <*0*> ; :: thesis: contradiction
then r1 - r2 = 0 by A8, FINSEQ_1:76;
hence contradiction by A5, A6, A3; :: thesis: verum
end;
end;
then consider a, b being Real such that
A9: qp = <*a*> and
A10: rp = <*b*> and
A11: affine-ratio (x,y,z) = a / b by Th24;
reconsider s1 = r1 - r2, s2 = r3 - r2 as Real ;
A12: ( a = s1 & b = s2 ) by A9, A10, A8, FINSEQ_1:76;
reconsider r2 = r2, r1 = r1, r3 = r3 as Real ;
take r2 ; :: thesis: ex b, c being Real st
( x = <*r2*> & y = <*b*> & z = <*c*> & affine-ratio (x,y,z) = (b - r2) / (c - r2) )
take r1 ; :: thesis: ex c being Real st
( x = <*r2*> & y = <*r1*> & z = <*c*> & affine-ratio (x,y,z) = (r1 - r2) / (c - r2) )
take r3 ; :: thesis: ( x = <*r2*> & y = <*r1*> & z = <*r3*> & affine-ratio (x,y,z) = (r1 - r2) / (r3 - r2) )
thus ( x = <*r2*> & y = <*r1*> & z = <*r3*> & affine-ratio (x,y,z) = (r1 - r2) / (r3 - r2) ) by A11, A12, A5, A6, A7; :: thesis: verum