let n be Nat; for L, L0, L1, L2 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 holds
L meets L2
let L, L0, L1, L2 be Element of line_of_REAL n; for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 holds
L meets L2
let P be Element of plane_of_REAL n; ( L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 implies L meets L2 )
assume that
A1:
( L0 c= P & L1 c= P )
and
A2:
L2 c= P
and
A3:
L0 // L1
and
A4:
L1 // L2
and
A5:
L0 <> L1
; ( not L meets L0 or not L meets L1 or L meets L2 )
A6:
L1 is being_line
by A3, Th66;
assume that
A7:
L meets L0
and
A8:
L meets L1
; L meets L2
consider x0 being Element of REAL n such that
A9:
x0 in L
and
A10:
x0 in L0
by A7, Th49;
A11:
L0 misses L1
by A3, A5, Th71;
then
not x0 in L1
by A10, Th49;
then consider L9 being Element of line_of_REAL n such that
A12:
x0 in L9
and
A13:
L9 _|_ L1
and
A14:
L9 meets L1
by A6, Th62;
consider y1 being Element of REAL n such that
A15:
y1 in L9
and
A16:
y1 in L1
by A14, Th49;
A17:
x0 <> y1
by A10, A11, A16, Th49;
then A18:
L9 = Line (x0,y1)
by A12, A15, Th64;
then
L9 c= P
by A1, A10, A16, Th95;
then
L9,L2 are_coplane
by A2, Th96;
then A19:
L9 meets L2
by A4, A13, Th61, Th109;
then consider y2 being Element of REAL n such that
A20:
y2 in L9
and
A21:
y2 in L2
by Th49;
consider a being Real such that
A22:
y2 - x0 = a * (y1 - x0)
by A12, A15, A17, A20, Th70;
L2 is being_line
by A4, Th66;
then consider x2 being Element of REAL n such that
A23:
( x2 <> y2 & x2 in L2 )
by Th53;
consider x1 being Element of REAL n such that
A24:
x1 in L
and
A25:
x1 in L1
by A8, Th49;
x0 <> x1
by A10, A25, A11, Th49;
then A26:
L = Line (x0,x1)
by A9, A24, Th64;
A27:
L2 = Line (y2,x2)
by A21, A23, Th64;
now ( ( x1 = y1 & L meets L2 ) or ( x1 <> y1 & L meets L2 ) )per cases
( x1 = y1 or x1 <> y1 )
;
case A28:
x1 <> y1
;
L meets L2set x =
((1 - a) * x0) + (a * x1);
consider b being
Real such that A29:
b <> 0
and A30:
x2 - y2 = b * (x1 - y1)
by A4, A25, A16, A21, A23, A28, Th32, Th77;
A31:
x1 - y1 =
1
* (x1 - y1)
by EUCLID_4:3
.=
((1 / b) * b) * (x1 - y1)
by A29, XCMPLX_1:87
.=
(1 / b) * (x2 - y2)
by A30, EUCLID_4:4
;
((1 - a) * x0) + (a * x1) =
((1 * x0) + (- (a * x0))) + (a * x1)
by Th11
.=
(x0 + (- (a * x0))) + (a * x1)
by EUCLID_4:3
.=
((a * x1) + (- (a * x0))) + x0
by RVSUM_1:15
.=
(a * (x1 - x0)) + x0
by Th12
.=
(a * ((x1 + (0* n)) + (- x0))) + x0
by EUCLID_4:1
.=
(a * ((x1 + ((- y1) + y1)) + (- x0))) + x0
by Th2
.=
(a * (((x1 + (- y1)) + y1) + (- x0))) + x0
by RVSUM_1:15
.=
(a * ((x1 - y1) + (y1 + (- x0)))) + x0
by RVSUM_1:15
.=
((a * ((1 / b) * (x2 - y2))) + (a * (y1 - x0))) + x0
by A31, EUCLID_4:6
.=
(((a * (1 / b)) * (x2 - y2)) + (a * (y1 - x0))) + x0
by EUCLID_4:4
.=
(((a / b) * (x2 - y2)) + (a * (y1 - x0))) + x0
by XCMPLX_1:99
.=
((a / b) * (x2 - y2)) + ((y2 + (- x0)) + x0)
by A22, RVSUM_1:15
.=
((a / b) * (x2 - y2)) + (y2 + ((- x0) + x0))
by RVSUM_1:15
.=
((a / b) * (x2 - y2)) + (y2 + (0* n))
by Th2
.=
((a / b) * (x2 - y2)) + y2
by EUCLID_4:1
.=
(((a / b) * x2) + (- ((a / b) * y2))) + y2
by Th12
.=
(y2 + (- ((a / b) * y2))) + ((a / b) * x2)
by RVSUM_1:15
.=
((1 * y2) + (- ((a / b) * y2))) + ((a / b) * x2)
by EUCLID_4:3
.=
((1 - (a / b)) * y2) + ((a / b) * x2)
by Th11
;
then A32:
((1 - a) * x0) + (a * x1) in L2
by A27;
((1 - a) * x0) + (a * x1) in L
by A26;
hence
L meets L2
by A32, Th49;
verum end; end; end;
hence
L meets L2
; verum