let n be Element of NAT ; :: thesis: for x2, x1, x3, y2, y3 being Element of REAL n
for L1, L2 being Element of line_of_REAL n st x2 - x1,x3 - x1 are_lindependent2 & y2 in Line x1,x2 & y3 in Line x1,x3 & L1 = Line x2,x3 & L2 = Line y2,y3 holds
( L1 // L2 iff ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) )
let x2, x1, x3, y2, y3 be Element of REAL n; :: thesis: for L1, L2 being Element of line_of_REAL n st x2 - x1,x3 - x1 are_lindependent2 & y2 in Line x1,x2 & y3 in Line x1,x3 & L1 = Line x2,x3 & L2 = Line y2,y3 holds
( L1 // L2 iff ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( x2 - x1,x3 - x1 are_lindependent2 & y2 in Line x1,x2 & y3 in Line x1,x3 & L1 = Line x2,x3 & L2 = Line y2,y3 implies ( L1 // L2 iff ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) ) )
assume A1:
( x2 - x1,x3 - x1 are_lindependent2 & y2 in Line x1,x2 & y3 in Line x1,x3 & L1 = Line x2,x3 & L2 = Line y2,y3 )
; :: thesis: ( L1 // L2 iff ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) )
thus
( L1 // L2 implies ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) )
:: thesis: ( ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) implies L1 // L2 )proof
assume A2:
L1 // L2
;
:: thesis: ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) )
then
(
L1 is
being_line &
L2 is
being_line )
by Th71;
then A3:
(
x2 <> x3 &
y2 <> y3 )
by A1, Th81;
(
x2 in L1 &
x3 in L1 &
y2 in L2 &
y3 in L2 )
by A1, EUCLID_4:10;
then A4:
y3 - y2 // x3 - x2
by A2, A3, Th82;
then consider a being
Real such that A5:
y3 - y2 = a * (x3 - x2)
by Def1;
A6:
(
y3 - y2 <> 0* n &
x3 - x2 <> 0* n )
by A4, Def1;
consider s being
Real such that A7:
y2 = ((1 - s) * x1) + (s * x2)
by A1;
consider t being
Real such that A8:
y3 = ((1 - t) * x1) + (t * x3)
by A1;
0* n =
(y3 - y2) - (a * (x3 - x2))
by A5, Th14
.=
(((((1 - t) * x1) + (t * x3)) - ((1 - s) * x1)) - (s * x2)) - (a * (x3 - x2))
by A7, A8, RVSUM_1:60
.=
(((((1 * x1) + (- (t * x1))) + (t * x3)) - ((1 - s) * x1)) - (s * x2)) - (a * (x3 - x2))
by Th16
.=
(((((1 * x1) + (- (t * x1))) + (t * x3)) - ((1 * x1) + (- (s * x1)))) - (s * x2)) - (a * (x3 - x2))
by Th16
.=
((((((1 * x1) + (- (t * x1))) + (t * x3)) - (1 * x1)) - (- (s * x1))) - (s * x2)) - (a * (x3 - x2))
by RVSUM_1:60
.=
((((((1 * x1) + (- (t * x1))) + (- (1 * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))
by RVSUM_1:32
.=
((((((1 * x1) + (- (1 * x1))) + (- (t * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))
by RVSUM_1:32
.=
(((((0* n) + (- (t * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))
by Th7
.=
((((- (t * x1)) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))
by EUCLID_4:1
.=
(((t * (x3 - x1)) + (s * x1)) + (- (s * x2))) - (a * (x3 - x2))
by Th17
.=
(((t * (x3 - x1)) - (s * x2)) + (s * x1)) - (a * (x3 - x2))
by RVSUM_1:32
.=
((t * (x3 - x1)) - ((s * x2) - (s * x1))) - (a * (x3 - x2))
by Th9
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (x3 - x2))
by Th17
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - (0* n)) - x2))
by RVSUM_1:53
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - (x1 - x1)) - x2))
by Th7
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (((x3 - x1) + x1) + (- x2)))
by Th9
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - x1) + ((- x2) + x1)))
by RVSUM_1:32
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - ((a * (x3 - x1)) + (a * ((- x2) + x1)))
by EUCLID_4:6
.=
(((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (x3 - x1))) - (a * ((- x2) + x1))
by RVSUM_1:60
.=
((t * (x3 - x1)) - ((a * (x3 - x1)) + (s * (x2 - x1)))) - (a * ((- x2) + x1))
by RVSUM_1:60
.=
(((t * (x3 - x1)) - (a * (x3 - x1))) - (s * (x2 - x1))) - (a * ((- x2) + x1))
by RVSUM_1:60
.=
(((t - a) * (x3 - x1)) - (s * (x2 - x1))) - (a * ((- x2) + x1))
by Th16
.=
(((t - a) * (x3 - x1)) - (s * (x2 - x1))) - ((a * (- x2)) + (a * x1))
by EUCLID_4:6
.=
(((t - a) * (x3 - x1)) - (s * (x2 - x1))) - ((- (a * x2)) + (a * x1))
by Th8
.=
((((t - a) * (x3 - x1)) - (s * (x2 - x1))) - (- (a * x2))) - (a * x1)
by RVSUM_1:60
.=
(((t - a) * (x3 - x1)) - (s * (x2 - x1))) + ((a * x2) + (- (a * x1)))
by RVSUM_1:32
.=
(((t - a) * (x3 - x1)) - (s * (x2 - x1))) + (a * (x2 - x1))
by Th17
.=
((t - a) * (x3 - x1)) - ((s * (x2 - x1)) - (a * (x2 - x1)))
by Th9
.=
((t - a) * (x3 - x1)) + (- ((s - a) * (x2 - x1)))
by Th16
.=
((t - a) * (x3 - x1)) + ((- (s - a)) * (x2 - x1))
by Th8
.=
((t - a) * (x3 - x1)) + ((a - s) * (x2 - x1))
;
then A9:
(
t - a = 0 &
a - s = 0 )
by A1, Def2;
then A10:
y2 - x1 =
(((1 * x1) + (- (a * x1))) + (a * x2)) - x1
by A7, Th16
.=
((x1 + (- (a * x1))) + (a * x2)) - x1
by EUCLID_4:3
.=
(((- (a * x1)) + (a * x2)) + x1) - x1
by RVSUM_1:32
.=
((- (a * x1)) + (a * x2)) + (x1 - x1)
by Th10
.=
((- (a * x1)) + (a * x2)) + (0* n)
by Th7
.=
(- (a * x1)) + (a * x2)
by EUCLID_4:1
.=
a * (x2 - x1)
by Th17
;
A11:
y3 - x1 =
(((1 * x1) + (- (a * x1))) + (a * x3)) - x1
by A8, A9, Th16
.=
((x1 + (- (a * x1))) + (a * x3)) - x1
by EUCLID_4:3
.=
(((- (a * x1)) + (a * x3)) + x1) - x1
by RVSUM_1:32
.=
((- (a * x1)) + (a * x3)) + (x1 - x1)
by Th10
.=
((- (a * x1)) + (a * x3)) + (0* n)
by Th7
.=
(- (a * x1)) + (a * x3)
by EUCLID_4:1
.=
a * (x3 - x1)
by Th17
;
take
a
;
:: thesis: ( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) )
thus
(
a <> 0 &
y2 - x1 = a * (x2 - x1) &
y3 - x1 = a * (x3 - x1) )
by A5, A6, A10, A11, EUCLID_4:3;
:: thesis: verum
end;
now assume
ex
a being
Real st
(
a <> 0 &
y2 - x1 = a * (x2 - x1) &
y3 - x1 = a * (x3 - x1) )
;
:: thesis: ex a being Real ex x2, x3, y2, y3 being Element of REAL n st L1 // L2then consider a being
Real such that A12:
(
a <> 0 &
y2 - x1 = a * (x2 - x1) &
y3 - x1 = a * (x3 - x1) )
;
A13:
y3 - y2 =
(x1 + (a * (x3 - x1))) - y2
by A12, Th11
.=
((a * (x3 - x1)) + x1) - (x1 + (a * (x2 - x1)))
by A12, Th11
.=
(((a * (x3 - x1)) + x1) - x1) - (a * (x2 - x1))
by RVSUM_1:60
.=
((a * (x3 - x1)) + (x1 - x1)) - (a * (x2 - x1))
by Th10
.=
((a * (x3 - x1)) + (0* n)) - (a * (x2 - x1))
by Th7
.=
(a * (x3 - x1)) - (a * (x2 - x1))
by EUCLID_4:1
.=
((a * x3) + (- (a * x1))) - (a * (x2 - x1))
by Th17
.=
((a * x3) + (- (a * x1))) - ((- (a * x1)) + (a * x2))
by Th17
.=
(((a * x3) + (- (a * x1))) - (- (a * x1))) - (a * x2)
by RVSUM_1:60
.=
((a * x3) + ((- (a * x1)) - (- (a * x1)))) - (a * x2)
by Th10
.=
((a * x3) + (0* n)) - (a * x2)
by Th7
.=
(a * x3) - (a * x2)
by EUCLID_4:1
.=
a * (x3 - x2)
by Th17
;
x2 <> x3
by A1, Th42;
then A14:
x3 - x2 <> 0* n
by Th14;
then A15:
y3 - y2 <> 0* n
by A12, A13, EUCLID_4:5;
take a =
a;
:: thesis: ex x2, x3, y2, y3 being Element of REAL n st L1 // L2A16:
y3 - y2 // x3 - x2
by A13, A14, A15, Def1;
take x2 =
x2;
:: thesis: ex x3, y2, y3 being Element of REAL n st L1 // L2take x3 =
x3;
:: thesis: ex y2, y3 being Element of REAL n st L1 // L2take y2 =
y2;
:: thesis: ex y3 being Element of REAL n st L1 // L2take y3 =
y3;
:: thesis: L1 // L2thus
L1 // L2
by A1, A16, Def7;
:: thesis: verum end;
hence
( ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) implies L1 // L2 )
; :: thesis: verum