let n be Nat; for x1, x2, 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 x1, x2, x3, y2, y3 be 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 L1, L2 be Element of line_of_REAL n; ( 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 that
A1:
x2 - x1,x3 - x1 are_lindependent2
and
A2:
y2 in Line (x1,x2)
and
A3:
y3 in Line (x1,x3)
and
A4:
L1 = Line (x2,x3)
and
A5:
L2 = Line (y2,y3)
; ( 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) ) )
( ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) implies L1 // L2 )proof
assume A6:
L1 // L2
;
ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) )
then
L1 is
being_line
by Th66;
then A7:
x2 <> x3
by A4, Th76;
L2 is
being_line
by A6, Th66;
then A8:
y2 <> y3
by A5, Th76;
A9:
(
y2 in L2 &
y3 in L2 )
by A5, EUCLID_4:9;
consider t being
Real such that A10:
y3 = ((1 - t) * x1) + (t * x3)
by A3;
(
x2 in L1 &
x3 in L1 )
by A4, EUCLID_4:9;
then A11:
y3 - y2 // x3 - x2
by A6, A7, A8, A9, Th77;
then consider a being
Real such that A12:
y3 - y2 = a * (x3 - x2)
;
take
a
;
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) )
consider s being
Real such that A13:
y2 = ((1 - s) * x1) + (s * x2)
by A2;
A14:
0* n =
(y3 - y2) - (a * (x3 - x2))
by A12, Th9
.=
(((((1 - t) * x1) + (t * x3)) - ((1 - s) * x1)) - (s * x2)) - (a * (x3 - x2))
by A13, A10, RVSUM_1:39
.=
(((((1 * x1) + (- (t * x1))) + (t * x3)) - ((1 - s) * x1)) - (s * x2)) - (a * (x3 - x2))
by Th11
.=
(((((1 * x1) + (- (t * x1))) + (t * x3)) - ((1 * x1) + (- (s * x1)))) - (s * x2)) - (a * (x3 - x2))
by Th11
.=
((((((1 * x1) + (- (t * x1))) + (t * x3)) - (1 * x1)) - (- (s * x1))) - (s * x2)) - (a * (x3 - x2))
by RVSUM_1:39
.=
((((((1 * x1) + (- (t * x1))) + (- (1 * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))
by RVSUM_1:15
.=
((((((1 * x1) + (- (1 * x1))) + (- (t * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))
by RVSUM_1:15
.=
(((((0* n) + (- (t * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))
by Th2
.=
((((- (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 Th12
.=
(((t * (x3 - x1)) - (s * x2)) + (s * x1)) - (a * (x3 - x2))
by RVSUM_1:15
.=
((t * (x3 - x1)) - ((s * x2) - (s * x1))) - (a * (x3 - x2))
by Th4
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (x3 - x2))
by Th12
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - (0* n)) - x2))
by RVSUM_1:32
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - (x1 - x1)) - x2))
by Th2
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (((x3 - x1) + x1) + (- x2)))
by Th4
.=
((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - x1) + ((- x2) + x1)))
by RVSUM_1:15
.=
((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:39
.=
((t * (x3 - x1)) - ((a * (x3 - x1)) + (s * (x2 - x1)))) - (a * ((- x2) + x1))
by RVSUM_1:39
.=
(((t * (x3 - x1)) - (a * (x3 - x1))) - (s * (x2 - x1))) - (a * ((- x2) + x1))
by RVSUM_1:39
.=
(((t - a) * (x3 - x1)) - (s * (x2 - x1))) - (a * ((- x2) + x1))
by Th11
.=
(((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 Th3
.=
((((t - a) * (x3 - x1)) - (s * (x2 - x1))) - (- (a * x2))) - (a * x1)
by RVSUM_1:39
.=
(((t - a) * (x3 - x1)) - (s * (x2 - x1))) + ((a * x2) + (- (a * x1)))
by RVSUM_1:15
.=
(((t - a) * (x3 - x1)) - (s * (x2 - x1))) + (a * (x2 - x1))
by Th12
.=
((t - a) * (x3 - x1)) - ((s * (x2 - x1)) - (a * (x2 - x1)))
by Th4
.=
((t - a) * (x3 - x1)) + (- ((s - a) * (x2 - x1)))
by Th11
.=
((t - a) * (x3 - x1)) + ((- (s - a)) * (x2 - x1))
by Th3
.=
((t - a) * (x3 - x1)) + ((a - s) * (x2 - x1))
;
then
t - a = 0
by A1;
then A15:
y3 - x1 =
(((1 * x1) + (- (a * x1))) + (a * x3)) - x1
by A10, Th11
.=
((x1 + (- (a * x1))) + (a * x3)) - x1
by EUCLID_4:3
.=
(((- (a * x1)) + (a * x3)) + x1) - x1
by RVSUM_1:15
.=
((- (a * x1)) + (a * x3)) + (x1 - x1)
by Th5
.=
((- (a * x1)) + (a * x3)) + (0* n)
by Th2
.=
(- (a * x1)) + (a * x3)
by EUCLID_4:1
.=
a * (x3 - x1)
by Th12
;
a - s = 0
by A1, A14;
then A16:
y2 - x1 =
(((1 * x1) + (- (a * x1))) + (a * x2)) - x1
by A13, Th11
.=
((x1 + (- (a * x1))) + (a * x2)) - x1
by EUCLID_4:3
.=
(((- (a * x1)) + (a * x2)) + x1) - x1
by RVSUM_1:15
.=
((- (a * x1)) + (a * x2)) + (x1 - x1)
by Th5
.=
((- (a * x1)) + (a * x2)) + (0* n)
by Th2
.=
(- (a * x1)) + (a * x2)
by EUCLID_4:1
.=
a * (x2 - x1)
by Th12
;
y3 - y2 <> 0* n
by A11;
hence
(
a <> 0 &
y2 - x1 = a * (x2 - x1) &
y3 - x1 = a * (x3 - x1) )
by A12, A16, A15, EUCLID_4:3;
verum
end;
now ( ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) implies ex a being Real ex x2, x3, y2, y3 being Element of REAL n st L1 // L2 )assume
ex
a being
Real st
(
a <> 0 &
y2 - x1 = a * (x2 - x1) &
y3 - x1 = a * (x3 - x1) )
;
ex a being Real ex x2, x3, y2, y3 being Element of REAL n st L1 // L2then consider a being
Real such that A17:
a <> 0
and A18:
y2 - x1 = a * (x2 - x1)
and A19:
y3 - x1 = a * (x3 - x1)
;
take a =
a;
ex x2, x3, y2, y3 being Element of REAL n st L1 // L2take x2 =
x2;
ex x3, y2, y3 being Element of REAL n st L1 // L2take x3 =
x3;
ex y2, y3 being Element of REAL n st L1 // L2take y2 =
y2;
ex y3 being Element of REAL n st L1 // L2take y3 =
y3;
L1 // L2
x2 <> x3
by A1, Th37;
then A20:
x3 - x2 <> 0* n
by Th9;
A21:
y3 - y2 =
(x1 + (a * (x3 - x1))) - y2
by A19, Th6
.=
((a * (x3 - x1)) + x1) - (x1 + (a * (x2 - x1)))
by A18, Th6
.=
(((a * (x3 - x1)) + x1) - x1) - (a * (x2 - x1))
by RVSUM_1:39
.=
((a * (x3 - x1)) + (x1 - x1)) - (a * (x2 - x1))
by Th5
.=
((a * (x3 - x1)) + (0* n)) - (a * (x2 - x1))
by Th2
.=
(a * (x3 - x1)) - (a * (x2 - x1))
by EUCLID_4:1
.=
((a * x3) + (- (a * x1))) - (a * (x2 - x1))
by Th12
.=
((a * x3) + (- (a * x1))) - ((- (a * x1)) + (a * x2))
by Th12
.=
(((a * x3) + (- (a * x1))) - (- (a * x1))) - (a * x2)
by RVSUM_1:39
.=
((a * x3) + ((- (a * x1)) - (- (a * x1)))) - (a * x2)
by Th5
.=
((a * x3) + (0* n)) - (a * x2)
by Th2
.=
(a * x3) - (a * x2)
by EUCLID_4:1
.=
a * (x3 - x2)
by Th12
;
then
y3 - y2 <> 0* n
by A17, A20, EUCLID_4:5;
then
y3 - y2 // x3 - x2
by A21, A20;
hence
L1 // L2
by A4, A5;
verum end;
hence
( ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) implies L1 // L2 )
; verum