let n be Element of NAT ; :: thesis: for T being non empty convex SubSpace of TOP-REAL n
for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
reconsider x0 = 0 , x1 = 1 as Point of I[01] by BORSUK_1:def 14, BORSUK_1:def 15;
let T be non empty convex SubSpace of TOP-REAL n; :: thesis: for a, b being Point of T
for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
let a, b be Point of T; :: thesis: for P, Q being Path of a,b
for s being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
let P, Q be Path of a,b; :: thesis: for s being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
set F = ConvexHomotopy (P,Q);
let s be Point of I[01]; :: thesis: ( (ConvexHomotopy (P,Q)) . (s,0) = P . s & (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:25;
A1: P . x0 = a by BORSUK_2:def 4;
(ConvexHomotopy (P,Q)) . (s,x0) = ((1 - x0) * a1) + (x0 * b1) by Def2;
hence (ConvexHomotopy (P,Q)) . (s,0) = a1 + (0 * b1) by RLVECT_1:def 8
.= a1 + (0. (TOP-REAL n)) by RLVECT_1:10
.= P . s by RLVECT_1:4 ;
:: thesis: ( (ConvexHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b ) ) )
(ConvexHomotopy (P,Q)) . (s,x1) = ((1 - x1) * a1) + (x1 * b1) by Def2;
hence (ConvexHomotopy (P,Q)) . (s,1) = (0. (TOP-REAL n)) + (1 * b1) by RLVECT_1:10
.= (0. (TOP-REAL n)) + b1 by RLVECT_1:def 8
.= Q . s by RLVECT_1:4 ;
:: thesis: for t being Point of I[01] holds
( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b )
reconsider a1 = P . x0, b1 = Q . x0 as Point of (TOP-REAL n) by PRE_TOPC:25;
let t be Point of I[01]; :: thesis: ( (ConvexHomotopy (P,Q)) . (0,t) = a & (ConvexHomotopy (P,Q)) . (1,t) = b )
( (ConvexHomotopy (P,Q)) . (0,t) = ((1 - t) * a1) + (t * b1) & Q . x0 = a ) by Def2, BORSUK_2:def 4;
hence (ConvexHomotopy (P,Q)) . (0,t) = ((1 * a1) - (t * a1)) + (t * a1) by A1, RLVECT_1:35
.= 1 * a1 by RLVECT_4:1
.= a by A1, RLVECT_1:def 8 ;
:: thesis: (ConvexHomotopy (P,Q)) . (1,t) = b
A2: Q . x1 = b by BORSUK_2:def 4;
reconsider a1 = P . x1, b1 = Q . x1 as Point of (TOP-REAL n) by PRE_TOPC:25;
A3: P . x1 = b by BORSUK_2:def 4;
(ConvexHomotopy (P,Q)) . (1,t) = ((1 - t) * a1) + (t * b1) by Def2;
hence (ConvexHomotopy (P,Q)) . (1,t) = ((1 * a1) - (t * b1)) + (t * a1) by A3, A2, RLVECT_1:35
.= 1 * b1 by A3, A2, RLVECT_4:1
.= b by A2, RLVECT_1:def 8 ;
:: thesis: verum