let A, B, C be Point of (TOP-REAL 2); :: thesis: for L1, L2 being Element of line_of_REAL 2
for D being Point of (TOP-REAL 2) st L1 _|_ L2 & L1 = Line (A,B) & L2 = Line (C,D) holds
|((B - A),(D - C))| = 0
let L1, L2 be Element of line_of_REAL 2; :: thesis: for D being Point of (TOP-REAL 2) st L1 _|_ L2 & L1 = Line (A,B) & L2 = Line (C,D) holds
|((B - A),(D - C))| = 0
let D be Point of (TOP-REAL 2); :: thesis: ( L1 _|_ L2 & L1 = Line (A,B) & L2 = Line (C,D) implies |((B - A),(D - C))| = 0 )
assume that
A1: L1 _|_ L2 and
A2: L1 = Line (A,B) and
A3: L2 = Line (C,D) ; :: thesis: |((B - A),(D - C))| = 0
consider x1, x2, y1, y2 being Element of REAL 2 such that
A4: L1 = Line (x1,x2) and
A5: L2 = Line (y1,y2) and
A6: x2 - x1 _|_ y2 - y1 by A1, EUCLIDLP:def 8;
A7: |((x2 - x1),(y2 - y1))| = 0 by A6, EUCLIDLP:def 3, RVSUM_1:def 17;
A8: ( A in Line (x1,x2) & B in Line (x1,x2) ) by A2, A4, EUCLID_4:41;
then consider lambda being Real such that
A9: A = ((1 - lambda) * x1) + (lambda * x2) ;
consider mu being Real such that
A10: B = ((1 - mu) * x1) + (mu * x2) by A8;
A11: ( C in Line (y1,y2) & D in Line (y1,y2) ) by A3, A5, EUCLID_4:41;
then consider lambda2 being Real such that
A12: C = ((1 - lambda2) * y1) + (lambda2 * y2) ;
consider mu2 being Real such that
A13: D = ((1 - mu2) * y1) + (mu2 * y2) by A11;
A14: B - A = (mu - lambda) * (x2 - x1) by A9, A10, Th1;
reconsider a = mu - lambda, b = mu2 - lambda2 as Real ;
|((B - A),(D - C))| = |((a * (x2 - x1)),(b * (y2 - y1)))| by A14, A12, A13, Th1
.= a * |((x2 - x1),(b * (y2 - y1)))| by EUCLID_4:21
.= a * (b * |((x2 - x1),(y2 - y1))|) by EUCLID_4:22
.= 0 by A7 ;
hence |((B - A),(D - C))| = 0 ; :: thesis: verum