:: TOPMETR2 semantic presentation
begin
theorem :: TOPMETR2:1
for f, g being Function st f is one-to-one & g is one-to-one & ( for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds
g . x1 <> f . x2 ) holds
f +* g is one-to-one
proof
let f, g be Function; ::_thesis: ( f is one-to-one & g is one-to-one & ( for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds
g . x1 <> f . x2 ) implies f +* g is one-to-one )
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds
g . x1 <> f . x2 ; ::_thesis: f +* g is one-to-one
now__::_thesis:_for_x11,_x22_being_set_st_x11_in_dom_(f_+*_g)_&_x22_in_dom_(f_+*_g)_&_(f_+*_g)_._x11_=_(f_+*_g)_._x22_holds_
x11_=_x22
let x11, x22 be set ; ::_thesis: ( x11 in dom (f +* g) & x22 in dom (f +* g) & (f +* g) . x11 = (f +* g) . x22 implies x11 = x22 )
assume that
A4: x11 in dom (f +* g) and
A5: x22 in dom (f +* g) and
A6: (f +* g) . x11 = (f +* g) . x22 ; ::_thesis: x11 = x22
A7: x22 in (dom f) \/ (dom g) by A5, FUNCT_4:def_1;
then A8: x22 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;
A9: x11 in (dom f) \/ (dom g) by A4, FUNCT_4:def_1;
then A10: x11 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;
now__::_thesis:_x11_=_x22
percases ( x11 in (dom f) \ (dom g) or x11 in dom g ) by A10, XBOOLE_0:def_3;
supposeA11: x11 in (dom f) \ (dom g) ; ::_thesis: x11 = x22
then not x11 in dom g by XBOOLE_0:def_5;
then A12: (f +* g) . x11 = f . x11 by A9, FUNCT_4:def_1;
now__::_thesis:_(_(_x22_in_(dom_f)_\_(dom_g)_&_x11_=_x22_)_or_(_x22_in_dom_g_&_contradiction_)_)
percases ( x22 in (dom f) \ (dom g) or x22 in dom g ) by A8, XBOOLE_0:def_3;
caseA13: x22 in (dom f) \ (dom g) ; ::_thesis: x11 = x22
then not x22 in dom g by XBOOLE_0:def_5;
then f . x11 = f . x22 by A6, A7, A12, FUNCT_4:def_1;
hence x11 = x22 by A1, A11, A13, FUNCT_1:def_4; ::_thesis: verum
end;
caseA14: x22 in dom g ; ::_thesis: contradiction
then g . x22 <> f . x11 by A3, A11;
hence contradiction by A6, A7, A12, A14, FUNCT_4:def_1; ::_thesis: verum
end;
end;
end;
hence x11 = x22 ; ::_thesis: verum
end;
supposeA15: x11 in dom g ; ::_thesis: x11 = x22
now__::_thesis:_(_(_x22_in_(dom_f)_\_(dom_g)_&_contradiction_)_or_(_x22_in_dom_g_&_x11_=_x22_)_)
percases ( x22 in (dom f) \ (dom g) or x22 in dom g ) by A8, XBOOLE_0:def_3;
caseA16: x22 in (dom f) \ (dom g) ; ::_thesis: contradiction
then not x22 in dom g by XBOOLE_0:def_5;
then A17: (f +* g) . x22 = f . x22 by A7, FUNCT_4:def_1;
g . x11 <> f . x22 by A3, A15, A16;
hence contradiction by A6, A9, A15, A17, FUNCT_4:def_1; ::_thesis: verum
end;
caseA18: x22 in dom g ; ::_thesis: x11 = x22
then (f +* g) . x22 = g . x22 by A7, FUNCT_4:def_1;
then g . x11 = g . x22 by A6, A9, A15, FUNCT_4:def_1;
hence x11 = x22 by A2, A15, A18, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
hence x11 = x22 ; ::_thesis: verum
end;
end;
end;
hence x11 = x22 ; ::_thesis: verum
end;
hence f +* g is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;
Lm1: for f, g being Function st f .: ((dom f) /\ (dom g)) c= rng g holds
(rng f) \ (rng g) c= rng (f +* g)
proof
let f, g be Function; ::_thesis: ( f .: ((dom f) /\ (dom g)) c= rng g implies (rng f) \ (rng g) c= rng (f +* g) )
assume A1: f .: ((dom f) /\ (dom g)) c= rng g ; ::_thesis: (rng f) \ (rng g) c= rng (f +* g)
let y1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not y1 in (rng f) \ (rng g) or y1 in rng (f +* g) )
assume A2: y1 in (rng f) \ (rng g) ; ::_thesis: y1 in rng (f +* g)
then consider x1 being set such that
A3: x1 in dom f and
A4: y1 = f . x1 by FUNCT_1:def_3;
A5: x1 in (dom f) \/ (dom g) by A3, XBOOLE_0:def_3;
then A6: x1 in dom (f +* g) by FUNCT_4:def_1;
now__::_thesis:_not_x1_in_dom_g
assume x1 in dom g ; ::_thesis: contradiction
then x1 in (dom f) /\ (dom g) by A3, XBOOLE_0:def_4;
then f . x1 in f .: ((dom f) /\ (dom g)) by A3, FUNCT_1:def_6;
hence contradiction by A1, A2, A4, XBOOLE_0:def_5; ::_thesis: verum
end;
then (f +* g) . x1 = f . x1 by A5, FUNCT_4:def_1;
hence y1 in rng (f +* g) by A4, A6, FUNCT_1:def_3; ::_thesis: verum
end;
theorem :: TOPMETR2:2
for f, g being Function st f .: ((dom f) /\ (dom g)) c= rng g holds
(rng f) \/ (rng g) = rng (f +* g)
proof
let f, g be Function; ::_thesis: ( f .: ((dom f) /\ (dom g)) c= rng g implies (rng f) \/ (rng g) = rng (f +* g) )
assume f .: ((dom f) /\ (dom g)) c= rng g ; ::_thesis: (rng f) \/ (rng g) = rng (f +* g)
then A1: (rng f) \ (rng g) c= rng (f +* g) by Lm1;
rng g c= rng (f +* g) by FUNCT_4:18;
then ((rng f) \ (rng g)) \/ (rng g) c= rng (f +* g) by A1, XBOOLE_1:8;
then A2: (rng f) \/ (rng g) c= rng (f +* g) by XBOOLE_1:39;
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
hence (rng f) \/ (rng g) = rng (f +* g) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TOPMETR2:3
for T being T_2 TopSpace
for P, Q being Subset of T
for p being Point of T
for f being Function of I[01],(T | P)
for g being Function of I[01],(T | Q) st P /\ Q = {p} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds
ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
proof
let T be T_2 TopSpace; ::_thesis: for P, Q being Subset of T
for p being Point of T
for f being Function of I[01],(T | P)
for g being Function of I[01],(T | Q) st P /\ Q = {p} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds
ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
1 / 2 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then reconsider pp = 1 / 2 as Point of I[01] by BORSUK_1:40, RCOMP_1:def_1;
reconsider PP = [.0,(1 / 2).] as Subset of R^1 by TOPMETR:17;
A1: 1 / 2 in [.0,1.] by XXREAL_1:1;
1 in [.0,1.] by XXREAL_1:1;
then [.(1 / 2),1.] c= the carrier of I[01] by A1, BORSUK_1:40, XXREAL_2:def_12;
then A2: the carrier of (Closed-Interval-TSpace ((1 / 2),1)) c= the carrier of I[01] by TOPMETR:18;
0 in [.0,1.] by XXREAL_1:1;
then [.0,(1 / 2).] c= the carrier of I[01] by A1, BORSUK_1:40, XXREAL_2:def_12;
then the carrier of (Closed-Interval-TSpace (0,(1 / 2))) c= the carrier of I[01] by TOPMETR:18;
then reconsider T1 = Closed-Interval-TSpace (0,(1 / 2)), T2 = Closed-Interval-TSpace ((1 / 2),1) as SubSpace of I[01] by A2, TOPMETR:3;
deffunc H1( Element of REAL ) -> Element of REAL = 2 * $1;
let P, Q be Subset of T; ::_thesis: for p being Point of T
for f being Function of I[01],(T | P)
for g being Function of I[01],(T | Q) st P /\ Q = {p} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds
ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
let p be Point of T; ::_thesis: for f being Function of I[01],(T | P)
for g being Function of I[01],(T | Q) st P /\ Q = {p} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds
ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
let f be Function of I[01],(T | P); ::_thesis: for g being Function of I[01],(T | Q) st P /\ Q = {p} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds
ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
let g be Function of I[01],(T | Q); ::_thesis: ( P /\ Q = {p} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p implies ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 ) )
assume that
A3: P /\ Q = {p} and
A4: f is being_homeomorphism and
A5: f . 1 = p and
A6: g is being_homeomorphism and
A7: g . 0 = p ; ::_thesis: ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
Q = [#] (T | Q) by PRE_TOPC:def_5;
then A8: rng g = Q by A6, TOPS_2:def_5;
p in P /\ Q by A3, TARSKI:def_1;
then reconsider M = T as non empty TopSpace ;
reconsider P9 = P, Q9 = Q as non empty Subset of M by A3;
reconsider R = P9 \/ Q9 as non empty Subset of M ;
A9: M | P9 is SubSpace of M | R by TOPMETR:4;
defpred S1[ set , set ] means for a being Real st a = $1 holds
$2 = f . (2 * a);
consider f3 being Function of REAL,REAL such that
A10: for x being Real holds f3 . x = H1(x) from FUNCT_2:sch_4();
A11: R = [#] (M | R) by PRE_TOPC:def_5
.= the carrier of (M | R) ;
then dom g = the carrier of I[01] by FUNCT_2:def_1;
then reconsider g9 = g as Function of I[01],(M | R) by A8, A11, RELSET_1:4, XBOOLE_1:7;
A12: M | Q9 is SubSpace of M | R by TOPMETR:4;
g is continuous by A6, TOPS_2:def_5;
then A13: g9 is continuous by A12, PRE_TOPC:26;
reconsider PP = PP as non empty Subset of R^1 by XXREAL_1:1;
A14: ( T1 is compact & T2 is compact ) by HEINE:4;
P = [#] (T | P) by PRE_TOPC:def_5;
then A15: rng f = P by A4, TOPS_2:def_5;
dom f = the carrier of I[01] by A11, FUNCT_2:def_1;
then reconsider ff = f as Function of I[01],(M | R) by A15, A11, RELSET_1:4, XBOOLE_1:7;
f is continuous by A4, TOPS_2:def_5;
then A16: ff is continuous by A9, PRE_TOPC:26;
reconsider f3 = f3 as Function of R^1,R^1 by TOPMETR:17;
A17: dom (f3 | [.0,(1 / 2).]) = (dom f3) /\ [.0,(1 / 2).] by RELAT_1:61
.= REAL /\ [.0,(1 / 2).] by FUNCT_2:def_1
.= [.0,(1 / 2).] by XBOOLE_1:28
.= the carrier of T1 by TOPMETR:18 ;
rng (f3 | [.0,(1 / 2).]) c= the carrier of R^1 ;
then reconsider f39 = f3 | PP as Function of T1,R^1 by A17, FUNCT_2:def_1, RELSET_1:4;
A18: dom f39 = the carrier of T1 by FUNCT_2:def_1;
rng f39 c= the carrier of I[01]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f39 or y in the carrier of I[01] )
assume y in rng f39 ; ::_thesis: y in the carrier of I[01]
then consider x being set such that
A19: x in dom f39 and
A20: y = f39 . x by FUNCT_1:def_3;
x in [.0,(1 / 2).] by A18, A19, TOPMETR:18;
then x in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by RCOMP_1:def_1;
then consider r being Real such that
A21: x = r and
A22: ( 0 <= r & r <= 1 / 2 ) ;
A23: ( 2 * 0 <= 2 * r & 2 * r <= 2 * (1 / 2) ) by A22, XREAL_1:64;
y = f3 . x by A19, A20, FUNCT_1:47
.= 2 * r by A10, A21 ;
then y in { rr where rr is Real : ( 0 <= rr & rr <= 1 ) } by A23;
hence y in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def_1; ::_thesis: verum
end;
then reconsider f4 = f39 as Function of T1,I[01] by A18, RELSET_1:4;
A24: R^1 | PP = T1 by TOPMETR:19;
for x being Real holds f3 . x = (2 * x) + 0 by A10;
then f39 is continuous by A24, TOPMETR:7, TOPMETR:21;
then A25: f4 is continuous by PRE_TOPC:27;
reconsider PP = [.(1 / 2),1.] as Subset of R^1 by TOPMETR:17;
reconsider PP = PP as non empty Subset of R^1 by XXREAL_1:1;
deffunc H2( Element of REAL ) -> Element of REAL = (2 * $1) - 1;
consider g3 being Function of REAL,REAL such that
A26: for x being Real holds g3 . x = H2(x) from FUNCT_2:sch_4();
reconsider g3 = g3 as Function of R^1,R^1 by TOPMETR:17;
A27: dom (g3 | [.(1 / 2),1.]) = (dom g3) /\ [.(1 / 2),1.] by RELAT_1:61
.= REAL /\ [.(1 / 2),1.] by FUNCT_2:def_1
.= [.(1 / 2),1.] by XBOOLE_1:28
.= the carrier of T2 by TOPMETR:18 ;
rng (g3 | [.(1 / 2),1.]) c= the carrier of R^1 ;
then reconsider g39 = g3 | PP as Function of T2,R^1 by A27, FUNCT_2:def_1, RELSET_1:4;
A28: dom g39 = the carrier of T2 by FUNCT_2:def_1;
rng g39 c= the carrier of I[01]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g39 or y in the carrier of I[01] )
assume y in rng g39 ; ::_thesis: y in the carrier of I[01]
then consider x being set such that
A29: x in dom g39 and
A30: y = g39 . x by FUNCT_1:def_3;
x in [.(1 / 2),1.] by A28, A29, TOPMETR:18;
then x in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by RCOMP_1:def_1;
then consider r being Real such that
A31: x = r and
A32: 1 / 2 <= r and
A33: r <= 1 ;
2 * (1 / 2) <= 2 * r by A32, XREAL_1:64;
then A34: 1 - 1 <= (2 * r) - 1 by XREAL_1:9;
2 * r <= 2 * 1 by A33, XREAL_1:64;
then A35: (2 * r) - 1 <= (1 + 1) - 1 by XREAL_1:9;
y = g3 . x by A29, A30, FUNCT_1:47
.= (2 * r) - 1 by A26, A31 ;
then y in { rr where rr is Real : ( 0 <= rr & rr <= 1 ) } by A34, A35;
hence y in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def_1; ::_thesis: verum
end;
then reconsider g4 = g39 as Function of T2,I[01] by A28, RELSET_1:4;
( [#] T1 = [.0,(1 / 2).] & [#] T2 = [.(1 / 2),1.] ) by TOPMETR:18;
then A36: ( ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pp} ) by BORSUK_1:40, XXREAL_1:165, XXREAL_1:418;
A37: for x being Real holds g3 . x = (2 * x) + (- 1)
proof
let x be Real; ::_thesis: g3 . x = (2 * x) + (- 1)
thus g3 . x = (2 * x) - 1 by A26
.= (2 * x) + (- 1) ; ::_thesis: verum
end;
R^1 | PP = T2 by TOPMETR:19;
then g39 is continuous by A37, TOPMETR:7, TOPMETR:21;
then A38: g4 is continuous by PRE_TOPC:27;
A39: for x being set st x in [.0,(1 / 2).] holds
ex u being set st S1[x,u]
proof
let x be set ; ::_thesis: ( x in [.0,(1 / 2).] implies ex u being set st S1[x,u] )
assume x in [.0,(1 / 2).] ; ::_thesis: ex u being set st S1[x,u]
then x in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by RCOMP_1:def_1;
then consider r being Real such that
A40: r = x and
0 <= r and
r <= 1 / 2 ;
take f . (2 * r) ; ::_thesis: S1[x,f . (2 * r)]
thus S1[x,f . (2 * r)] by A40; ::_thesis: verum
end;
consider f2 being Function such that
A41: dom f2 = [.0,(1 / 2).] and
A42: for x being set st x in [.0,(1 / 2).] holds
S1[x,f2 . x] from CLASSES1:sch_1(A39);
A43: dom f2 = the carrier of T1 by A41, TOPMETR:18;
f is Function of the carrier of I[01], the carrier of (M | P9) ;
then A44: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def_1;
now__::_thesis:_for_y_being_set_st_y_in_rng_f2_holds_
y_in_P
let y be set ; ::_thesis: ( y in rng f2 implies y in P )
assume y in rng f2 ; ::_thesis: y in P
then consider x being set such that
A45: x in dom f2 and
A46: y = f2 . x by FUNCT_1:def_3;
x in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by A41, A45, RCOMP_1:def_1;
then consider a being Real such that
A47: x = a and
A48: ( 0 <= a & a <= 1 / 2 ) ;
( 0 <= 2 * a & 2 * a <= 2 * (1 / 2) ) by A48, XREAL_1:64, XREAL_1:127;
then 2 * a in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then A49: 2 * a in dom f by A44, RCOMP_1:def_1;
y = f . (2 * a) by A41, A42, A45, A46, A47;
hence y in P by A15, A49, FUNCT_1:def_3; ::_thesis: verum
end;
then A50: rng f2 c= P by TARSKI:def_3;
P c= P \/ Q by XBOOLE_1:7;
then rng f2 c= the carrier of (T | (P \/ Q)) by A11, A50, XBOOLE_1:1;
then reconsider f1 = f2 as Function of T1,(M | R) by A43, FUNCT_2:def_1, RELSET_1:4;
for x being set st x in the carrier of T1 holds
f1 . x = (ff * f4) . x
proof
let x be set ; ::_thesis: ( x in the carrier of T1 implies f1 . x = (ff * f4) . x )
assume A51: x in the carrier of T1 ; ::_thesis: f1 . x = (ff * f4) . x
the carrier of T1 = [.0,(1 / 2).] by TOPMETR:18;
then reconsider x9 = x as Real by A51;
the carrier of T1 = [.0,(1 / 2).] by TOPMETR:18;
hence f1 . x = f . (2 * x9) by A42, A51
.= f . (f3 . x9) by A10
.= f . (f4 . x) by A17, A51, FUNCT_1:47
.= (ff * f4) . x by A51, FUNCT_2:15 ;
::_thesis: verum
end;
then A52: f1 is continuous by A25, A16, FUNCT_2:12;
A53: now__::_thesis:_for_x_being_Real_st_x_in_dom_f2_holds_
2_*_x_in_dom_f
let x be Real; ::_thesis: ( x in dom f2 implies 2 * x in dom f )
assume x in dom f2 ; ::_thesis: 2 * x in dom f
then x in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by A41, RCOMP_1:def_1;
then consider a being Real such that
A54: a = x and
A55: ( 0 <= a & a <= 1 / 2 ) ;
( 0 <= 2 * a & 2 * a <= 2 * (1 / 2) ) by A55, XREAL_1:64, XREAL_1:127;
then 2 * a in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
hence 2 * x in dom f by A44, A54, RCOMP_1:def_1; ::_thesis: verum
end;
defpred S2[ set , set ] means for a being Real st a = $1 holds
$2 = g . ((2 * a) - 1);
A56: for x being set st x in [.(1 / 2),1.] holds
ex u being set st S2[x,u]
proof
let x be set ; ::_thesis: ( x in [.(1 / 2),1.] implies ex u being set st S2[x,u] )
assume x in [.(1 / 2),1.] ; ::_thesis: ex u being set st S2[x,u]
then x in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by RCOMP_1:def_1;
then consider r being Real such that
A57: r = x and
1 / 2 <= r and
r <= 1 ;
take g . ((2 * r) - 1) ; ::_thesis: S2[x,g . ((2 * r) - 1)]
thus S2[x,g . ((2 * r) - 1)] by A57; ::_thesis: verum
end;
consider g2 being Function such that
A58: dom g2 = [.(1 / 2),1.] and
A59: for x being set st x in [.(1 / 2),1.] holds
S2[x,g2 . x] from CLASSES1:sch_1(A56);
A60: dom g2 = the carrier of T2 by A58, TOPMETR:18;
g is Function of the carrier of I[01], the carrier of (M | Q9) ;
then A61: dom g = [.0,1.] by BORSUK_1:40, FUNCT_2:def_1;
now__::_thesis:_for_y_being_set_st_y_in_rng_g2_holds_
y_in_Q
let y be set ; ::_thesis: ( y in rng g2 implies y in Q )
assume y in rng g2 ; ::_thesis: y in Q
then consider x being set such that
A62: x in dom g2 and
A63: y = g2 . x by FUNCT_1:def_3;
x in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A58, A62, RCOMP_1:def_1;
then consider a being Real such that
A64: x = a and
A65: 1 / 2 <= a and
A66: a <= 1 ;
2 * a <= 2 * 1 by A66, XREAL_1:64;
then A67: (2 * a) - 1 <= (1 + 1) - 1 by XREAL_1:9;
2 * (1 / 2) = 1 ;
then 1 <= 2 * a by A65, XREAL_1:64;
then 1 - 1 <= (2 * a) - 1 by XREAL_1:9;
then (2 * a) - 1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A67;
then A68: (2 * a) - 1 in dom g by A61, RCOMP_1:def_1;
y = g . ((2 * a) - 1) by A58, A59, A62, A63, A64;
hence y in Q by A8, A68, FUNCT_1:def_3; ::_thesis: verum
end;
then A69: rng g2 c= Q by TARSKI:def_3;
A70: Q c= rng g2
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Q or a in rng g2 )
assume a in Q ; ::_thesis: a in rng g2
then consider x being set such that
A71: x in dom g and
A72: a = g . x by A8, FUNCT_1:def_3;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A61, A71, RCOMP_1:def_1;
then consider x9 being Real such that
A73: x9 = x and
A74: 0 <= x9 and
A75: x9 <= 1 ;
x9 + 1 <= 1 + 1 by A75, XREAL_1:6;
then A76: (x9 + 1) / 2 <= 2 / 2 by XREAL_1:72;
0 + 1 <= x9 + 1 by A74, XREAL_1:6;
then 1 / 2 <= (x9 + 1) / 2 by XREAL_1:72;
then (x9 + 1) / 2 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by A76;
then A77: (x9 + 1) / 2 in dom g2 by A58, RCOMP_1:def_1;
a = g . ((2 * ((x9 + 1) / 2)) - 1) by A72, A73
.= g2 . ((x9 + 1) / 2) by A58, A59, A77 ;
hence a in rng g2 by A77, FUNCT_1:def_3; ::_thesis: verum
end;
TopSpaceMetr RealSpace is T_2 by PCOMPS_1:34;
then A78: I[01] is T_2 by TOPMETR:2, TOPMETR:def_6;
A79: 1 / 2 in [.(1 / 2),1.] by XXREAL_1:1;
A80: now__::_thesis:_for_x_being_Real_st_x_in_dom_g2_holds_
(2_*_x)_-_1_in_dom_g
let x be Real; ::_thesis: ( x in dom g2 implies (2 * x) - 1 in dom g )
assume x in dom g2 ; ::_thesis: (2 * x) - 1 in dom g
then x in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A58, RCOMP_1:def_1;
then consider a being Real such that
A81: a = x and
A82: 1 / 2 <= a and
A83: a <= 1 ;
2 * a <= 2 * 1 by A83, XREAL_1:64;
then A84: (2 * a) - 1 <= (1 + 1) - 1 by XREAL_1:9;
2 * (1 / 2) = 1 ;
then 1 <= 2 * a by A82, XREAL_1:64;
then 1 - 1 <= (2 * a) - 1 by XREAL_1:9;
then (2 * a) - 1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A84;
hence (2 * x) - 1 in dom g by A61, A81, RCOMP_1:def_1; ::_thesis: verum
end;
Q c= P \/ Q by XBOOLE_1:7;
then rng g2 c= the carrier of (M | R) by A11, A69, XBOOLE_1:1;
then reconsider g1 = g2 as Function of T2,(M | R) by A60, FUNCT_2:def_1, RELSET_1:4;
for x being set st x in the carrier of T2 holds
g1 . x = (g9 * g4) . x
proof
let x be set ; ::_thesis: ( x in the carrier of T2 implies g1 . x = (g9 * g4) . x )
assume A85: x in the carrier of T2 ; ::_thesis: g1 . x = (g9 * g4) . x
the carrier of T2 = [.(1 / 2),1.] by TOPMETR:18;
then reconsider x9 = x as Real by A85;
the carrier of T2 = [.(1 / 2),1.] by TOPMETR:18;
hence g1 . x = g . ((2 * x9) - 1) by A59, A85
.= g . (g3 . x9) by A26
.= g . (g4 . x) by A27, A85, FUNCT_1:47
.= (g9 * g4) . x by A85, FUNCT_2:15 ;
::_thesis: verum
end;
then A86: g1 is continuous by A38, A13, FUNCT_2:12;
1 / 2 in [.0,(1 / 2).] by XXREAL_1:1;
then f1 . pp = g . ((2 * (1 / 2)) - 1) by A5, A7, A42
.= g1 . pp by A59, A79 ;
then reconsider h = f2 +* g2 as continuous Function of I[01],(M | R) by A36, A14, A78, A52, A86, COMPTS_1:20;
A87: g is one-to-one by A6, TOPS_2:def_5;
A88: f is one-to-one by A4, TOPS_2:def_5;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_h_&_x2_in_dom_h_&_h_._x1_=_h_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 implies x1 = x2 )
assume that
A89: x1 in dom h and
A90: x2 in dom h and
A91: h . x1 = h . x2 ; ::_thesis: x1 = x2
now__::_thesis:_x1_=_x2
percases ( ( not x1 in dom g2 & not x2 in dom g2 ) or ( not x1 in dom g2 & x2 in dom g2 ) or ( x1 in dom g2 & not x2 in dom g2 ) or ( x1 in dom g2 & x2 in dom g2 ) ) ;
supposeA92: ( not x1 in dom g2 & not x2 in dom g2 ) ; ::_thesis: x1 = x2
A93: dom h = (dom f2) \/ (dom g2) by FUNCT_4:def_1;
then x1 in [.0,(1 / 2).] by A41, A89, A92, XBOOLE_0:def_3;
then x1 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by RCOMP_1:def_1;
then consider x19 being Real such that
A94: x19 = x1 and
0 <= x19 and
x19 <= 1 / 2 ;
A95: x1 in dom f2 by A89, A92, A93, XBOOLE_0:def_3;
then A96: 2 * x19 in dom f by A53, A94;
x2 in [.0,(1 / 2).] by A41, A90, A92, A93, XBOOLE_0:def_3;
then x2 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by RCOMP_1:def_1;
then consider x29 being Real such that
A97: x29 = x2 and
0 <= x29 and
x29 <= 1 / 2 ;
A98: x2 in dom f2 by A90, A92, A93, XBOOLE_0:def_3;
then A99: 2 * x29 in dom f by A53, A97;
f . (2 * x19) = f2 . x1 by A41, A42, A95, A94
.= h . x2 by A91, A92, FUNCT_4:11
.= f2 . x2 by A92, FUNCT_4:11
.= f . (2 * x29) by A41, A42, A98, A97 ;
then 2 * x19 = 2 * x29 by A88, A96, A99, FUNCT_1:def_4;
hence x1 = x2 by A94, A97; ::_thesis: verum
end;
supposeA100: ( not x1 in dom g2 & x2 in dom g2 ) ; ::_thesis: x1 = x2
dom h = (dom f2) \/ (dom g2) by FUNCT_4:def_1;
then A101: x1 in dom f2 by A89, A100, XBOOLE_0:def_3;
then x1 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by A41, RCOMP_1:def_1;
then consider x19 being Real such that
A102: x19 = x1 and
0 <= x19 and
x19 <= 1 / 2 ;
A103: 2 * x19 in dom f by A53, A101, A102;
then A104: f . (2 * x19) in P by A15, FUNCT_1:def_3;
x2 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A58, A100, RCOMP_1:def_1;
then consider x29 being Real such that
A105: x29 = x2 and
1 / 2 <= x29 and
x29 <= 1 ;
A106: (2 * x29) - 1 in dom g by A80, A100, A105;
then A107: g . ((2 * x29) - 1) in Q by A8, FUNCT_1:def_3;
A108: 1 in dom f by A44, XXREAL_1:1;
A109: 0 in dom g by A61, XXREAL_1:1;
A110: f . (2 * x19) = f2 . x1 by A41, A42, A101, A102
.= h . x2 by A91, A100, FUNCT_4:11
.= g2 . x2 by A100, FUNCT_4:13
.= g . ((2 * x29) - 1) by A58, A59, A100, A105 ;
then g . ((2 * x29) - 1) in P /\ Q by A104, A107, XBOOLE_0:def_4;
then g . ((2 * x29) - 1) = p by A3, TARSKI:def_1;
then A111: ((2 * x29) - 1) + 1 = 0 + 1 by A7, A87, A106, A109, FUNCT_1:def_4;
f . (2 * x19) in P /\ Q by A110, A104, A107, XBOOLE_0:def_4;
then f . (2 * x19) = p by A3, TARSKI:def_1;
then (1 / 2) * (2 * x19) = (1 / 2) * 1 by A5, A88, A103, A108, FUNCT_1:def_4;
hence x1 = x2 by A105, A102, A111; ::_thesis: verum
end;
supposeA112: ( x1 in dom g2 & not x2 in dom g2 ) ; ::_thesis: x1 = x2
dom h = (dom f2) \/ (dom g2) by FUNCT_4:def_1;
then A113: x2 in dom f2 by A90, A112, XBOOLE_0:def_3;
then x2 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by A41, RCOMP_1:def_1;
then consider x29 being Real such that
A114: x29 = x2 and
0 <= x29 and
x29 <= 1 / 2 ;
A115: 2 * x29 in dom f by A53, A113, A114;
then A116: f . (2 * x29) in P by A15, FUNCT_1:def_3;
x1 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A58, A112, RCOMP_1:def_1;
then consider x19 being Real such that
A117: x19 = x1 and
1 / 2 <= x19 and
x19 <= 1 ;
A118: (2 * x19) - 1 in dom g by A80, A112, A117;
then A119: g . ((2 * x19) - 1) in Q by A8, FUNCT_1:def_3;
A120: 1 in dom f by A44, XXREAL_1:1;
A121: 0 in dom g by A61, XXREAL_1:1;
A122: f . (2 * x29) = f2 . x2 by A41, A42, A113, A114
.= h . x1 by A91, A112, FUNCT_4:11
.= g2 . x1 by A112, FUNCT_4:13
.= g . ((2 * x19) - 1) by A58, A59, A112, A117 ;
then g . ((2 * x19) - 1) in P /\ Q by A116, A119, XBOOLE_0:def_4;
then g . ((2 * x19) - 1) = p by A3, TARSKI:def_1;
then A123: ((2 * x19) - 1) + 1 = 0 + 1 by A7, A87, A118, A121, FUNCT_1:def_4;
f . (2 * x29) in P /\ Q by A122, A116, A119, XBOOLE_0:def_4;
then f . (2 * x29) = p by A3, TARSKI:def_1;
then (1 / 2) * (2 * x29) = (1 / 2) * 1 by A5, A88, A115, A120, FUNCT_1:def_4;
hence x1 = x2 by A117, A114, A123; ::_thesis: verum
end;
supposeA124: ( x1 in dom g2 & x2 in dom g2 ) ; ::_thesis: x1 = x2
then x2 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A58, RCOMP_1:def_1;
then consider x29 being Real such that
A125: x29 = x2 and
1 / 2 <= x29 and
x29 <= 1 ;
A126: (2 * x29) - 1 in dom g by A80, A124, A125;
x1 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A58, A124, RCOMP_1:def_1;
then consider x19 being Real such that
A127: x19 = x1 and
1 / 2 <= x19 and
x19 <= 1 ;
A128: (2 * x19) - 1 in dom g by A80, A124, A127;
g . ((2 * x19) - 1) = g2 . x1 by A58, A59, A124, A127
.= h . x2 by A91, A124, FUNCT_4:13
.= g2 . x2 by A124, FUNCT_4:13
.= g . ((2 * x29) - 1) by A58, A59, A124, A125 ;
then ((2 * x19) - 1) + 1 = ((2 * x29) - 1) + 1 by A87, A128, A126, FUNCT_1:def_4;
hence x1 = x2 by A127, A125; ::_thesis: verum
end;
end;
end;
hence x1 = x2 ; ::_thesis: verum
end;
then A129: ( dom h = [#] I[01] & h is one-to-one ) by FUNCT_1:def_4, FUNCT_2:def_1;
reconsider h9 = h as Function of I[01],(T | (P \/ Q)) ;
take h9 ; ::_thesis: ( h9 is being_homeomorphism & h9 . 0 = f . 0 & h9 . 1 = g . 1 )
A130: 0 in [.0,(1 / 2).] by XXREAL_1:1;
A131: P c= rng f2
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in P or a in rng f2 )
assume a in P ; ::_thesis: a in rng f2
then consider x being set such that
A132: x in dom f and
A133: a = f . x by A15, FUNCT_1:def_3;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A44, A132, RCOMP_1:def_1;
then consider x9 being Real such that
A134: x9 = x and
A135: ( 0 <= x9 & x9 <= 1 ) ;
( 0 / 2 <= x9 / 2 & x9 / 2 <= 1 / 2 ) by A135, XREAL_1:72;
then x9 / 2 in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } ;
then A136: x9 / 2 in dom f2 by A41, RCOMP_1:def_1;
a = f . (2 * (x9 / 2)) by A133, A134
.= f2 . (x9 / 2) by A41, A42, A136 ;
hence a in rng f2 by A136, FUNCT_1:def_3; ::_thesis: verum
end;
A137: P c= rng h
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in P or a in rng h )
assume a in P ; ::_thesis: a in rng h
then consider x being set such that
A138: x in dom f2 and
A139: a = f2 . x by A131, FUNCT_1:def_3;
now__::_thesis:_a_in_rng_h
percases ( x in [.(1 / 2),1.] or not x in [.(1 / 2),1.] ) ;
supposeA140: x in [.(1 / 2),1.] ; ::_thesis: a in rng h
then x in [.0,(1 / 2).] /\ [.(1 / 2),1.] by A41, A138, XBOOLE_0:def_4;
then x in {(1 / 2)} by XXREAL_1:418;
then A141: x = 1 / 2 by TARSKI:def_1;
x in (dom f2) \/ (dom g2) by A138, XBOOLE_0:def_3;
then A142: x in dom h by FUNCT_4:def_1;
A143: 1 / 2 in [.0,(1 / 2).] by XXREAL_1:1;
h . x = g2 . x by A58, A140, FUNCT_4:13
.= g . ((2 * (1 / 2)) - 1) by A59, A140, A141
.= f2 . (1 / 2) by A5, A7, A42, A143 ;
hence a in rng h by A139, A141, A142, FUNCT_1:def_3; ::_thesis: verum
end;
supposeA144: not x in [.(1 / 2),1.] ; ::_thesis: a in rng h
A145: x in (dom f2) \/ (dom g2) by A138, XBOOLE_0:def_3;
then A146: x in dom h by FUNCT_4:def_1;
h . x = f2 . x by A58, A144, A145, FUNCT_4:def_1;
hence a in rng h by A139, A146, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence a in rng h ; ::_thesis: verum
end;
( rng h c= (rng f2) \/ (rng g2) & (rng f2) \/ (rng g2) c= P \/ Q ) by A50, A69, FUNCT_4:17, XBOOLE_1:13;
then A147: rng h c= P \/ Q by XBOOLE_1:1;
rng g2 c= rng h by FUNCT_4:18;
then Q c= rng h by A70, XBOOLE_1:1;
then P \/ Q c= rng h by A137, XBOOLE_1:8;
then rng h = P \/ Q by A147, XBOOLE_0:def_10;
then A148: rng h = [#] (M | R) by PRE_TOPC:def_5;
( I[01] is compact & M | R is T_2 ) by HEINE:4, TOPMETR:2, TOPMETR:20;
hence h9 is being_homeomorphism by A148, A129, COMPTS_1:17; ::_thesis: ( h9 . 0 = f . 0 & h9 . 1 = g . 1 )
not 0 in dom g2 by A58, XXREAL_1:1;
hence h9 . 0 = f2 . 0 by FUNCT_4:11
.= f . (2 * 0) by A42, A130
.= f . 0 ;
::_thesis: h9 . 1 = g . 1
A149: 1 in dom g2 by A58, XXREAL_1:1;
hence h9 . 1 = g2 . 1 by FUNCT_4:13
.= g . ((2 * 1) - 1) by A58, A59, A149
.= g . 1 ;
::_thesis: verum
end;