let n be Nat; for L, L1, L2 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 holds
L1 // L2
let L, L1, L2 be Element of line_of_REAL n; for P being Element of plane_of_REAL n st L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 holds
L1 // L2
let P be Element of plane_of_REAL n; ( L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 implies L1 // L2 )
assume that
A1:
L c= P
and
A2:
L1 c= P
and
A3:
L2 c= P
; ( not L _|_ L1 or not L _|_ L2 or L1 // L2 )
assume that
A4:
L _|_ L1
and
A5:
L _|_ L2
; L1 // L2
L,L2 are_coplane
by A1, A3, Th96;
then
L meets L2
by A5, Th109;
then consider x2 being Element of REAL n such that
A6:
x2 in L
and
A7:
x2 in L2
by Th49;
A8:
L1 is being_line
by A4, Th67;
L,L1 are_coplane
by A1, A2, Th96;
then
L meets L1
by A4, Th109;
then consider x1 being Element of REAL n such that
A9:
x1 in L
and
A10:
x1 in L1
by Th49;
A11:
L2 is being_line
by A5, Th67;
now ( ( x1 = x2 & L1 // L2 ) or ( x1 <> x2 & L1 // L2 ) )per cases
( x1 = x2 or x1 <> x2 )
;
case
x1 = x2
;
L1 // L2hence
L1 // L2
by A1, A2, A3, A4, A5, A9, A10, A7, A8, Th65, Th108;
verum end; case A12:
x1 <> x2
;
L1 // L2then
x1 - x2 <> 0* n
by Th9;
then A13:
|((x1 - x2),(x1 - x2))| <> 0
by EUCLID_4:17;
consider x being
Element of
REAL n such that A14:
x <> x2
and A15:
x in L2
by A11, Th53;
A16:
L2 = Line (
x2,
x)
by A7, A14, A15, Th64;
consider x0 being
Element of
REAL n such that A17:
x0 <> x1
and A18:
x0 in L1
by A8, Th53;
A19:
L1 = Line (
x0,
x1)
by A10, A17, A18, Th64;
A20:
x0 - x1 _|_ x2 - x1
by A4, A9, A10, A6, A12, A17, A18, Th74;
then
x0 - x1,
x2 - x1 are_orthogonal
;
then A21:
|((x0 - x1),(x2 - x1))| = 0
by RVSUM_1:def 17;
P = plane (
x1,
x0,
x2)
by A1, A2, A9, A6, A18, A20, Th45, Th92;
then consider a1,
a3,
a2 being
Real such that A22:
(a1 + a3) + a2 = 1
and A23:
x = ((a1 * x1) + (a3 * x0)) + (a2 * x2)
by A3, A15, Th88;
A24:
(a2 + a1) + a3 = 1
by A22;
A25:
x - x2 =
(- x2) + (((a2 * x2) + (a1 * x1)) + (a3 * x0))
by A23, RVSUM_1:15
.=
(- x2) + ((x2 + (a1 * (x1 - x2))) + (a3 * (x0 - x2)))
by A24, Th27
.=
(- x2) + (x2 + ((a1 * (x1 - x2)) + (a3 * (x0 - x2))))
by RVSUM_1:15
.=
((- x2) + x2) + ((a1 * (x1 - x2)) + (a3 * (x0 - x2)))
by RVSUM_1:15
.=
(0* n) + ((a1 * (x1 - x2)) + (a3 * (x0 - x2)))
by Th2
.=
(a1 * (x1 - x2)) + (a3 * (x0 - x2))
by EUCLID_4:1
;
A26:
|((x0 - x1),(x1 - x2))| =
|((x0 - x1),(((- 1) * x2) + (- (- x1))))|
.=
|((x0 - x1),((- 1) * (x2 + (- x1))))|
by EUCLID_4:6
.=
(- 1) * |((x0 - x1),(x2 - x1))|
by EUCLID_4:22
.=
0
by A21
;
A27:
x0 - x2 =
x0 - ((0* n) + x2)
by EUCLID_4:1
.=
x0 - ((x1 - x1) + x2)
by Th2
.=
(x0 - (x1 - x1)) - x2
by RVSUM_1:39
.=
((x0 - x1) + x1) - x2
by Th4
.=
(x0 - x1) + (x1 - x2)
by Th5
;
x - x2 _|_ x1 - x2
by A5, A9, A6, A7, A12, A14, A15, Th74;
then
x - x2,
x1 - x2 are_orthogonal
;
then 0 =
|(((a1 * (x1 - x2)) + (a3 * (x0 - x2))),(x1 - x2))|
by A25, RVSUM_1:def 17
.=
|((a1 * (x1 - x2)),(x1 - x2))| + |((a3 * (x0 - x2)),(x1 - x2))|
by EUCLID_4:20
.=
(a1 * |((x1 - x2),(x1 - x2))|) + |((a3 * (x0 - x2)),(x1 - x2))|
by EUCLID_4:21
.=
(a1 * |((x1 - x2),(x1 - x2))|) + (a3 * |((x0 - x2),(x1 - x2))|)
by EUCLID_4:21
.=
(a1 * |((x1 - x2),(x1 - x2))|) + (a3 * (|((x0 - x1),(x1 - x2))| + |((x1 - x2),(x1 - x2))|))
by A27, EUCLID_4:20
.=
(a1 + a3) * |((x1 - x2),(x1 - x2))|
by A26
;
then
a1 + a3 = 0
by A13, XCMPLX_1:6;
then
a3 = - a1
;
then A28:
x - x2 =
a1 * ((x1 + (- x2)) - (x0 - x2))
by A25, Th12
.=
a1 * ((x1 - x0) + ((- x2) - (- x2)))
by Th18
.=
a1 * ((x1 - x0) + (0* n))
by Th2
.=
a1 * (x1 - x0)
by EUCLID_4:1
;
A29:
x1 - x0 <> 0* n
by A17, Th9;
x - x2 <> 0* n
by A14, Th9;
then
x - x2 // x1 - x0
by A28, A29;
hence
L1 // L2
by A19, A16;
verum end;
hence
L1 // L2
; verum