let a, b, c be Element of (OASpace (TOP-REAL 2)); :: thesis: ( Mid a,b,c iff ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) )
A1: now :: thesis: ( not Mid a,b,c or a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) )
assume Mid a,b,c ; :: thesis: ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) )
then a,b // b,c ;
then consider u, v, w, y being VECTOR of (TOP-REAL 2) such that
A2: [a,b] = [u,v] and
A3: [b,c] = [w,y] and
A4: u,v // w,y by ANALOAF:def 3;
A5: ( a = u & b = v & b = w & c = y ) by A2, A3, XTUPLE_0:1;
per cases ( u = v or w = y or ex r, s being Real st
( 0 < r & 0 < s & r * (v - u) = s * (y - w) ) ) by A4;
suppose u = v ; :: thesis: ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) )
hence ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) by A5; :: thesis: verum
end;
suppose w = y ; :: thesis: ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) )
hence ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) by A5; :: thesis: verum
end;
suppose ex r, s being Real st
( 0 < r & 0 < s & r * (v - u) = s * (y - w) ) ; :: thesis: ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) )
then consider r, s being Real such that
A6: 0 < r and
A7: 0 < s and
A8: r * (v - u) = s * (y - w) ;
(r * v) - (r * u) = r * (v - u) by RLVECT_1:34
.= (s * y) - (s * v) by A5, A8, RLVECT_1:34 ;
then A9: (r + s) * v = (r * u) + (s * y) by THJC;
reconsider t = 1 / (r + s) as Real ;
A10: 1 - (s / (r + s)) = ((r + s) / (r + s)) - (s / (r + s)) by A6, A7, XCMPLX_1:60
.= r / (r + s) ;
A11: (1 / (r + s)) * (r + s) = (r + s) / (r + s)
.= 1 by A6, A7, XCMPLX_1:60 ;
A12: v = 1 * v by RVSUM_1:52
.= t * ((r + s) * v) by A11, RVSUM_1:49
.= (t * (r * u)) + (t * (s * y)) by RVSUM_1:51, A9
.= ((t * r) * u) + (t * (s * y)) by RVSUM_1:49
.= ((1 - (s / (r + s))) * u) + ((s / (r + s)) * y) by A10, RVSUM_1:49 ;
reconsider l = s / (r + s) as Real ;
( 0 <= l & l <= 1 & v = ((1 - l) * u) + (l * y) ) by A12, A6, A7, THJD;
then v in { (((1 - l) * u) + (l * y)) where l is Real : ( 0 <= l & l <= 1 ) } ;
then b in LSeg (u,y) by A5, RLTOPSP1:def 2;
hence ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) by A5; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) implies Mid a,b,c )
assume A13: ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) ; :: thesis: Mid a,b,c
reconsider OAS = OASpace (TOP-REAL 2) as OAffinSpace by THQQ;
per cases ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) by A13;
suppose A14: a = b ; :: thesis: Mid a,b,c
( a is Element of OAS & b is Element of OAS ) ;
hence Mid a,b,c by A14, DIRAF:10; :: thesis: verum
end;
suppose A15: b = c ; :: thesis: Mid a,b,c
( b is Element of OAS & c is Element of OAS ) ;
hence Mid a,b,c by A15, DIRAF:10; :: thesis: verum
end;
suppose ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ; :: thesis: Mid a,b,c
then consider u, v being Point of (TOP-REAL 2) such that
A16: u = a and
A17: v = c and
A18: b in LSeg (u,v) ;
b in { (((1 - l) * u) + (l * v)) where l is Real : ( 0 <= l & l <= 1 ) } by RLTOPSP1:def 2, A18;
then consider l being Real such that
A19: b = ((1 - l) * u) + (l * v) and
A20: 0 <= l and
A21: l <= 1 ;
reconsider w = b, y = b as Point of (TOP-REAL 2) ;
now :: thesis: ex u, w, y, v being Point of (TOP-REAL 2) st
( [a,b] = [u,w] & [b,c] = [y,v] & u,w // y,v )
take u = u; :: thesis: ex w, y, v being Point of (TOP-REAL 2) st
( [a,b] = [u,w] & [b,c] = [y,v] & b4,b5 // b6,b7 )
take w = w; :: thesis: ex y, v being Point of (TOP-REAL 2) st
( [a,b] = [u,w] & [b,c] = [y,v] & b3,b4 // b5,b6 )
take y = y; :: thesis: ex v being Point of (TOP-REAL 2) st
( [a,b] = [u,w] & [b,c] = [y,v] & b2,b3 // b4,b5 )
take v = v; :: thesis: ( [a,b] = [u,w] & [b,c] = [y,v] & b1,b2 // b3,b4 )
thus ( [a,b] = [u,w] & [b,c] = [y,v] ) by A16, A17; :: thesis: b1,b2 // b3,b4
A22: w - ((1 - l) * u) = ((l * v) + ((1 - l) * u)) + (((- 1) * (1 - l)) * u) by A19, RVSUM_1:49
.= (l * v) + (((1 - l) * u) + ((- (1 - l)) * u)) by RVSUM_1:15
.= (l * v) + (((1 - l) + (- (1 - l))) * u) by RVSUM_1:50
.= l * v by THJE ;
|[(l * (v `1)),(l * (v `2))]| = l * v by EUCLID:57
.= |[(w `1),(w `2)]| - ((1 - l) * u) by A22, EUCLID:53
.= |[(w `1),(w `2)]| - |[((1 - l) * (u `1)),((1 - l) * (u `2))]| by EUCLID:57
.= |[((w `1) - ((1 - l) * (u `1))),((w `2) - ((1 - l) * (u `2)))]| by EUCLID:62 ;
then A23: ( l * (v `1) = (w `1) - ((1 - l) * (u `1)) & l * (v `2) = (w `2) - ((1 - l) * (u `2)) ) by FINSEQ_1:77;
A24: ((1 - l) * w) - ((1 - l) * u) = (l * v) - (l * w)
proof
A25: ((1 - l) * w) - ((1 - l) * u) = ((1 - l) * |[(w `1),(w `2)]|) - ((1 - l) * u) by EUCLID:53
.= ((1 - l) * |[(w `1),(w `2)]|) - ((1 - l) * |[(u `1),(u `2)]|) by EUCLID:53
.= |[((1 - l) * (w `1)),((1 - l) * (w `2))]| - ((1 - l) * |[(u `1),(u `2)]|) by EUCLID:58
.= |[((1 - l) * (w `1)),((1 - l) * (w `2))]| - |[((1 - l) * (u `1)),((1 - l) * (u `2))]| by EUCLID:58
.= |[(((1 - l) * (w `1)) - ((1 - l) * (u `1))),(((1 - l) * (w `2)) - ((1 - l) * (u `2)))]| by EUCLID:62
.= |[((l * (v `1)) - (l * (w `1))),((l * (v `2)) - (l * (w `2)))]| by A23 ;
(l * v) - (l * w) = (l * |[(v `1),(v `2)]|) - (l * w) by EUCLID:53
.= (l * |[(v `1),(v `2)]|) - (l * |[(w `1),(w `2)]|) by EUCLID:53
.= |[(l * (v `1)),(l * (v `2))]| - (l * |[(w `1),(w `2)]|) by EUCLID:58
.= |[(l * (v `1)),(l * (v `2))]| - |[(l * (w `1)),(l * (w `2))]| by EUCLID:58
.= |[((l * (v `1)) - (l * (w `1))),((l * (v `2)) - (l * (w `2)))]| by EUCLID:62 ;
hence ((1 - l) * w) - ((1 - l) * u) = (l * v) - (l * w) by A25; :: thesis: verum
end;
A26: (1 - l) * (w - u) = ((1 - l) * w) + ((1 - l) * (- u)) by RVSUM_1:51
.= ((1 - l) * w) + (((1 - l) * (- 1)) * u) by RVSUM_1:49
.= ((1 - l) * w) - ((1 - l) * u) by RVSUM_1:49
.= (l * v) + (((- 1) * l) * w) by A24, RVSUM_1:49
.= (l * v) + (l * ((- 1) * w)) by RVSUM_1:49
.= l * (v - w) by RVSUM_1:51 ;
per cases ( l = 1 or l = 0 or ( 0 < l & l < 1 ) ) by A20, A21, XXREAL_0:1;
suppose l = 1 ; :: thesis: b1,b2 // b3,b4
then w = v + (0 * u) by A19, RVSUM_1:52
.= v by THJE ;
hence u,w // y,v ; :: thesis: verum
end;
suppose l = 0 ; :: thesis: b1,b2 // b3,b4
then w = u + (0 * v) by A19, RVSUM_1:52
.= u by THJE ;
hence u,w // y,v ; :: thesis: verum
end;
suppose A27: ( 0 < l & l < 1 ) ; :: thesis: b1,b2 // b3,b4
then l - l < 1 - l by XREAL_1:9;
hence u,w // y,v by A27, A26; :: thesis: verum
end;
end;
end;
then a,b // b,c by ANALOAF:def 3;
hence Mid a,b,c ; :: thesis: verum
end;
end;
end;
hence ( Mid a,b,c iff ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) ) by A1; :: thesis: verum