let T be non empty convex SubSpace of R^1 ; :: thesis: for P, Q being continuous Function of I[01] ,T holds R1Homotopy P,Q is continuous
let P, Q be continuous Function of I[01] ,T; :: thesis: R1Homotopy P,Q is continuous
set F = R1Homotopy P,Q;
set E = the carrier of R^1 ;
set PI = [:P,(id I[01] ):];
set QI = [:Q,(id I[01] ):];
A1:
the carrier of T is Subset of R^1
by TSEP_1:1;
then reconsider G = R1Homotopy P,Q as Function of [:I[01] ,I[01] :],R^1 by FUNCT_2:9;
reconsider P1 = P, Q1 = Q as Function of I[01] ,R^1 by A1, FUNCT_2:9;
reconsider P1 = P1, Q1 = Q1 as continuous Function of I[01] ,R^1 by PRE_TOPC:56;
set P1I = [:P1,(id I[01] ):];
set Q1I = [:Q1,(id I[01] ):];
A2:
( [:P1,(id I[01] ):] is continuous & [:Q1,(id I[01] ):] is continuous )
by BORSUK_2:12;
defpred S1[ Element of the carrier of R^1 , Element of the carrier of I[01] , set ] means $3 = (1 - $2) * $1;
defpred S2[ Element of the carrier of R^1 , Element of the carrier of I[01] , set ] means $3 = $2 * $1;
A3:
for x being Element of the carrier of R^1
for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S1[x,y,z]
by TOPMETR:24;
consider Pa being Function of [:the carrier of R^1 ,the carrier of I[01] :],the carrier of R^1 such that
A4:
for x being Element of the carrier of R^1
for i being Element of the carrier of I[01] holds S1[x,i,Pa . x,i]
from BINOP_1:sch 3(A3);
A5:
for x being Element of the carrier of R^1
for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S2[x,y,z]
consider Pb being Function of [:the carrier of R^1 ,the carrier of I[01] :],the carrier of R^1 such that
A6:
for x being Element of the carrier of R^1
for i being Element of the carrier of I[01] holds S2[x,i,Pb . x,i]
from BINOP_1:sch 3(A5);
reconsider Pa = Pa, Pb = Pb as Function of [:R^1 ,I[01] :],R^1 by Lm3;
( Pa is continuous & Pb is continuous )
by A4, A6, Th6, Th7;
then A7:
( Pa * [:P1,(id I[01] ):] is continuous & Pb * [:Q1,(id I[01] ):] is continuous )
by A2;
A8:
for p being Point of [:I[01] ,I[01] :] holds G . p = ((Pa * [:P1,(id I[01] ):]) . p) + ((Pb * [:Q1,(id I[01] ):]) . p)
proof
let p be
Point of
[:I[01] ,I[01] :];
:: thesis: G . p = ((Pa * [:P1,(id I[01] ):]) . p) + ((Pb * [:Q1,(id I[01] ):]) . p)
consider s,
t being
Point of
I[01] such that A9:
p = [s,t]
by BORSUK_1:50;
A10:
dom P = the
carrier of
I[01]
by FUNCT_2:def 1;
A11:
dom Q = the
carrier of
I[01]
by FUNCT_2:def 1;
A12:
(id I[01] ) . t = t
by FUNCT_1:35;
P . s in the
carrier of
T
;
then B1:
P . s in the
carrier of
R^1
by A1;
Q . s in the
carrier of
T
;
then B3:
Q . s in the
carrier of
R^1
by A1;
A13:
(Pa * [:P,(id I[01] ):]) . p =
Pa . ([:P,(id I[01] ):] . s,t)
by A9, FUNCT_2:21
.=
Pa . (P . s),
t
by A10, A12, Lm4, FUNCT_3:def 9
.=
(1 - t) * (P . s)
by B1, A4
;
A14:
(Pb * [:Q,(id I[01] ):]) . p =
Pb . ([:Q,(id I[01] ):] . s,t)
by A9, FUNCT_2:21
.=
Pb . (Q . s),
t
by A11, A12, Lm4, FUNCT_3:def 9
.=
t * (Q . s)
by B3, A6
;
reconsider a1 =
P . s,
b1 =
Q . s as
Point of
R^1 by PRE_TOPC:55;
(R1Homotopy P,Q) . s,
t = ((1 - t) * a1) + (t * b1)
by Def5;
hence
G . p = ((Pa * [:P1,(id I[01] ):]) . p) + ((Pb * [:Q1,(id I[01] ):]) . p)
by A9, A13, A14;
:: thesis: verum
end;
consider g being Function of [:I[01] ,I[01] :],R^1 such that
A15:
for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st (Pa * [:P1,(id I[01] ):]) . p = r1 & (Pb * [:Q1,(id I[01] ):]) . p = r2 holds
g . p = r1 + r2
and
A16:
g is continuous
by A7, JGRAPH_2:29;
for p being Point of [:I[01] ,I[01] :] holds G . p = g . p
then
G = g
by FUNCT_2:113;
hence
R1Homotopy P,Q is continuous
by A16, PRE_TOPC:57; :: thesis: verum