let f be Function of E,F; :: thesis: ( f is isometric & f is midpoints-preserving implies f is Affine )
assume that
A1: f is isometric and
A2: f is midpoints-preserving ; :: thesis: f is Affine
let a be Point of E; :: according to MAZURULM:def 2 :: thesis: for b being Point of E
for t being Real st 0 <= t & t <= 1 holds
f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b))
let b be Point of E; :: thesis: for t being Real st 0 <= t & t <= 1 holds
f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b))
let t be Real; :: thesis: ( 0 <= t & t <= 1 implies f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b)) )
assume ( 0 <= t & t <= 1 ) ; :: thesis: f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b))
then t in [.0,1.] by XXREAL_1:1;
then consider s being Real_Sequence such that
A3: rng s c= DYADIC and
A4: s is convergent and
A5: lim s = t by Th2, MEASURE6:64;
A6: dom f = the carrier of E by FUNCT_2:def 1;
set stb = s * b;
set 1t = 1 + (- s);
set s1ta = (1 + (- s)) * a;
set s1 = ((1 + (- s)) * a) + (s * b);
set za = (1 + (- s)) * (f . a);
set zb = s * (f . b);
A7: f is_continuous_on dom f by A1, Th24;
A8: - s is convergent by A4;
A9: ((1 + (- s)) * a) + (s * b) is convergent by A4, NORMSP_1:19;
A10: lim ((1 + (- s)) * a) = (lim (1 + (- s))) * a by A8, Th10;
A11: lim (- s) = - (lim s) by A4, SEQ_2:10;
A12: lim (1 + (- s)) = 1 + (lim (- s)) by A8, Th7
.= 1 - (lim s) by A11
.= 1 - t by A5 ;
lim (s * b) = (lim s) * b by A4, Th10;
then A13: lim (((1 + (- s)) * a) + (s * b)) = ((1 - t) * a) + (t * b) by A5, A10, A12, A4, NORMSP_1:25;
A14: lim ((1 + (- s)) * (f . a)) = (1 - t) * (f . a) by A8, A12, Th10;
A15: lim (s * (f . b)) = t * (f . b) by A4, A5, Th10;
A16: f /* (((1 + (- s)) * a) + (s * b)) = ((1 + (- s)) * (f . a)) + (s * (f . b))
proof
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (f /* (((1 + (- s)) * a) + (s * b))) . n = (((1 + (- s)) * (f . a)) + (s * (f . b))) . n
A17: (1 + (- s)) . n = 1 + ((- s) . n) by VALUED_1:2
.= 1 + (- (s . n)) by VALUED_1:8 ;
dom s = NAT by FUNCT_2:def 1;
then s . n in rng s by FUNCT_1:3;
then consider m being Nat such that
A18: s . n in dyadic m by A3, URYSOHN1:def 2;
consider i being Nat such that
A19: ( i <= 2 |^ m & s . n = i / (2 |^ m) ) by A18, URYSOHN1:def 1;
reconsider t = i as Nat ;
A20: f . (((1 - (t / (2 |^ m))) * a) + ((t / (2 |^ m)) * b)) = ((1 - (t / (2 |^ m))) * (f . a)) + ((t / (2 |^ m)) * (f . b)) by A19, Lm11, A2;
rng (((1 + (- s)) * a) + (s * b)) c= dom f by A6;
hence (f /* (((1 + (- s)) * a) + (s * b))) . n = f . ((((1 + (- s)) * a) + (s * b)) . n) by FUNCT_2:108
.= f . ((((1 + (- s)) * a) . n) + ((s * b) . n)) by NORMSP_1:def 2
.= f . (((1 - (s . n)) * a) + ((s * b) . n)) by A17, NDIFF_1:def 3
.= f . (((1 - (s . n)) * a) + ((s . n) * b)) by NDIFF_1:def 3
.= ((1 - (s . n)) * (f . a)) + ((s . n) * (f . b)) by A19, A20
.= (((1 + (- s)) . n) * (f . a)) + ((s * (f . b)) . n) by A17, NDIFF_1:def 3
.= (((1 + (- s)) * (f . a)) . n) + ((s * (f . b)) . n) by NDIFF_1:def 3
.= (((1 + (- s)) * (f . a)) + (s * (f . b))) . n by NORMSP_1:def 2 ;
:: thesis: verum
end;
A21: rng (((1 + (- s)) * a) + (s * b)) c= the carrier of E ;
thus f . (((1 - t) * a) + (t * b)) = f /. (((1 - t) * a) + (t * b))
.= lim (f /* (((1 + (- s)) * a) + (s * b))) by A6, A7, A21, A9, A13, NFCONT_1:18
.= ((1 - t) * (f . a)) + (t * (f . b)) by A14, A15, A4, A16, NORMSP_1:25 ; :: thesis: verum