let a, b be Real; :: thesis: for p, q being Point of (REAL-NS 1)
for I being Function of REAL,(REAL-NS 1) st p = <*a*> & q = <*b*> & I = (proj (1,1)) " holds
( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )
let p, q be Point of (REAL-NS 1); :: thesis: for I being Function of REAL,(REAL-NS 1) st p = <*a*> & q = <*b*> & I = (proj (1,1)) " holds
( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )
let I be Function of REAL,(REAL-NS 1); :: thesis: ( p = <*a*> & q = <*b*> & I = (proj (1,1)) " implies ( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) ) )
assume that
A1: ( p = <*a*> & q = <*b*> ) and
A2: I = (proj (1,1)) " ; :: thesis: ( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )
hereby :: thesis: ( a < b implies I .: ].a,b.[ = ].p,q.[ )
assume X1: a <= b ; :: thesis: I .: [.a,b.] = [.p,q.]
now :: thesis: for y being object st y in I .: [.a,b.] holds
y in [.p,q.]
let y be object ; :: thesis: ( y in I .: [.a,b.] implies y in [.p,q.] )
assume y in I .: [.a,b.] ; :: thesis: y in [.p,q.]
then consider x being object such that
A3: ( x in dom I & [x,y] in I & x in [.a,b.] ) by RELAT_1:110;
reconsider x = x as Element of REAL by A3;
I . x = <*x*> by A2, PDIFF_1:1;
then I . x in [.p,q.] by A1, A3, LM519C1;
hence y in [.p,q.] by A3, FUNCT_1:1; :: thesis: verum
end;
then A6: I .: [.a,b.] c= [.p,q.] ;
reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;
A7: ( J . p = a & J . q = b ) by A1, PDIFF_1:1;
now :: thesis: for x being object st x in [.p,q.] holds
x in I .: [.a,b.]
let x be object ; :: thesis: ( x in [.p,q.] implies x in I .: [.a,b.] )
assume B0: x in [.p,q.] ; :: thesis: x in I .: [.a,b.]
then x in { (((1 - r) * p) + (r * q)) where r is Real : ( 0 <= r & r <= 1 ) } by RLTOPSP1:def 2;
then consider r being Real such that
B2: ( x = ((1 - r) * p) + (r * q) & 0 <= r & r <= 1 ) ;
J . x = (J . ((1 - r) * p)) + (J . (r * q)) by B2, PDIFF_1:4
.= ((1 - r) * (J . p)) + (J . (r * q)) by PDIFF_1:4
.= ((1 - r) * (J . p)) + (r * (J . q)) by PDIFF_1:4 ;
then ( a <= J . x & J . x <= b ) by A7, X1, XREAL_1:171, XREAL_1:172, B2;
then B5: J . x in [.a,b.] ;
then reconsider z = J . x as Element of REAL ;
set z1 = I . z;
[z,(I . z)] in I by A2, PDIFF_1:2, FUNCT_1:1;
then B9: I . z in I .: [.a,b.] by B5, A2, PDIFF_1:2, RELAT_1:110;
I * J = id (rng I) by PDIFF_1:2, A2, Lm2, FUNCT_1:39;
then J = I " by A2, PDIFF_1:2, Lm2, FUNCT_1:42;
hence x in I .: [.a,b.] by B9, FUNCT_1:35, Lm1, A2, PDIFF_1:2, B0; :: thesis: verum
end;
then [.p,q.] c= I .: [.a,b.] ;
hence I .: [.a,b.] = [.p,q.] by A6, XBOOLE_0:def 10; :: thesis: verum
end;
assume X2: a < b ; :: thesis: I .: ].a,b.[ = ].p,q.[
now :: thesis: for y being object st y in I .: ].a,b.[ holds
y in ].p,q.[
let y be object ; :: thesis: ( y in I .: ].a,b.[ implies y in ].p,q.[ )
assume y in I .: ].a,b.[ ; :: thesis: y in ].p,q.[
then consider x being object such that
B3: ( x in dom I & [x,y] in I & x in ].a,b.[ ) by RELAT_1:110;
reconsider x = x as Element of REAL by B3;
I . x = <*x*> by A2, PDIFF_1:1;
then I . x in ].p,q.[ by A1, B3, LM519B1;
hence y in ].p,q.[ by B3, FUNCT_1:1; :: thesis: verum
end;
then B6: I .: ].a,b.[ c= ].p,q.[ ;
reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;
A7: ( J . p = a & J . q = b ) by A1, PDIFF_1:1;
now :: thesis: for x being object st x in ].p,q.[ holds
x in I .: ].a,b.[
let x be object ; :: thesis: ( x in ].p,q.[ implies x in I .: ].a,b.[ )
assume B0: x in ].p,q.[ ; :: thesis: x in I .: ].a,b.[
then B0c: ( x in [.p,q.] & not x in {p,q} ) by XBOOLE_0:def 5;
then B0b: ( x <> p & x <> q ) by TARSKI:def 2;
x in { (((1 - r) * p) + (r * q)) where r is Real : ( 0 <= r & r <= 1 ) } by B0c, RLTOPSP1:def 2;
then consider r being Real such that
B1: ( x = ((1 - r) * p) + (r * q) & 0 <= r & r <= 1 ) ;
now :: thesis: not r = 1
assume r = 1 ; :: thesis: contradiction
then x = (0. (REAL-NS 1)) + (1 * q) by B1, RLVECT_1:10;
hence contradiction by B0b, RLVECT_1:def 8; :: thesis: verum
end;
then B1a: r < 1 by B1, XXREAL_0:1;
B1b: now :: thesis: not r = 0
assume r = 0 ; :: thesis: contradiction
then x = (1 * p) + (0. (REAL-NS 1)) by B1, RLVECT_1:10;
hence contradiction by B0b, RLVECT_1:def 8; :: thesis: verum
end;
J . x = (J . ((1 - r) * p)) + (J . (r * q)) by B1, PDIFF_1:4
.= ((1 - r) * (J . p)) + (J . (r * q)) by PDIFF_1:4
.= ((1 - r) * (J . p)) + (r * (J . q)) by PDIFF_1:4 ;
then ( a < J . x & J . x < b ) by A7, X2, XREAL_1:177, XREAL_1:178, B1a, B1, B1b;
then B5: J . x in ].a,b.[ ;
then reconsider z = J . x as Element of REAL ;
set z1 = I . z;
B91: [z,(I . z)] in I by A2, PDIFF_1:2, FUNCT_1:1;
B11: rng I = the carrier of (REAL-NS 1) by A2, REAL_NS1:def 4, PDIFF_1:2;
I * J = id (rng I) by PDIFF_1:2, A2, Lm2, FUNCT_1:39;
then B14: J = I " by A2, PDIFF_1:2, Lm2, FUNCT_1:42;
x = I . (J . x) by A2, B14, FUNCT_1:35, B11, B0;
hence x in I .: ].a,b.[ by B91, B5, A2, PDIFF_1:2, RELAT_1:110; :: thesis: verum
end;
then ].p,q.[ c= I .: ].a,b.[ ;
hence I .: ].a,b.[ = ].p,q.[ by B6, XBOOLE_0:def 10; :: thesis: verum