let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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 :: thesis: ( ( x1 = y1 & L meets L2 ) or ( x1 <> y1 & L meets L2 ) )
per cases ( x1 = y1 or x1 <> y1 ) ;
case x1 = y1 ; :: thesis: L meets L2
hence L meets L2 by A9, A24, A17, A18, A19, Th64; :: thesis: verum
end;
case A28: x1 <> y1 ; :: thesis: L meets L2
set 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; :: thesis: verum
end;
end;
end;
hence L meets L2 ; :: thesis: verum