let P, Q be Element of BK_model ; :: thesis: ( P <> Q implies ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear ) )
assume A1: P <> Q ; :: thesis: ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear )
consider u being non zero Element of (TOP-REAL 3) such that
A2: ( Dir u = P & u . 3 = 1 & BK_to_REAL2 P = |[(u . 1),(u . 2)]| ) by Def01;
consider v being non zero Element of (TOP-REAL 3) such that
A3: ( Dir v = Q & v . 3 = 1 & BK_to_REAL2 Q = |[(v . 1),(v . 2)]| ) by Def01;
reconsider s = |[(u . 1),(u . 2)]|, t = |[(v . 1),(v . 2)]| as Point of (TOP-REAL 2) ;
set a = 0 ;
set b = 0 ;
set r = 1;
reconsider S = s, T = t, X = |[0,0]| as Element of REAL 2 by EUCLID:22;
reconsider w1 = ((- (2 * |((t - s),(s - |[0,0]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[0,0]|))|),((Sum (sqr (S - X))) - (1 ^2)))))) / (2 * (Sum (sqr (T - S)))) as Real ;
consider e1 being Point of (TOP-REAL 2) such that
A4: ( {e1} = (halfline (s,t)) /\ (circle (0,0,1)) & e1 = ((1 - w1) * s) + (w1 * t) ) by Th02, A1, A2, A3, TOPREAL9:58;
reconsider w2 = ((- (2 * |((s - t),(t - |[0,0]|))|)) + (sqrt (delta ((Sum (sqr (S - T))),(2 * |((s - t),(t - |[0,0]|))|),((Sum (sqr (T - X))) - (1 ^2)))))) / (2 * (Sum (sqr (S - T)))) as Real ;
consider e2 being Point of (TOP-REAL 2) such that
A5: ( {e2} = (halfline (t,s)) /\ (circle (0,0,1)) & e2 = ((1 - w2) * t) + (w2 * s) ) by Th02, A1, A2, A3, TOPREAL9:58;
reconsider f = |[(e1 `1),(e1 `2),1]| as Element of (TOP-REAL 3) ;
not f is zero by FINSEQ_1:78, EUCLID_5:4;
then reconsider ee1 = f as non zero Element of (TOP-REAL 3) ;
A6: ( s . 1 = u . 1 & s . 2 = u . 2 & t . 1 = v . 1 & t . 2 = v . 2 ) ;
reconsider P1 = Dir ee1 as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
((1 * ee1) + ((- (1 - w1)) * u)) + ((- w1) * v) = 0. (TOP-REAL 3)
proof
A7: 1 * ee1 = |[(1 * (ee1 `1)),(1 * (ee1 `2)),(1 * (ee1 `3))]| by EUCLID_5:7
.= ee1 by EUCLID_5:3 ;
ee1 = ((1 - w1) * u) + (w1 * v)
proof
A8: ((1 - w1) * s) + (w1 * t) = |[((((1 - w1) * s) + (w1 * t)) `1),((((1 - w1) * s) + (w1 * t)) `2)]| by EUCLID:53;
((1 - w1) * s) + (w1 * t) = |[((((1 - w1) * s) `1) + ((w1 * t) `1)),((((1 - w1) * s) `2) + ((w1 * t) `2))]| by EUCLID:55
.= |[((((1 - w1) * s) . 1) + ((w1 * t) `1)),((((1 - w1) * s) `2) + ((w1 * t) `2))]| by EUCLID:def 9
.= |[((((1 - w1) * s) . 1) + ((w1 * t) . 1)),((((1 - w1) * s) `2) + ((w1 * t) `2))]| by EUCLID:def 9
.= |[((((1 - w1) * s) . 1) + ((w1 * t) . 1)),((((1 - w1) * s) . 2) + ((w1 * t) `2))]| by EUCLID:def 10
.= |[((((1 - w1) * s) . 1) + ((w1 * t) . 1)),((((1 - w1) * s) . 2) + ((w1 * t) . 2))]| by EUCLID:def 10
.= |[(((1 - w1) * (s . 1)) + ((w1 * t) . 1)),((((1 - w1) * s) . 2) + ((w1 * t) . 2))]| by RVSUM_1:44
.= |[(((1 - w1) * (s . 1)) + (w1 * (t . 1))),((((1 - w1) * s) . 2) + ((w1 * t) . 2))]| by RVSUM_1:44
.= |[(((1 - w1) * (s . 1)) + (w1 * (t . 1))),(((1 - w1) * (s . 2)) + ((w1 * t) . 2))]| by RVSUM_1:44
.= |[(((1 - w1) * (u . 1)) + (w1 * (v . 1))),(((1 - w1) * (u . 2)) + (w1 * (v . 2)))]| by A6, RVSUM_1:44 ;
then A9: ( e1 `1 = ((1 - w1) * (u . 1)) + (w1 * (v . 1)) & e1 `2 = ((1 - w1) * (u . 2)) + (w1 * (v . 2)) ) by A4, A8, FINSEQ_1:77;
((1 - w1) * u) + (w1 * v) = |[(((1 - w1) * (u . 1)) + (w1 * (v . 1))),(((1 - w1) * (u . 2)) + (w1 * (v . 2))),(((1 - w1) * (u . 3)) + (w1 * (v . 3)))]|
proof
((1 - w1) * u) `1 = (1 - w1) * (u `1) by EUCLID_5:9
.= (1 - w1) * (u . 1) by EUCLID_5:def 1 ;
then A10: (((1 - w1) * u) `1) + ((w1 * v) `1) = ((1 - w1) * (u . 1)) + ((w1 * v) . 1) by EUCLID_5:def 1
.= ((1 - w1) * (u . 1)) + (w1 * (v . 1)) by RVSUM_1:44 ;
((1 - w1) * u) `2 = (1 - w1) * (u `2) by EUCLID_5:9
.= (1 - w1) * (u . 2) by EUCLID_5:def 2 ;
then A11: (((1 - w1) * u) `2) + ((w1 * v) `2) = ((1 - w1) * (u . 2)) + ((w1 * v) . 2) by EUCLID_5:def 2
.= ((1 - w1) * (u . 2)) + (w1 * (v . 2)) by RVSUM_1:44 ;
((1 - w1) * u) `3 = (1 - w1) * (u `3) by EUCLID_5:9
.= (1 - w1) * (u . 3) by EUCLID_5:def 3 ;
then (((1 - w1) * u) `3) + ((w1 * v) `3) = ((1 - w1) * (u . 3)) + ((w1 * v) . 3) by EUCLID_5:def 3
.= ((1 - w1) * (u . 3)) + (w1 * (v . 3)) by RVSUM_1:44 ;
hence ((1 - w1) * u) + (w1 * v) = |[(((1 - w1) * (u . 1)) + (w1 * (v . 1))),(((1 - w1) * (u . 2)) + (w1 * (v . 2))),(((1 - w1) * (u . 3)) + (w1 * (v . 3)))]| by A10, A11, EUCLID_5:5; :: thesis: verum
end;
hence ee1 = ((1 - w1) * u) + (w1 * v) by A9, A2, A3; :: thesis: verum
end;
then (ee1 + ((- (1 - w1)) * u)) + ((- w1) * v) = (((1 - w1) * u) + (w1 * v)) + (((- (1 - w1)) * u) + ((- w1) * v)) by RVSUM_1:15
.= ((1 - w1) * u) + ((w1 * v) + (((- (1 - w1)) * u) + ((- w1) * v))) by RVSUM_1:15
.= ((1 - w1) * u) + (((- (1 - w1)) * u) + ((w1 * v) + ((- w1) * v))) by RVSUM_1:15
.= (((1 - w1) * u) + ((- (1 - w1)) * u)) + ((w1 * v) + ((- w1) * v)) by RVSUM_1:15
.= (0. (TOP-REAL 3)) + ((w1 * v) + ((- w1) * v)) by BKMODEL1:4
.= |[0,0,0]| + |[0,0,0]| by BKMODEL1:4, EUCLID_5:4
.= |[(0 + 0),(0 + 0),(0 + 0)]| by EUCLID_5:6
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence ((1 * ee1) + ((- (1 - w1)) * u)) + ((- w1) * v) = 0. (TOP-REAL 3) by A7; :: thesis: verum
end;
then A12: P1,P,Q are_collinear by A2, A3, ANPROJ_8:11;
e1 in {e1} by TARSKI:def 1;
then A13: e1 in circle (0,0,1) by A4, XBOOLE_0:def 4;
now :: thesis: ( |[(ee1 . 1),(ee1 . 2)]| in circle (0,0,1) & ee1 . 3 = 1 )
thus |[(ee1 . 1),(ee1 . 2)]| in circle (0,0,1) by A13, EUCLID:53; :: thesis: ee1 . 3 = 1
thus ee1 . 3 = 1 ; :: thesis: verum
end;
then A15: P1 is Element of absolute by BKMODEL1:86;
reconsider g = |[(e2 `1),(e2 `2),1]| as Element of (TOP-REAL 3) ;
not g is zero by EUCLID_5:4, FINSEQ_1:78;
then reconsider ee2 = g as non zero Element of (TOP-REAL 3) ;
reconsider P2 = Dir ee2 as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
((1 * ee2) + ((- (1 - w2)) * v)) + ((- w2) * u) = 0. (TOP-REAL 3)
proof
A16: 1 * ee2 = |[(1 * (ee2 `1)),(1 * (ee2 `2)),(1 * (ee2 `3))]| by EUCLID_5:7
.= ee2 by EUCLID_5:3 ;
ee2 = ((1 - w2) * v) + (w2 * u)
proof
A17: ((1 - w2) * t) + (w2 * s) = |[((((1 - w2) * t) + (w2 * s)) `1),((((1 - w2) * t) + (w2 * s)) `2)]| by EUCLID:53;
((1 - w2) * t) + (w2 * s) = |[((((1 - w2) * t) `1) + ((w2 * s) `1)),((((1 - w2) * t) `2) + ((w2 * s) `2))]| by EUCLID:55
.= |[((((1 - w2) * t) . 1) + ((w2 * s) `1)),((((1 - w2) * t) `2) + ((w2 * s) `2))]| by EUCLID:def 9
.= |[((((1 - w2) * t) . 1) + ((w2 * s) . 1)),((((1 - w2) * t) `2) + ((w2 * s) `2))]| by EUCLID:def 9
.= |[((((1 - w2) * t) . 1) + ((w2 * s) . 1)),((((1 - w2) * t) . 2) + ((w2 * s) `2))]| by EUCLID:def 10
.= |[((((1 - w2) * t) . 1) + ((w2 * s) . 1)),((((1 - w2) * t) . 2) + ((w2 * s) . 2))]| by EUCLID:def 10
.= |[(((1 - w2) * (t . 1)) + ((w2 * s) . 1)),((((1 - w2) * t) . 2) + ((w2 * s) . 2))]| by RVSUM_1:44
.= |[(((1 - w2) * (t . 1)) + (w2 * (s . 1))),((((1 - w2) * t) . 2) + ((w2 * s) . 2))]| by RVSUM_1:44
.= |[(((1 - w2) * (t . 1)) + (w2 * (s . 1))),(((1 - w2) * (t . 2)) + ((w2 * s) . 2))]| by RVSUM_1:44
.= |[(((1 - w2) * (v . 1)) + (w2 * (u . 1))),(((1 - w2) * (v . 2)) + (w2 * (u . 2)))]| by A6, RVSUM_1:44 ;
then A18: ( e2 `1 = ((1 - w2) * (v . 1)) + (w2 * (u . 1)) & e2 `2 = ((1 - w2) * (v . 2)) + (w2 * (u . 2)) ) by A5, A17, FINSEQ_1:77;
((1 - w2) * v) + (w2 * u) = |[(((1 - w2) * (v . 1)) + (w2 * (u . 1))),(((1 - w2) * (v . 2)) + (w2 * (u . 2))),(((1 - w2) * (v . 3)) + (w2 * (u . 3)))]|
proof
((1 - w2) * v) `1 = (1 - w2) * (v `1) by EUCLID_5:9
.= (1 - w2) * (v . 1) by EUCLID_5:def 1 ;
then A19: (((1 - w2) * v) `1) + ((w2 * u) `1) = ((1 - w2) * (v . 1)) + ((w2 * u) . 1) by EUCLID_5:def 1
.= ((1 - w2) * (v . 1)) + (w2 * (u . 1)) by RVSUM_1:44 ;
((1 - w2) * v) `2 = (1 - w2) * (v `2) by EUCLID_5:9
.= (1 - w2) * (v . 2) by EUCLID_5:def 2 ;
then A20: (((1 - w2) * v) `2) + ((w2 * u) `2) = ((1 - w2) * (v . 2)) + ((w2 * u) . 2) by EUCLID_5:def 2
.= ((1 - w2) * (v . 2)) + (w2 * (u . 2)) by RVSUM_1:44 ;
((1 - w2) * v) `3 = (1 - w2) * (v `3) by EUCLID_5:9
.= (1 - w2) * (v . 3) by EUCLID_5:def 3 ;
then (((1 - w2) * v) `3) + ((w2 * u) `3) = ((1 - w2) * (v . 3)) + ((w2 * u) . 3) by EUCLID_5:def 3
.= ((1 - w2) * (v . 3)) + (w2 * (u . 3)) by RVSUM_1:44 ;
hence ((1 - w2) * v) + (w2 * u) = |[(((1 - w2) * (v . 1)) + (w2 * (u . 1))),(((1 - w2) * (v . 2)) + (w2 * (u . 2))),(((1 - w2) * (v . 3)) + (w2 * (u . 3)))]| by EUCLID_5:5, A19, A20; :: thesis: verum
end;
hence ee2 = ((1 - w2) * v) + (w2 * u) by A18, A2, A3; :: thesis: verum
end;
then (ee2 + ((- (1 - w2)) * v)) + ((- w2) * u) = (((1 - w2) * v) + (w2 * u)) + (((- (1 - w2)) * v) + ((- w2) * u)) by RVSUM_1:15
.= ((1 - w2) * v) + ((w2 * u) + (((- (1 - w2)) * v) + ((- w2) * u))) by RVSUM_1:15
.= ((1 - w2) * v) + (((- (1 - w2)) * v) + ((w2 * u) + ((- w2) * u))) by RVSUM_1:15
.= (((1 - w2) * v) + ((- (1 - w2)) * v)) + ((w2 * u) + ((- w2) * u)) by RVSUM_1:15
.= (0. (TOP-REAL 3)) + ((w2 * u) + ((- w2) * u)) by BKMODEL1:4
.= (0. (TOP-REAL 3)) + (0. (TOP-REAL 3)) by BKMODEL1:4
.= |[(0 + 0),(0 + 0),(0 + 0)]| by EUCLID_5:4, EUCLID_5:6
.= 0. (TOP-REAL 3) by EUCLID_5:4 ;
hence ((1 * ee2) + ((- (1 - w2)) * v)) + ((- w2) * u) = 0. (TOP-REAL 3) by A16; :: thesis: verum
end;
then A21: P2,Q,P are_collinear by A2, A3, ANPROJ_8:11;
e2 in (halfline (t,s)) /\ (circle (0,0,1)) by A5, TARSKI:def 1;
then A22: e2 in circle (0,0,1) by XBOOLE_0:def 4;
now :: thesis: ( |[(ee2 . 1),(ee2 . 2)]| in circle (0,0,1) & ee2 . 3 = 1 )
thus |[(ee2 . 1),(ee2 . 2)]| in circle (0,0,1) by A22, EUCLID:53; :: thesis: ee2 . 3 = 1
thus ee2 . 3 = 1 ; :: thesis: verum
end;
then A24: P2 is Element of absolute by BKMODEL1:86;
A25: P1 <> P2
proof
assume P1 = P2 ; :: thesis: contradiction
then are_Prop ee1,ee2 by ANPROJ_1:22;
then consider l being Real such that
l <> 0 and
A26: ee1 = l * ee2 by ANPROJ_1:1;
|[(e1 `1),(e1 `2),1]| = |[(l * (e2 `1)),(l * (e2 `2)),(l * 1)]| by A26, EUCLID_5:8;
then A27: ( 1 = l * 1 & e1 `1 = l * (e2 `1) & e1 `2 = l * (e2 `2) ) by FINSEQ_1:78;
A28: e1 = |[(e1 `1),(e1 `2)]| by EUCLID:53
.= e2 by A27, EUCLID:53 ;
1 - (w1 + w2) <> 0
proof
assume A29: 1 - (w1 + w2) = 0 ; :: thesis: contradiction
A30: 2 * (Sum (sqr (S - T))) = 2 * (Sum (sqr (T - S))) by BKMODEL1:6;
not Sum (sqr (S - T)) is zero
proof
assume A31: Sum (sqr (S - T)) is zero ; :: thesis: contradiction
Sum (sqr (S - T)) = |.(S - T).| ^2 by TOPREAL9:5;
then A32: |.(S - T).| = 0 by A31;
reconsider n = 2 as Nat ;
S = T
proof
reconsider Sn = S, Tn = T as Element of n -tuples_on REAL by EUCLID:def 1;
Sn = (Sn - Tn) + Tn by RVSUM_1:43
.= (0* n) + Tn by A32, EUCLID:8
.= Tn by EUCLID_4:1 ;
hence S = T ; :: thesis: verum
end;
then A33: ( u . 1 = v . 1 & u . 2 = v . 2 & u . 3 = v . 3 ) by A2, A3, FINSEQ_1:77;
A34: |[(u . 1),(u . 2),(u . 3)]| = |[(u `1),(u . 2),(u . 3)]| by EUCLID_5:def 1
.= |[(u `1),(u `2),(u . 3)]| by EUCLID_5:def 2
.= |[(u `1),(u `2),(u `3)]| by EUCLID_5:def 3
.= u by EUCLID_5:3 ;
|[(v . 1),(v . 2),(v . 3)]| = |[(v `1),(v . 2),(v . 3)]| by EUCLID_5:def 1
.= |[(v `1),(v `2),(v . 3)]| by EUCLID_5:def 2
.= |[(v `1),(v `2),(v `3)]| by EUCLID_5:def 3
.= v by EUCLID_5:3 ;
hence contradiction by A1, A2, A3, A34, A33; :: thesis: verum
end;
then reconsider l = Sum (sqr (S - T)) as non zero Real ;
A35: s - |[0,0]| = |[(s `1),(s `2)]| - |[0,0]| by EUCLID:53
.= |[((s `1) - 0),((s `2) - 0)]| by EUCLID:62
.= s by EUCLID:53 ;
A36: t - |[0,0]| = |[(t `1),(t `2)]| - |[0,0]| by EUCLID:53
.= |[((t `1) - 0),((t `2) - 0)]| by EUCLID:62
.= t by EUCLID:53 ;
A38: w1 + w2 = (((- (2 * |((t - s),s)|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),s)|),((Sum (sqr (S - X))) - (1 ^2)))))) / (2 * l)) + (((- (2 * |((s - t),t)|)) + (sqrt (delta ((Sum (sqr (S - T))),(2 * |((s - t),t)|),((Sum (sqr (T - X))) - (1 ^2)))))) / (2 * l)) by A35, A36, BKMODEL1:6
.= (((- (2 * |((t - s),s)|)) + (sqrt (delta (l,(2 * |((t - s),s)|),((Sum (sqr S)) - 1))))) / (2 * l)) + (((- (2 * |((s - t),t)|)) + (sqrt (delta (l,(2 * |((s - t),t)|),((Sum (sqr T)) - 1))))) / (2 * l)) by A35, A36, BKMODEL1:6 ;
reconsider l2 = - (2 * |((t - s),s)|), l3 = - (2 * |((s - t),t)|), l4 = (Sum (sqr S)) - 1, l5 = (Sum (sqr T)) - 1 as Real ;
reconsider l6 = sqrt (delta (l,(- l2),l4)), l7 = sqrt (delta (l,(- l3),l5)), l8 = 2 * l as Real ;
0 <= |.(S - T).| ^2 ;
then A39: 0 <= l by TOPREAL9:5;
|[(u . 1),(u . 2)]| - |[0,0]| = |[((u . 1) - 0),((u . 2) - 0)]| by EUCLID:62
.= s ;
then A40: |.S.| < 1 by A2, TOPREAL9:45;
|[(v . 1),(v . 2)]| - |[0,0]| = |[((v . 1) - 0),((v . 2) - 0)]| by EUCLID:62
.= t ;
then |.T.| < 1 by A3, TOPREAL9:45;
then A42: ( |.S.| ^2 <= 1 & |.T.| ^2 <= 1 ) by A40, XREAL_1:160;
then ( 0 <= delta (l,(- l2),l4) & 0 <= delta (l,(- l3),l5) ) by BKMODEL1:18, A30;
then A43: ( 0 <= l6 & 0 <= l7 ) by SQUARE_1:def 2;
A44: l2 + l3 = l8
proof
|((t - s),s)| + |((s - t),t)| = (|(t,s)| - |(s,s)|) + |((s - t),t)| by EUCLID_2:24
.= ((- |(s,s)|) + |(t,s)|) + (|(s,t)| - |(t,t)|) by EUCLID_2:24
.= - ((|(s,s)| - (2 * |(t,s)|)) + |(t,t)|)
.= - |((s - t),(s - t))| by EUCLID_2:31
.= - (|.(S - T).| ^2) by EUCLID_2:36
.= - (Sum (sqr (S - T))) by TOPREAL9:5 ;
hence l2 + l3 = l8 ; :: thesis: verum
end;
w1 + w2 = ((l2 / l8) + (l6 / l8)) + ((l3 + l7) / l8) by A38, XCMPLX_1:62
.= ((l2 / l8) + (l6 / l8)) + ((l3 / l8) + (l7 / l8)) by XCMPLX_1:62
.= ((l2 / l8) + (l3 / l8)) + ((l6 / l8) + (l7 / l8))
.= (l8 / l8) + ((l6 / l8) + (l7 / l8)) by A44, XCMPLX_1:62
.= 1 + ((l6 / l8) + (l7 / l8)) by XCMPLX_1:60 ;
then 0 = (l6 + l7) / l8 by A29, XCMPLX_1:62;
then ( l6 = 0 & l7 = 0 ) by A43;
then A45: ( delta (l,(- l2),l4) = 0 & delta (l,(- l3),l5) = 0 ) by A42, BKMODEL1:18, A30, SQUARE_1:24;
l4 < 0 hence contradiction by A45, A39, BKMODEL1:5; :: thesis: verum
end;
then reconsider w1w2 = 1 - (w1 + w2) as non zero Real ;
w1w2 * s = w1w2 * t by A28, A4, A5, BKMODEL1:70;
then s = t by EUCLID_4:8;
then A46: ( u . 1 = v . 1 & u . 2 = v . 2 & u . 3 = v . 3 ) by A2, A3, FINSEQ_1:77;
A47: |[(u . 1),(u . 2),(u . 3)]| = |[(u `1),(u . 2),(u . 3)]| by EUCLID_5:def 1
.= |[(u `1),(u `2),(u . 3)]| by EUCLID_5:def 2
.= |[(u `1),(u `2),(u `3)]| by EUCLID_5:def 3
.= u by EUCLID_5:3 ;
|[(v . 1),(v . 2),(v . 3)]| = |[(v `1),(v . 2),(v . 3)]| by EUCLID_5:def 1
.= |[(v `1),(v `2),(v . 3)]| by EUCLID_5:def 2
.= |[(v `1),(v `2),(v `3)]| by EUCLID_5:def 3
.= v by EUCLID_5:3 ;
hence contradiction by A1, A2, A3, A47, A46; :: thesis: verum
end;
A48: P,Q,P1 are_collinear by COLLSP:8, A12;
Q,P2,P are_collinear by A21, COLLSP:7;
then P2,P,Q are_collinear by COLLSP:8;
then P,Q,P2 are_collinear by COLLSP:8;
hence ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear ) by A15, A24, A25, A48; :: thesis: verum