let T be RealLinearSpace; ( 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
; 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; ( 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
; 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 ( 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;
qp <> <*0*>thus
qp <> <*0*>
verum 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
; ex b, c being Real st
( x = <*r2*> & y = <*b*> & z = <*c*> & affine-ratio (x,y,z) = (b - r2) / (c - r2) )
take
r1
; ex c being Real st
( x = <*r2*> & y = <*r1*> & z = <*c*> & affine-ratio (x,y,z) = (r1 - r2) / (c - r2) )
take
r3
; ( 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; verum