let P, Q, R be Element of absolute ; :: thesis: ( P,Q,R are_mutually_distinct implies not P,Q,R are_collinear )
assume A1: P,Q,R are_mutually_distinct ; :: thesis: not P,Q,R are_collinear
consider up being Element of (TOP-REAL 3) such that
A2: not up is zero and
A3: P = Dir up by ANPROJ_1:26;
consider uq being Element of (TOP-REAL 3) such that
A4: not uq is zero and
A5: Q = Dir uq by ANPROJ_1:26;
consider ur being Element of (TOP-REAL 3) such that
A6: not ur is zero and
A7: R = Dir ur by ANPROJ_1:26;
reconsider up1 = up `1 , up2 = up `2 , up3 = up `3 , uq1 = uq `1 , uq2 = uq `2 , uq3 = uq `3 , ur1 = ur `1 , ur2 = ur `2 , ur3 = ur `3 as Real ;
( up . 3 <> 0 & uq . 3 <> 0 & ur . 3 <> 0 ) by A2, A3, A4, A5, A6, A7, Th67;
then A8: ( up3 <> 0 & uq3 <> 0 & ur3 <> 0 ) by EUCLID_5:def 3;
reconsider vp1 = up1 / up3, vp2 = up2 / up3, vq1 = uq1 / uq3, vq2 = uq2 / uq3, vr1 = ur1 / ur3, vr2 = ur2 / ur3 as Real ;
reconsider vp = |[vp1,vp2,1]|, vq = |[vq1,vq2,1]|, vr = |[vr1,vr2,1]| as non zero Element of (TOP-REAL 3) by Th36;
A9: ( vp `3 = 1 & vq `3 = 1 & vr `3 = 1 ) by EUCLID_5:2;
then A10: ( vp . 3 = 1 & vq . 3 = 1 & vr . 3 = 1 ) by EUCLID_5:def 3;
A11: ( P = Dir vp & Q = Dir vq & R = Dir vr )
proof
thus P = Dir vp :: thesis: ( Q = Dir vq & R = Dir vr )
proof
are_Prop up,vp
proof
up3 * vp = |[(up3 * (up1 / up3)),(up3 * (up2 / up3)),(up3 * 1)]| by EUCLID_5:8
.= |[up1,(up3 * (up2 / up3)),(up3 * 1)]| by A8, XCMPLX_1:87
.= |[up1,up2,(up3 * 1)]| by A8, XCMPLX_1:87
.= up by EUCLID_5:3 ;
hence are_Prop up,vp by A8, ANPROJ_1:1; :: thesis: verum
end;
hence P = Dir vp by A2, A3, ANPROJ_1:22; :: thesis: verum
end;
thus Q = Dir vq :: thesis: R = Dir vr
proof
are_Prop uq,vq
proof
uq3 * vq = |[(uq3 * (uq1 / uq3)),(uq3 * (uq2 / uq3)),(uq3 * 1)]| by EUCLID_5:8
.= |[uq1,(uq3 * (uq2 / uq3)),(uq3 * 1)]| by A8, XCMPLX_1:87
.= |[uq1,uq2,(uq3 * 1)]| by A8, XCMPLX_1:87
.= uq by EUCLID_5:3 ;
hence are_Prop uq,vq by A8, ANPROJ_1:1; :: thesis: verum
end;
hence Q = Dir vq by A4, A5, ANPROJ_1:22; :: thesis: verum
end;
thus R = Dir vr :: thesis: verum
proof
are_Prop ur,vr
proof
ur3 * vr = |[(ur3 * (ur1 / ur3)),(ur3 * (ur2 / ur3)),(ur3 * 1)]| by EUCLID_5:8
.= |[ur1,(ur3 * (ur2 / ur3)),(ur3 * 1)]| by A8, XCMPLX_1:87
.= |[ur1,ur2,(ur3 * 1)]| by A8, XCMPLX_1:87
.= ur by EUCLID_5:3 ;
hence are_Prop ur,vr by A8, ANPROJ_1:1; :: thesis: verum
end;
hence R = Dir vr by A6, A7, ANPROJ_1:22; :: thesis: verum
end;
end;
assume P,Q,R are_collinear ; :: thesis: contradiction
then consider tp, tq, tr being Element of (TOP-REAL 3) such that
A12: ( P = Dir tp & Q = Dir tq & R = Dir tr ) and
A13: ( not tp is zero & not tq is zero & not tr is zero ) and
A14: ex a1, b1, c1 being Real st
( ((a1 * tp) + (b1 * tq)) + (c1 * tr) = 0. (TOP-REAL 3) & ( a1 <> 0 or b1 <> 0 or c1 <> 0 ) ) by ANPROJ_8:11;
consider a1, b1, c1 being Real such that
A15: ((a1 * tp) + (b1 * tq)) + (c1 * tr) = 0. (TOP-REAL 3) and
A16: ( a1 <> 0 or b1 <> 0 or c1 <> 0 ) by A14;
A17: ( are_Prop tp,vp & are_Prop tq,vq & are_Prop tr,vr ) by A12, A13, A11, ANPROJ_1:22;
consider lp being Real such that
A18: lp <> 0 and
A19: tp = lp * vp by A17, ANPROJ_1:1;
consider lq being Real such that
A20: lq <> 0 and
A21: tq = lq * vq by A17, ANPROJ_1:1;
consider lr being Real such that
A22: lr <> 0 and
A23: tr = lr * vr by A17, ANPROJ_1:1;
reconsider A = |[(vp `1),(vp `2)]|, B = |[(vq `1),(vq `2)]|, C = |[(vr `1),(vr `2)]| as Element of (TOP-REAL 2) ;
A24: B . 1 = B `1 by EUCLID:def 9
.= vq `1 by EUCLID:52
.= vq . 1 by EUCLID_5:def 1 ;
A25: B . 2 = B `2 by EUCLID:def 10
.= vq `2 by EUCLID:52
.= vq . 2 by EUCLID_5:def 2 ;
A26: C . 1 = C `1 by EUCLID:def 9
.= vr `1 by EUCLID:52
.= vr . 1 by EUCLID_5:def 1 ;
A27: C . 2 = C `2 by EUCLID:def 10
.= vr `2 by EUCLID:52
.= vr . 2 by EUCLID_5:def 2 ;
A28: A . 1 = A `1 by EUCLID:def 9
.= vp `1 by EUCLID:52
.= vp . 1 by EUCLID_5:def 1 ;
A29: A . 2 = A `2 by EUCLID:def 10
.= vp `2 by EUCLID:52
.= vp . 2 by EUCLID_5:def 2 ;
A30: A <> B
proof
assume A = B ; :: thesis: contradiction
then A30BIS: ( vp `1 = vq `1 & vp `2 = vq `2 ) by FINSEQ_1:77;
vp = |[(vp `1),(vp `2),(vp `3)]| by EUCLID_5:3
.= vq by A9, A30BIS, EUCLID_5:3 ;
hence contradiction by A11, A1; :: thesis: verum
end;
A31: A <> C
proof
assume A = C ; :: thesis: contradiction
then A31BIS: ( vp `1 = vr `1 & vp `2 = vr `2 ) by FINSEQ_1:77;
vp = |[(vp `1),(vp `2),(vp `3)]| by EUCLID_5:3
.= vr by A9, A31BIS, EUCLID_5:3 ;
hence contradiction by A11, A1; :: thesis: verum
end;
A32: B <> C
proof
assume B = C ; :: thesis: contradiction
then A32BIS: ( vq `1 = vr `1 & vq `2 = vr `2 ) by FINSEQ_1:77;
vq = |[(vq `1),(vq `2),(vq `3)]| by EUCLID_5:3
.= vr by A9, A32BIS, EUCLID_5:3 ;
hence contradiction by A11, A1; :: thesis: verum
end;
A34: A in Sphere ((0. (TOP-REAL 2)),1)
proof
A35: qfconic (1,1,(- 1),0,0,0,vp) = 0
proof
P in conic (1,1,(- 1),0,0,0) ;
then P in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 } by PASCAL:def 2;
then ex PP being Point of (ProjectiveSpace (TOP-REAL 3)) st
( P = PP & ( for u being Element of (TOP-REAL 3) st not u is zero & PP = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 ) ) ;
hence qfconic (1,1,(- 1),0,0,0,vp) = 0 by A11; :: thesis: verum
end;
( vp . 1 = vp `1 & vp . 2 = vp `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;
hence A in Sphere ((0. (TOP-REAL 2)),1) by A35, A10, Th70; :: thesis: verum
end;
A36: qfconic (1,1,(- 1),0,0,0,vq) = 0
proof
Q in conic (1,1,(- 1),0,0,0) ;
then Q in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 } by PASCAL:def 2;
then ex QP being Point of (ProjectiveSpace (TOP-REAL 3)) st
( Q = QP & ( for u being Element of (TOP-REAL 3) st not u is zero & QP = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 ) ) ;
hence qfconic (1,1,(- 1),0,0,0,vq) = 0 by A11; :: thesis: verum
end;
( vq . 1 = vq `1 & vq . 2 = vq `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;
then A37: B in Sphere ((0. (TOP-REAL 2)),1) by A36, A10, Th70;
A38: C in Sphere ((0. (TOP-REAL 2)),1)
proof
A39: qfconic (1,1,(- 1),0,0,0,vr) = 0
proof
R in conic (1,1,(- 1),0,0,0) ;
then R in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 } by PASCAL:def 2;
then ex RP being Point of (ProjectiveSpace (TOP-REAL 3)) st
( R = RP & ( for u being Element of (TOP-REAL 3) st not u is zero & RP = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 ) ) ;
hence qfconic (1,1,(- 1),0,0,0,vr) = 0 by A11; :: thesis: verum
end;
( vr . 1 = vr `1 & vr . 2 = vr `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;
hence C in Sphere ((0. (TOP-REAL 2)),1) by A39, A10, Th70; :: thesis: verum
end;
A40: ( (halfline (B,C)) /\ (Sphere ((0. (TOP-REAL 2)),1)) = {B,C} & (halfline (C,B)) /\ (Sphere ((0. (TOP-REAL 2)),1)) = {C,B} & (halfline (A,C)) /\ (Sphere ((0. (TOP-REAL 2)),1)) = {A,C} & (halfline (C,A)) /\ (Sphere ((0. (TOP-REAL 2)),1)) = {C,A} & (halfline (A,B)) /\ (Sphere ((0. (TOP-REAL 2)),1)) = {A,B} & (halfline (B,A)) /\ (Sphere ((0. (TOP-REAL 2)),1)) = {B,A} ) by A37, A38, A34, TOPREAL9:36;
per cases ( a1 <> 0 or b1 <> 0 or c1 <> 0 ) by A16;
suppose a1 <> 0 ; :: thesis: contradiction
then A41: lp * vp = (((- b1) / a1) * (lq * vq)) + (((- c1) / a1) * (lr * vr)) by A19, A21, A23, A15, ANPROJ_8:12
.= ((((- b1) / a1) * lq) * vq) + (((- c1) / a1) * (lr * vr)) by RVSUM_1:49
.= ((((- b1) / a1) * lq) * vq) + ((((- c1) / a1) * lr) * vr) by RVSUM_1:49 ;
reconsider m1 = (1 / lp) * (((- b1) / a1) * lq), m2 = (1 / lp) * (((- c1) / a1) * lr) as Real ;
1 = lp / lp by A18, XCMPLX_1:60
.= (1 / lp) * lp by XCMPLX_1:99 ;
then A42: vp = ((1 / lp) * lp) * vp by RVSUM_1:52
.= (1 / lp) * (((((- b1) / a1) * lq) * vq) + ((((- c1) / a1) * lr) * vr)) by A41, RVSUM_1:49
.= ((1 / lp) * ((((- b1) / a1) * lq) * vq)) + ((1 / lp) * ((((- c1) / a1) * lr) * vr)) by RVSUM_1:51
.= (((1 / lp) * (((- b1) / a1) * lq)) * vq) + ((1 / lp) * ((((- c1) / a1) * lr) * vr)) by RVSUM_1:49
.= (m1 * vq) + (m2 * vr) by RVSUM_1:49 ;
A43: m1 = 1 - m2
proof
(m1 * vq) + (m2 * vr) = |[(m1 * (vq `1)),(m1 * (vq `2)),(m1 * (vq `3))]| + (m2 * vr) by EUCLID_5:7
.= |[(m1 * (vq `1)),(m1 * (vq `2)),(m1 * (vq `3))]| + |[(m2 * (vr `1)),(m2 * (vr `2)),(m2 * (vr `3))]| by EUCLID_5:7
.= |[((m1 * (vq `1)) + (m2 * (vr `1))),((m1 * (vq `2)) + (m2 * (vr `2))),((m1 * (vq `3)) + (m2 * (vr `3)))]| by EUCLID_5:6 ;
then vp `3 = (m1 * (vq `3)) + (m2 * (vr `3)) by A42, EUCLID_5:14;
hence m1 = 1 - m2 by A9; :: thesis: verum
end;
per cases ( 0 <= m2 or m2 < 0 ) ;
suppose A44: 0 <= m2 ; :: thesis: contradiction
A45: A in halfline (B,C)
proof
reconsider tu = (1 - m2) * vq, tv = m2 * vr as Element of (TOP-REAL 3) ;
A46: ((1 - m2) * vq) . 1 = (1 - m2) * (vq . 1) by RVSUM_1:44;
A47: ( tu `1 = tu . 1 & tv `1 = tv . 1 ) by EUCLID_5:def 1;
A48: A `1 = vp `1 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `1 by A43, A42, EUCLID_5:5
.= (tu . 1) + (tv . 1) by A47, EUCLID_5:2
.= ((1 - m2) * (B . 1)) + (m2 * (C . 1)) by A46, RVSUM_1:44, A24, A26 ;
A49: ((1 - m2) * vq) . 2 = (1 - m2) * (vq . 2) by RVSUM_1:44;
A50: ( tu `2 = tu . 2 & tv `2 = tv . 2 ) by EUCLID_5:def 2;
A51: A `2 = vp `2 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `2 by A43, A42, EUCLID_5:5
.= (tu . 2) + (tv . 2) by A50, EUCLID_5:2
.= ((1 - m2) * (B . 2)) + (m2 * (C . 2)) by A49, A25, A27, RVSUM_1:44 ;
A52: B = |[(B `1),(B `2)]| by EUCLID:53
.= |[(B `1),(B . 2)]| by EUCLID:def 10
.= |[(B . 1),(B . 2)]| by EUCLID:def 9 ;
A53: C = |[(C `1),(C `2)]| by EUCLID:53
.= |[(C `1),(C . 2)]| by EUCLID:def 10
.= |[(C . 1),(C . 2)]| by EUCLID:def 9 ;
A = |[(((1 - m2) * (B . 1)) + (m2 * (C . 1))),(((1 - m2) * (B . 2)) + (m2 * (C . 2)))]| by A48, A51, EUCLID:53
.= |[((1 - m2) * (B . 1)),((1 - m2) * (B . 2))]| + |[(m2 * (C . 1)),(m2 * (C . 2))]| by EUCLID:56
.= ((1 - m2) * |[(B . 1),(B . 2)]|) + |[(m2 * (C . 1)),(m2 * (C . 2))]| by EUCLID:58
.= ((1 - m2) * B) + (m2 * C) by A52, A53, EUCLID:58 ;
hence A in halfline (B,C) by A44, TOPREAL9:26; :: thesis: verum
end;
A in (halfline (B,C)) /\ (Sphere ((0. (TOP-REAL 2)),1)) by A45, A34, XBOOLE_0:def 4;
hence contradiction by A30, A31, A40, TARSKI:def 2; :: thesis: verum
end;
suppose A54: m2 < 0 ; :: thesis: contradiction
set m3 = 1 - m2;
A in halfline (C,B)
proof
reconsider tu = (1 - (1 - m2)) * vr, tv = (1 - m2) * vq as Element of (TOP-REAL 3) ;
A55: ((1 - (1 - m2)) * vr) . 1 = (1 - (1 - m2)) * (vr . 1) by RVSUM_1:44;
A56: ( tu `1 = tu . 1 & tv `1 = tv . 1 ) by EUCLID_5:def 1;
A56b: A `1 = vp `1 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `1 by A43, A42, EUCLID_5:5
.= (tu . 1) + (tv . 1) by EUCLID_5:2, A56
.= ((1 - (1 - m2)) * (C . 1)) + ((1 - m2) * (B . 1)) by A24, A26, A55, RVSUM_1:44 ;
A57: ((1 - (1 - m2)) * vr) . 2 = (1 - (1 - m2)) * (vr . 2) by RVSUM_1:44;
A58: ( tu `2 = tu . 2 & tv `2 = tv . 2 ) by EUCLID_5:def 2;
A59: A `2 = vp `2 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `2 by A43, A42, EUCLID_5:5
.= (tu `2) + (tv `2) by EUCLID_5:2
.= ((1 - (1 - m2)) * (C . 2)) + ((1 - m2) * (B . 2)) by A57, A58, RVSUM_1:44, A25, A27 ;
A60: B = |[(B `1),(B `2)]| by EUCLID:53
.= |[(B `1),(B . 2)]| by EUCLID:def 10
.= |[(B . 1),(B . 2)]| by EUCLID:def 9 ;
A61: C = |[(C `1),(C `2)]| by EUCLID:53
.= |[(C `1),(C . 2)]| by EUCLID:def 10
.= |[(C . 1),(C . 2)]| by EUCLID:def 9 ;
A = |[(((1 - (1 - m2)) * (C . 1)) + ((1 - m2) * (B . 1))),(((1 - (1 - m2)) * (C . 2)) + ((1 - m2) * (B . 2)))]| by A56b, A59, EUCLID:53
.= |[((1 - (1 - m2)) * (C . 1)),((1 - (1 - m2)) * (C . 2))]| + |[((1 - m2) * (B . 1)),((1 - m2) * (B . 2))]| by EUCLID:56
.= ((1 - (1 - m2)) * |[(C . 1),(C . 2)]|) + |[((1 - m2) * (B . 1)),((1 - m2) * (B . 2))]| by EUCLID:58
.= ((1 - (1 - m2)) * C) + ((1 - m2) * B) by A60, A61, EUCLID:58 ;
hence A in halfline (C,B) by A54, TOPREAL9:26; :: thesis: verum
end;
then A in {C,B} by A40, A34, XBOOLE_0:def 4;
hence contradiction by A30, A31, TARSKI:def 2; :: thesis: verum
end;
end;
end;
suppose A62: b1 <> 0 ; :: thesis: contradiction
((b1 * tq) + (a1 * tp)) + (c1 * tr) = 0. (TOP-REAL 3) by A15;
then A63: lq * vq = (((- a1) / b1) * (lp * vp)) + (((- c1) / b1) * (lr * vr)) by A19, A21, A23, A62, ANPROJ_8:12
.= ((((- a1) / b1) * lp) * vp) + (((- c1) / b1) * (lr * vr)) by RVSUM_1:49
.= ((((- a1) / b1) * lp) * vp) + ((((- c1) / b1) * lr) * vr) by RVSUM_1:49 ;
reconsider m1 = (1 / lq) * (((- a1) / b1) * lp), m2 = (1 / lq) * (((- c1) / b1) * lr) as Real ;
1 = lq / lq by A20, XCMPLX_1:60
.= (1 / lq) * lq by XCMPLX_1:99 ;
then A65: vq = ((1 / lq) * lq) * vq by RVSUM_1:52
.= (1 / lq) * (((((- a1) / b1) * lp) * vp) + ((((- c1) / b1) * lr) * vr)) by A63, RVSUM_1:49
.= ((1 / lq) * ((((- a1) / b1) * lp) * vp)) + ((1 / lq) * ((((- c1) / b1) * lr) * vr)) by RVSUM_1:51
.= (((1 / lq) * (((- a1) / b1) * lp)) * vp) + ((1 / lq) * ((((- c1) / b1) * lr) * vr)) by RVSUM_1:49
.= (m1 * vp) + (m2 * vr) by RVSUM_1:49 ;
A66: m1 = 1 - m2
proof
(m1 * vp) + (m2 * vr) = |[(m1 * (vp `1)),(m1 * (vp `2)),(m1 * (vp `3))]| + (m2 * vr) by EUCLID_5:7
.= |[(m1 * (vp `1)),(m1 * (vp `2)),(m1 * (vp `3))]| + |[(m2 * (vr `1)),(m2 * (vr `2)),(m2 * (vr `3))]| by EUCLID_5:7
.= |[((m1 * (vp `1)) + (m2 * (vr `1))),((m1 * (vp `2)) + (m2 * (vr `2))),((m1 * (vp `3)) + (m2 * (vr `3)))]| by EUCLID_5:6 ;
then 1 = (m1 * 1) + (m2 * 1) by A9, A65, EUCLID_5:14;
hence m1 = 1 - m2 ; :: thesis: verum
end;
per cases ( 0 <= m2 or m2 < 0 ) ;
suppose A67: 0 <= m2 ; :: thesis: contradiction
B in halfline (A,C)
proof
reconsider tu = (1 - m2) * vp, tv = m2 * vr as Element of (TOP-REAL 3) ;
A68: ((1 - m2) * vp) . 1 = (1 - m2) * (vp . 1) by RVSUM_1:44;
A69: ( tu `1 = tu . 1 & tv `1 = tv . 1 ) by EUCLID_5:def 1;
A70: B `1 = vq `1 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `1 by A66, A65, EUCLID_5:5
.= (tu `1) + (tv `1) by EUCLID_5:2
.= ((1 - m2) * (A . 1)) + (m2 * (C . 1)) by A26, A28, A68, A69, RVSUM_1:44 ;
A71: ((1 - m2) * vp) . 2 = (1 - m2) * (vp . 2) by RVSUM_1:44;
A72: ( tu `2 = tu . 2 & tv `2 = tv . 2 ) by EUCLID_5:def 2;
A73: B `2 = vq `2 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `2 by A66, A65, EUCLID_5:5
.= (tu `2) + (tv `2) by EUCLID_5:2
.= ((1 - m2) * (A . 2)) + (m2 * (C . 2)) by A27, A29, A71, A72, RVSUM_1:44 ;
A74: A = |[(A `1),(A `2)]| by EUCLID:53
.= |[(A `1),(A . 2)]| by EUCLID:def 10
.= |[(A . 1),(A . 2)]| by EUCLID:def 9 ;
A75: C = |[(C `1),(C `2)]| by EUCLID:53
.= |[(C `1),(C . 2)]| by EUCLID:def 10
.= |[(C . 1),(C . 2)]| by EUCLID:def 9 ;
B = |[(((1 - m2) * (A . 1)) + (m2 * (C . 1))),(((1 - m2) * (A . 2)) + (m2 * (C . 2)))]| by A70, A73, EUCLID:53
.= |[((1 - m2) * (A . 1)),((1 - m2) * (A . 2))]| + |[(m2 * (C . 1)),(m2 * (C . 2))]| by EUCLID:56
.= ((1 - m2) * |[(A . 1),(A . 2)]|) + |[(m2 * (C . 1)),(m2 * (C . 2))]| by EUCLID:58
.= ((1 - m2) * A) + (m2 * C) by A74, A75, EUCLID:58 ;
hence B in halfline (A,C) by A67, TOPREAL9:26; :: thesis: verum
end;
then B in {A,C} by A40, A37, XBOOLE_0:def 4;
hence contradiction by A30, A32, TARSKI:def 2; :: thesis: verum
end;
suppose A76: m2 < 0 ; :: thesis: contradiction
set m3 = 1 - m2;
B in halfline (C,A)
proof
reconsider tu = (1 - (1 - m2)) * vr, tv = (1 - m2) * vp as Element of (TOP-REAL 3) ;
A77: ((1 - (1 - m2)) * vr) . 1 = (1 - (1 - m2)) * (vr . 1) by RVSUM_1:44;
A78: ( tu `1 = tu . 1 & tv `1 = tv . 1 ) by EUCLID_5:def 1;
A79: B `1 = vq `1 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `1 by EUCLID_5:5, A66, A65
.= (tu `1) + (tv `1) by EUCLID_5:2
.= ((1 - (1 - m2)) * (C . 1)) + ((1 - m2) * (A . 1)) by A26, A28, A77, A78, RVSUM_1:44 ;
A80: ((1 - (1 - m2)) * vr) . 2 = (1 - (1 - m2)) * (vr . 2) by RVSUM_1:44;
A81: ( tu `2 = tu . 2 & tv `2 = tv . 2 ) by EUCLID_5:def 2;
A82: B `2 = vq `2 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `2 by A66, A65, EUCLID_5:5
.= (tu `2) + (tv `2) by EUCLID_5:2
.= ((1 - (1 - m2)) * (C . 2)) + ((1 - m2) * (A . 2)) by A27, A29, A80, A81, RVSUM_1:44 ;
A83: A = |[(A `1),(A `2)]| by EUCLID:53
.= |[(A `1),(A . 2)]| by EUCLID:def 10
.= |[(A . 1),(A . 2)]| by EUCLID:def 9 ;
A84: C = |[(C `1),(C `2)]| by EUCLID:53
.= |[(C `1),(C . 2)]| by EUCLID:def 10
.= |[(C . 1),(C . 2)]| by EUCLID:def 9 ;
B = |[(((1 - (1 - m2)) * (C . 1)) + ((1 - m2) * (A . 1))),(((1 - (1 - m2)) * (C . 2)) + ((1 - m2) * (A . 2)))]| by A79, A82, EUCLID:53
.= |[((1 - (1 - m2)) * (C . 1)),((1 - (1 - m2)) * (C . 2))]| + |[((1 - m2) * (A . 1)),((1 - m2) * (A . 2))]| by EUCLID:56
.= ((1 - (1 - m2)) * |[(C . 1),(C . 2)]|) + |[((1 - m2) * (A . 1)),((1 - m2) * (A . 2))]| by EUCLID:58
.= ((1 - (1 - m2)) * C) + ((1 - m2) * A) by A83, A84, EUCLID:58 ;
hence B in halfline (C,A) by A76, TOPREAL9:26; :: thesis: verum
end;
then B in {C,A} by A40, A37, XBOOLE_0:def 4;
hence contradiction by A30, A32, TARSKI:def 2; :: thesis: verum
end;
end;
end;
suppose A85: c1 <> 0 ; :: thesis: contradiction
((c1 * tr) + (a1 * tp)) + (b1 * tq) = 0. (TOP-REAL 3) by A15, RVSUM_1:15;
then A86: lr * vr = (((- a1) / c1) * (lp * vp)) + (((- b1) / c1) * (lq * vq)) by A19, A21, A23, A85, ANPROJ_8:12
.= ((((- a1) / c1) * lp) * vp) + (((- b1) / c1) * (lq * vq)) by RVSUM_1:49
.= ((((- a1) / c1) * lp) * vp) + ((((- b1) / c1) * lq) * vq) by RVSUM_1:49 ;
reconsider m1 = (1 / lr) * (((- a1) / c1) * lp), m2 = (1 / lr) * (((- b1) / c1) * lq) as Real ;
1 = lr / lr by A22, XCMPLX_1:60
.= (1 / lr) * lr by XCMPLX_1:99 ;
then A87: vr = ((1 / lr) * lr) * vr by RVSUM_1:52
.= (1 / lr) * (((((- a1) / c1) * lp) * vp) + ((((- b1) / c1) * lq) * vq)) by A86, RVSUM_1:49
.= ((1 / lr) * ((((- a1) / c1) * lp) * vp)) + ((1 / lr) * ((((- b1) / c1) * lq) * vq)) by RVSUM_1:51
.= (((1 / lr) * (((- a1) / c1) * lp)) * vp) + ((1 / lr) * ((((- b1) / c1) * lq) * vq)) by RVSUM_1:49
.= (m1 * vp) + (m2 * vq) by RVSUM_1:49 ;
A88: m1 = 1 - m2
proof
(m1 * vp) + (m2 * vq) = |[(m1 * (vp `1)),(m1 * (vp `2)),(m1 * (vp `3))]| + (m2 * vq) by EUCLID_5:7
.= |[(m1 * (vp `1)),(m1 * (vp `2)),(m1 * (vp `3))]| + |[(m2 * (vq `1)),(m2 * (vq `2)),(m2 * (vq `3))]| by EUCLID_5:7
.= |[((m1 * (vp `1)) + (m2 * (vq `1))),((m1 * (vp `2)) + (m2 * (vq `2))),((m1 * (vp `3)) + (m2 * (vq `3)))]| by EUCLID_5:6 ;
then 1 = (m1 * 1) + (m2 * 1) by A87, EUCLID_5:14, A9;
hence m1 = 1 - m2 ; :: thesis: verum
end;
per cases ( 0 <= m2 or m2 < 0 ) ;
suppose A89: 0 <= m2 ; :: thesis: contradiction
C in halfline (A,B)
proof
reconsider tu = (1 - m2) * vp, tv = m2 * vq as Element of (TOP-REAL 3) ;
A90: ((1 - m2) * vp) . 1 = (1 - m2) * (vp . 1) by RVSUM_1:44;
A91: ( tu `1 = tu . 1 & tv `1 = tv . 1 ) by EUCLID_5:def 1;
A92: C `1 = vr `1 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `1 by A88, A87, EUCLID_5:5
.= (tu . 1) + (tv . 1) by A91, EUCLID_5:2
.= ((1 - m2) * (A . 1)) + (m2 * (B . 1)) by A24, A28, A90, RVSUM_1:44 ;
A93: ((1 - m2) * vp) . 2 = (1 - m2) * (vp . 2) by RVSUM_1:44;
A94: ( tu `2 = tu . 2 & tv `2 = tv . 2 ) by EUCLID_5:def 2;
A95: C `2 = vr `2 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `2 by A88, A87, EUCLID_5:5
.= (tu `2) + (tv `2) by EUCLID_5:2
.= ((1 - m2) * (A . 2)) + (m2 * (B . 2)) by A25, A29, A93, A94, RVSUM_1:44 ;
A96: A = |[(A `1),(A `2)]| by EUCLID:53
.= |[(A `1),(A . 2)]| by EUCLID:def 10
.= |[(A . 1),(A . 2)]| by EUCLID:def 9 ;
A97: B = |[(B `1),(B `2)]| by EUCLID:53
.= |[(B `1),(B . 2)]| by EUCLID:def 10
.= |[(B . 1),(B . 2)]| by EUCLID:def 9 ;
C = |[(C `1),(C `2)]| by EUCLID:53
.= |[((1 - m2) * (A . 1)),((1 - m2) * (A . 2))]| + |[(m2 * (B . 1)),(m2 * (B . 2))]| by A92, A95, EUCLID:56
.= ((1 - m2) * |[(A . 1),(A . 2)]|) + |[(m2 * (B . 1)),(m2 * (B . 2))]| by EUCLID:58
.= ((1 - m2) * A) + (m2 * B) by EUCLID:58, A96, A97 ;
hence C in halfline (A,B) by A89, TOPREAL9:26; :: thesis: verum
end;
then C in {A,B} by A40, A38, XBOOLE_0:def 4;
hence contradiction by A31, A32, TARSKI:def 2; :: thesis: verum
end;
suppose A98: m2 < 0 ; :: thesis: contradiction
set m3 = 1 - m2;
C in halfline (B,A)
proof
reconsider tu = (1 - (1 - m2)) * vq, tv = (1 - m2) * vp as Element of (TOP-REAL 3) ;
A99: ((1 - (1 - m2)) * vq) . 1 = (1 - (1 - m2)) * (vq . 1) by RVSUM_1:44;
A100: ( tu `1 = tu . 1 & tv `1 = tv . 1 ) by EUCLID_5:def 1;
A101: C `1 = vr `1 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `1 by A88, A87, EUCLID_5:5
.= (tu . 1) + (tv . 1) by A100, EUCLID_5:2
.= ((1 - (1 - m2)) * (B . 1)) + ((1 - m2) * (A . 1)) by A24, A28, A99, RVSUM_1:44 ;
A102: ((1 - (1 - m2)) * vq) . 2 = (1 - (1 - m2)) * (vq . 2) by RVSUM_1:44;
A103: ( tu `2 = tu . 2 & tv `2 = tv . 2 ) by EUCLID_5:def 2;
A104: C `2 = vr `2 by EUCLID:52
.= |[((tu `1) + (tv `1)),((tu `2) + (tv `2)),((tu `3) + (tv `3))]| `2 by A88, A87, EUCLID_5:5
.= (tu `2) + (tv `2) by EUCLID_5:2
.= ((1 - (1 - m2)) * (B . 2)) + ((1 - m2) * (A . 2)) by A25, A29, A102, A103, RVSUM_1:44 ;
A105: A = |[(A `1),(A `2)]| by EUCLID:53
.= |[(A `1),(A . 2)]| by EUCLID:def 10
.= |[(A . 1),(A . 2)]| by EUCLID:def 9 ;
A106: B = |[(B `1),(B `2)]| by EUCLID:53
.= |[(B `1),(B . 2)]| by EUCLID:def 10
.= |[(B . 1),(B . 2)]| by EUCLID:def 9 ;
C = |[(((1 - (1 - m2)) * (B . 1)) + ((1 - m2) * (A . 1))),(((1 - (1 - m2)) * (B . 2)) + ((1 - m2) * (A . 2)))]| by A101, A104, EUCLID:53
.= |[((1 - (1 - m2)) * (B . 1)),((1 - (1 - m2)) * (B . 2))]| + |[((1 - m2) * (A . 1)),((1 - m2) * (A . 2))]| by EUCLID:56
.= ((1 - (1 - m2)) * |[(B . 1),(B . 2)]|) + |[((1 - m2) * (A . 1)),((1 - m2) * (A . 2))]| by EUCLID:58
.= ((1 - (1 - m2)) * B) + ((1 - m2) * A) by A105, A106, EUCLID:58 ;
hence C in halfline (B,A) by A98, TOPREAL9:26; :: thesis: verum
end;
then C in {B,A} by A40, A38, XBOOLE_0:def 4;
hence contradiction by A31, A32, TARSKI:def 2; :: thesis: verum
end;
end;
end;
end;