:: Mazur-Ulam Theorem :: by Artur Korni{\l}owicz :: :: Received December 21, 2010 :: Copyright (c) 2010-2012 Association of Mizar Users begin registration cluster I[01] -> closed for SubSpace of R^1 ; coherence for b1 being SubSpace of R^1 st b1 = I[01] holds b1 is closed by TOPMETR:20, TREAL_1:2; end; reconsider D = DYADIC as Subset of I[01] by BORSUK_1:40, URYSOHN2:28; Lm1: Cl D = [#] I[01] proofend; theorem :: MAZURULM:1 DYADIC is dense Subset of I[01] proofend; theorem Th2: :: MAZURULM:2 Cl DYADIC = [.0,1.] proofend; theorem Th3: :: MAZURULM:3 for E being RealNormSpace for a being Point of E holds a + a = 2 * a proofend; theorem Th4: :: MAZURULM:4 for E being RealNormSpace for a, b being Point of E holds (a + b) - b = a proofend; registration let A be real-membered bounded_above set ; let r be real non negative number ; clusterr ** A -> bounded_above ; coherence r ** A is bounded_above proofend; end; registration let A be real-membered bounded_above set ; let r be real non positive number ; clusterr ** A -> bounded_below ; coherence r ** A is bounded_below proofend; end; registration let A be real-membered bounded_below set ; let r be real non negative number ; clusterr ** A -> bounded_below ; coherence r ** A is bounded_below proofend; end; registration let A be non empty real-membered bounded_below set ; let r be real non positive number ; clusterr ** A -> bounded_above ; coherence r ** A is bounded_above proofend; end; theorem Th5: :: MAZURULM:5 for t being real number for f being Real_Sequence holds f + (NAT --> t) = t + f proofend; theorem Th6: :: MAZURULM:6 for r being Real holds lim (NAT --> r) = r proofend; theorem Th7: :: MAZURULM:7 for t being real number for f being convergent Real_Sequence holds lim (t + f) = t + (lim f) proofend; registration let f be convergent Real_Sequence; let t be real number ; clustert + f -> convergent for Real_Sequence; coherence for b1 being Real_Sequence st b1 = t + f holds b1 is convergent proofend; end; theorem Th8: :: MAZURULM:8 for E being RealNormSpace for a being Point of E for f being Real_Sequence holds f (#) (NAT --> a) = f * a proofend; theorem Th9: :: MAZURULM:9 for E being RealNormSpace for a being Point of E holds lim (NAT --> a) = a proofend; theorem Th10: :: MAZURULM:10 for E being RealNormSpace for a being Point of E for f being convergent Real_Sequence holds lim (f * a) = (lim f) * a proofend; registration let f be convergent Real_Sequence; let E be RealNormSpace; let a be Point of E; clusterf * a -> convergent ; coherence f * a is convergent proofend; end; definition let E, F be non empty NORMSTR ; let f be Function of E,F; attrf is isometric means :Def1: :: MAZURULM:def 1 for a, b being Point of E holds ||.((f . a) - (f . b)).|| = ||.(a - b).||; end; :: deftheorem Def1 defines isometric MAZURULM:def_1_:_ for E, F being non empty NORMSTR for f being Function of E,F holds ( f is isometric iff for a, b being Point of E holds ||.((f . a) - (f . b)).|| = ||.(a - b).|| ); definition let E, F be non empty RLSStruct ; let f be Function of E,F; attrf is Affine means :Def2: :: MAZURULM:def 2 for a, b being Point of E for t being real number st 0 <= t & t <= 1 holds f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b)); attrf is midpoints-preserving means :Def3: :: MAZURULM:def 3 for a, b being Point of E holds f . ((1 / 2) * (a + b)) = (1 / 2) * ((f . a) + (f . b)); end; :: deftheorem Def2 defines Affine MAZURULM:def_2_:_ for E, F being non empty RLSStruct for f being Function of E,F holds ( f is Affine iff for a, b being Point of E for t being real number st 0 <= t & t <= 1 holds f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b)) ); :: deftheorem Def3 defines midpoints-preserving MAZURULM:def_3_:_ for E, F being non empty RLSStruct for f being Function of E,F holds ( f is midpoints-preserving iff for a, b being Point of E holds f . ((1 / 2) * (a + b)) = (1 / 2) * ((f . a) + (f . b)) ); registration let E be non empty NORMSTR ; cluster id E -> isometric ; coherence id E is isometric proofend; end; registration let E be non empty RLSStruct ; cluster id E -> Affine midpoints-preserving ; coherence ( id E is midpoints-preserving & id E is Affine ) proofend; end; registration let E be non empty NORMSTR ; cluster non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total bijective isometric Affine midpoints-preserving for Element of K10(K11( the carrier of E, the carrier of E)); existence ex b1 being UnOp of E st ( b1 is bijective & b1 is isometric & b1 is midpoints-preserving & b1 is Affine ) proofend; end; theorem Th11: :: MAZURULM:11 for E, F, G being RealNormSpace for f being Function of E,F for g being Function of F,G st f is isometric & g is isometric holds g * f is isometric proofend; registration let E be RealNormSpace; let f, g be isometric UnOp of E; clusterg * f -> isometric for UnOp of E; coherence for b1 being UnOp of E st b1 = g * f holds b1 is isometric by Th11; end; Lm2: now__::_thesis:_for_E,_F_being_RealNormSpace for_f_being_Function_of_E,F_st_f_is_bijective_holds_ for_a_being_Point_of_F_holds_f_._((f_/")_._a)_=_a let E, F be RealNormSpace; ::_thesis: for f being Function of E,F st f is bijective holds for a being Point of F holds f . ((f /") . a) = a let f be Function of E,F; ::_thesis: ( f is bijective implies for a being Point of F holds f . ((f /") . a) = a ) assume A1: f is bijective ; ::_thesis: for a being Point of F holds f . ((f /") . a) = a set g = f /" ; let a be Point of F; ::_thesis: f . ((f /") . a) = a rng f = [#] F by A1, FUNCT_2:def_3; then A2: (f /") /" = f by A1, TOPS_2:51; A3: f /" = f " by A1, TOPS_2:def_4; A4: f /" is bijective by A1, PENCIL_2:12; f = (f /") " by A2, A4, TOPS_2:def_4; hence f . ((f /") . a) = a by A1, A3, FUNCT_2:26; ::_thesis: verum end; theorem Th12: :: MAZURULM:12 for E, F being RealNormSpace for f being Function of E,F st f is bijective & f is isometric holds f /" is isometric proofend; registration let E be RealNormSpace; let f be bijective isometric UnOp of E; clusterf /" -> isometric ; coherence f /" is isometric by Th12; end; theorem Th13: :: MAZURULM:13 for E, F, G being RealNormSpace for f being Function of E,F for g being Function of F,G st f is midpoints-preserving & g is midpoints-preserving holds g * f is midpoints-preserving proofend; registration let E be RealNormSpace; let f, g be midpoints-preserving UnOp of E; clusterg * f -> midpoints-preserving for UnOp of E; coherence for b1 being UnOp of E st b1 = g * f holds b1 is midpoints-preserving by Th13; end; Lm3: now__::_thesis:_for_E,_F_being_RealNormSpace for_f_being_Function_of_E,F_st_f_is_bijective_holds_ (f_/")_*_f_=_id_E let E, F be RealNormSpace; ::_thesis: for f being Function of E,F st f is bijective holds (f /") * f = id E let f be Function of E,F; ::_thesis: ( f is bijective implies (f /") * f = id E ) assume A1: f is bijective ; ::_thesis: (f /") * f = id E then A2: rng f = [#] F by FUNCT_2:def_3; dom f = [#] E by FUNCT_2:def_1; hence (f /") * f = id E by A1, A2, TOPS_2:52; ::_thesis: verum end; theorem Th14: :: MAZURULM:14 for E, F being RealNormSpace for f being Function of E,F st f is bijective & f is midpoints-preserving holds f /" is midpoints-preserving proofend; registration let E be RealNormSpace; let f be bijective midpoints-preserving UnOp of E; clusterf /" -> midpoints-preserving ; coherence f /" is midpoints-preserving by Th14; end; theorem Th15: :: MAZURULM:15 for E, F, G being RealNormSpace for f being Function of E,F for g being Function of F,G st f is Affine & g is Affine holds g * f is Affine proofend; registration let E be RealNormSpace; let f, g be Affine UnOp of E; clusterg * f -> Affine for UnOp of E; coherence for b1 being UnOp of E st b1 = g * f holds b1 is Affine by Th15; end; theorem Th16: :: MAZURULM:16 for E, F being RealNormSpace for f being Function of E,F st f is bijective & f is Affine holds f /" is Affine proofend; registration let E be RealNormSpace; let f be bijective Affine UnOp of E; clusterf /" -> Affine ; coherence f /" is Affine by Th16; end; definition let E be non empty RLSStruct ; let a be Point of E; funca -reflection -> UnOp of E means :Def4: :: MAZURULM:def 4 for b being Point of E holds it . b = (2 * a) - b; existence ex b1 being UnOp of E st for b being Point of E holds b1 . b = (2 * a) - b proofend; uniqueness for b1, b2 being UnOp of E st ( for b being Point of E holds b1 . b = (2 * a) - b ) & ( for b being Point of E holds b2 . b = (2 * a) - b ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines -reflection MAZURULM:def_4_:_ for E being non empty RLSStruct for a being Point of E for b3 being UnOp of E holds ( b3 = a -reflection iff for b being Point of E holds b3 . b = (2 * a) - b ); theorem Th17: :: MAZURULM:17 for E being RealNormSpace for a being Point of E holds (a -reflection) * (a -reflection) = id E proofend; registration let E be RealNormSpace; let a be Point of E; clustera -reflection -> bijective ; coherence a -reflection is bijective proofend; end; theorem Th18: :: MAZURULM:18 for E being RealNormSpace for a being Point of E holds ( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds a = b ) ) proofend; theorem Th19: :: MAZURULM:19 for E being RealNormSpace for a, b being Point of E holds ((a -reflection) . b) - a = a - b proofend; theorem Th20: :: MAZURULM:20 for E being RealNormSpace for a, b being Point of E holds ||.(((a -reflection) . b) - a).|| = ||.(b - a).|| proofend; theorem Th21: :: MAZURULM:21 for E being RealNormSpace for a, b being Point of E holds ((a -reflection) . b) - b = 2 * (a - b) proofend; theorem Th22: :: MAZURULM:22 for E being RealNormSpace for a, b being Point of E holds ||.(((a -reflection) . b) - b).|| = 2 * ||.(b - a).|| proofend; theorem Th23: :: MAZURULM:23 for E being RealNormSpace for a being Point of E holds (a -reflection) /" = a -reflection proofend; registration let E be RealNormSpace; let a be Point of E; clustera -reflection -> isometric ; coherence a -reflection is isometric proofend; end; deffunc H1( RealNormSpace, Point of $1, Point of $1) -> set = { g where g is UnOp of $1 : ( g is bijective & g is isometric & g . $2 = $2 & g . $3 = $3 ) } ; deffunc H2( RealNormSpace, Point of $1, Point of $1) -> set = { ||.((g . ((1 / 2) * ($2 + $3))) - ((1 / 2) * ($2 + $3))).|| where g is UnOp of $1 : g in H1($1,$2,$3) } ; Lm4: now__::_thesis:_for_E_being_RealNormSpace for_a,_b_being_Point_of_E for_l_being_real-membered_set_st_l_=_H2(E,a,b)_holds_ 2_*_||.(a_-_((1_/_2)_*_(a_+_b))).||_is_UpperBound_of_l let E be RealNormSpace; ::_thesis: for a, b being Point of E for l being real-membered set st l = H2(E,a,b) holds 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l let a, b be Point of E; ::_thesis: for l being real-membered set st l = H2(E,a,b) holds 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l let l be real-membered set ; ::_thesis: ( l = H2(E,a,b) implies 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l ) assume A1: l = H2(E,a,b) ; ::_thesis: 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l set z = (1 / 2) * (a + b); thus 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l ::_thesis: verum proof let x be ext-real number ; :: according toXXREAL_2:def_1 ::_thesis: ( not x in l or x <= 2 * ||.(a - ((1 / 2) * (a + b))).|| ) assume x in l ; ::_thesis: x <= 2 * ||.(a - ((1 / 2) * (a + b))).|| then consider g1 being UnOp of E such that A2: x = ||.((g1 . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| and A3: g1 in H1(E,a,b) by A1; consider g being UnOp of E such that A4: g1 = g and g is bijective and A5: g is isometric and A6: g . a = a and g . b = b by A3; A7: ||.((g . ((1 / 2) * (a + b))) - a).|| = ||.(((1 / 2) * (a + b)) - a).|| by A5, A6, Def1 .= ||.(a - ((1 / 2) * (a + b))).|| by NORMSP_1:7 ; ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| <= ||.((g . ((1 / 2) * (a + b))) - a).|| + ||.(a - ((1 / 2) * (a + b))).|| by NORMSP_1:10; hence x <= 2 * ||.(a - ((1 / 2) * (a + b))).|| by A2, A4, A7; ::_thesis: verum end; end; Lm5: now__::_thesis:_for_E_being_RealNormSpace for_a,_b_being_Point_of_E for_h_being_UnOp_of_E_st_h_in_H1(E,a,b)_holds_ (((((1_/_2)_*_(a_+_b))_-reflection)_*_(h_/"))_*_(((1_/_2)_*_(a_+_b))_-reflection))_*_h_in_H1(E,a,b) let E be RealNormSpace; ::_thesis: for a, b being Point of E for h being UnOp of E st h in H1(E,a,b) holds (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H1(E,a,b) let a, b be Point of E; ::_thesis: for h being UnOp of E st h in H1(E,a,b) holds (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H1(E,a,b) let h be UnOp of E; ::_thesis: ( h in H1(E,a,b) implies (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H1(E,a,b) ) assume A1: h in H1(E,a,b) ; ::_thesis: (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H1(E,a,b) set z = (1 / 2) * (a + b); set R = ((1 / 2) * (a + b)) -reflection ; set gs = (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h; consider g being UnOp of E such that A2: g = h and A3: g is bijective and A4: g is isometric and A5: g . a = a and A6: g . b = b by A1; A7: g /" = g " by A3, TOPS_2:def_4; then A8: g /" is bijective by A3, GROUP_6:63; A9: 2 * ((1 / 2) * (a + b)) = (2 * (1 / 2)) * (a + b) by RLVECT_1:def_7 .= a + b by RLVECT_1:def_8 ; then A10: (2 * ((1 / 2) * (a + b))) - a = b by Th4; A11: (2 * ((1 / 2) * (a + b))) - b = a by A9, Th4; A12: dom g = [#] E by FUNCT_2:def_1; A13: (g /") . b = b by A7, A6, A3, A12, FUNCT_1:32; A14: (g /") . a = a by A7, A5, A3, A12, FUNCT_1:32; A15: ((((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h) . a = (((((1 / 2) * (a + b)) -reflection) * (g /")) * (((1 / 2) * (a + b)) -reflection)) . a by A5, A2, FUNCT_2:15 .= ((((1 / 2) * (a + b)) -reflection) * (g /")) . ((((1 / 2) * (a + b)) -reflection) . a) by FUNCT_2:15 .= ((((1 / 2) * (a + b)) -reflection) * (g /")) . b by A10, Def4 .= (((1 / 2) * (a + b)) -reflection) . ((g /") . b) by FUNCT_2:15 .= (2 * ((1 / 2) * (a + b))) - b by A13, Def4 .= a by A9, Th4 ; ((((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h) . b = (((((1 / 2) * (a + b)) -reflection) * (g /")) * (((1 / 2) * (a + b)) -reflection)) . b by A6, A2, FUNCT_2:15 .= ((((1 / 2) * (a + b)) -reflection) * (g /")) . ((((1 / 2) * (a + b)) -reflection) . b) by FUNCT_2:15 .= ((((1 / 2) * (a + b)) -reflection) * (g /")) . a by A11, Def4 .= (((1 / 2) * (a + b)) -reflection) . ((g /") . a) by FUNCT_2:15 .= (2 * ((1 / 2) * (a + b))) - a by A14, Def4 .= b by A9, Th4 ; hence (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H1(E,a,b) by A2, A3, A4, A8, A15; ::_thesis: verum end; Lm6: now__::_thesis:_for_E_being_RealNormSpace for_a,_b_being_Point_of_E for_l_being_non_empty_bounded_above_Subset_of_REAL_st_l_=_H2(E,a,b)_holds_ sup_l_is_UpperBound_of_2_**_l let E be RealNormSpace; ::_thesis: for a, b being Point of E for l being non empty bounded_above Subset of REAL st l = H2(E,a,b) holds sup l is UpperBound of 2 ** l let a, b be Point of E; ::_thesis: for l being non empty bounded_above Subset of REAL st l = H2(E,a,b) holds sup l is UpperBound of 2 ** l let l be non empty bounded_above Subset of REAL; ::_thesis: ( l = H2(E,a,b) implies sup l is UpperBound of 2 ** l ) assume A1: l = H2(E,a,b) ; ::_thesis: sup l is UpperBound of 2 ** l thus sup l is UpperBound of 2 ** l ::_thesis: verum proof set z = (1 / 2) * (a + b); set R = ((1 / 2) * (a + b)) -reflection ; let x be ext-real number ; :: according toXXREAL_2:def_1 ::_thesis: ( not x in 2 ** l or x <= sup l ) assume x in 2 ** l ; ::_thesis: x <= sup l then consider w being Element of ExtREAL such that A2: x = 2 * w and A3: w in l by MEMBER_1:188; consider h being UnOp of E such that A4: w = ||.((h . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| and A5: h in H1(E,a,b) by A3, A1; consider g being UnOp of E such that A6: g = h and A7: g is bijective and A8: g is isometric and ( g . a = a & g . b = b ) by A5; A9: (((1 / 2) * (a + b)) -reflection) * ((g /") * ((((1 / 2) * (a + b)) -reflection) * g)) = ((((1 / 2) * (a + b)) -reflection) * (g /")) * ((((1 / 2) * (a + b)) -reflection) * g) by RELAT_1:36 .= (((((1 / 2) * (a + b)) -reflection) * (g /")) * (((1 / 2) * (a + b)) -reflection)) * g by RELAT_1:36 ; A10: (((1 / 2) * (a + b)) -reflection) . ((g /") . ((((1 / 2) * (a + b)) -reflection) . (g . ((1 / 2) * (a + b))))) = (((1 / 2) * (a + b)) -reflection) . ((g /") . (((((1 / 2) * (a + b)) -reflection) * g) . ((1 / 2) * (a + b)))) by FUNCT_2:15 .= (((1 / 2) * (a + b)) -reflection) . (((g /") * ((((1 / 2) * (a + b)) -reflection) * g)) . ((1 / 2) * (a + b))) by FUNCT_2:15 .= ((((1 / 2) * (a + b)) -reflection) * ((g /") * ((((1 / 2) * (a + b)) -reflection) * g))) . ((1 / 2) * (a + b)) by FUNCT_2:15 ; A11: g /" = g " by A7, TOPS_2:def_4; (((((1 / 2) * (a + b)) -reflection) * (g /")) * (((1 / 2) * (a + b)) -reflection)) * g in H1(E,a,b) by A5, A6, Lm5; then A12: ||.((((((((1 / 2) * (a + b)) -reflection) * (g /")) * (((1 / 2) * (a + b)) -reflection)) * g) . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| in l by A1; reconsider d = 2 as R_eal by XXREAL_0:def_1; ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| in ExtREAL by XXREAL_0:def_1; then A13: d * ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| = 2 * ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| by EXTREAL1:1; A14: (g /") . (g . ((1 / 2) * (a + b))) = (1 / 2) * (a + b) by A7, A11, FUNCT_2:26; 2 * ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| = ||.(((((1 / 2) * (a + b)) -reflection) . (g . ((1 / 2) * (a + b)))) - (g . ((1 / 2) * (a + b)))).|| by Th22 .= ||.(((g /") . ((((1 / 2) * (a + b)) -reflection) . (g . ((1 / 2) * (a + b))))) - ((g /") . (g . ((1 / 2) * (a + b))))).|| by A7, A8, Def1 .= ||.(((((1 / 2) * (a + b)) -reflection) . ((g /") . ((((1 / 2) * (a + b)) -reflection) . (g . ((1 / 2) * (a + b)))))) - ((1 / 2) * (a + b))).|| by A14, Th20 ; hence x <= sup l by A2, A4, A9, A10, A12, A6, A13, XXREAL_2:4; ::_thesis: verum end; end; Lm7: now__::_thesis:_for_E_being_RealNormSpace for_a,_b_being_Point_of_E for_l_being_real-membered_set_st_l_=_H2(E,a,b)_holds_ for_g_being_UnOp_of_E_st_g_in_H1(E,a,b)_holds_ g_._((1_/_2)_*_(a_+_b))_=_(1_/_2)_*_(a_+_b) let E be RealNormSpace; ::_thesis: for a, b being Point of E for l being real-membered set st l = H2(E,a,b) holds for g being UnOp of E st g in H1(E,a,b) holds g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) let a, b be Point of E; ::_thesis: for l being real-membered set st l = H2(E,a,b) holds for g being UnOp of E st g in H1(E,a,b) holds g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) let l be real-membered set ; ::_thesis: ( l = H2(E,a,b) implies for g being UnOp of E st g in H1(E,a,b) holds g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) ) assume A1: l = H2(E,a,b) ; ::_thesis: for g being UnOp of E st g in H1(E,a,b) holds g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) let g be UnOp of E; ::_thesis: ( g in H1(E,a,b) implies g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) ) assume A2: g in H1(E,a,b) ; ::_thesis: g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) set z = (1 / 2) * (a + b); set R = ((1 / 2) * (a + b)) -reflection ; A3: l c= REAL proof let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in l or x in REAL ) assume x in l ; ::_thesis: x in REAL then ex g being UnOp of E st ( x = ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| & g in H1(E,a,b) ) by A1; hence x in REAL ; ::_thesis: verum end; ( (id E) . a = a & (id E) . b = b ) by FUNCT_1:18; then id E in H1(E,a,b) ; then A4: ||.(((id E) . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| in l by A1; 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l by A1, Lm4; then reconsider A = l as non empty bounded_above Subset of REAL by A3, A4, XXREAL_2:def_10; set lambda = sup A; reconsider d = 2 as R_eal by XXREAL_0:def_1; A5: d * (sup A) = sup (2 ** A) by URYSOHN2:18; A6: ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| in A by A1, A2; A7: d * (sup A) = 2 * (sup A) by XXREAL_3:def_5; sup A is UpperBound of 2 ** A by A1, Lm6; then sup (2 ** A) <= sup A by XXREAL_2:def_3; then (2 * (sup A)) - (sup A) <= (sup A) - (sup A) by A7, A5, XREAL_1:9; then ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| = 0 by A6, XXREAL_2:4; hence g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) by NORMSP_1:6; ::_thesis: verum end; theorem Th24: :: MAZURULM:24 for E, F being RealNormSpace for f being Function of E,F st f is isometric holds f is_continuous_on dom f proofend; Lm8: for E being RealNormSpace for a, b being Point of E for t being real number holds ((1 - t) * a) + (t * b) = a + (t * (b - a)) proofend; Lm9: now__::_thesis:_for_E,_F_being_RealNormSpace for_f_being_Function_of_E,F for_a,_b_being_Point_of_E for_n,_j_being_Nat_st_f_is_midpoints-preserving_&_j_<=_2_|^_n_holds_ ex_x_being_Nat_st_ (_x_=_(2_|^_n)_-_j_&_f_._(a_+_((j_/_(2_|^_(n_+_1)))_*_(b_-_a)))_=_(1_/_2)_*_((f_._a)_+_(f_._((1_/_(2_|^_n))_*_((x_*_a)_+_(j_*_b)))))_) let E, F be RealNormSpace; ::_thesis: for f being Function of E,F for a, b being Point of E for n, j being Nat st f is midpoints-preserving & j <= 2 |^ n holds ex x being Nat st ( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) ) let f be Function of E,F; ::_thesis: for a, b being Point of E for n, j being Nat st f is midpoints-preserving & j <= 2 |^ n holds ex x being Nat st ( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) ) let a, b be Point of E; ::_thesis: for n, j being Nat st f is midpoints-preserving & j <= 2 |^ n holds ex x being Nat st ( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) ) let n, j be Nat; ::_thesis: ( f is midpoints-preserving & j <= 2 |^ n implies ex x being Nat st ( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) ) ) set m = 2 |^ (n + 1); set k = 2 |^ n; set x = (2 |^ n) - j; assume A1: f is midpoints-preserving ; ::_thesis: ( j <= 2 |^ n implies ex x being Nat st ( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) ) ) assume j <= 2 |^ n ; ::_thesis: ex x being Nat st ( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) ) then (2 |^ n) - j in NAT by INT_1:5; then reconsider x = (2 |^ n) - j as Nat ; take x = x; ::_thesis: ( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) ) thus x = (2 |^ n) - j ; ::_thesis: f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) set z = (1 - (j / (2 |^ (n + 1)))) - (1 / 2); A2: 2 |^ n <> 0 by NEWTON:83; A3: 2 * (2 |^ n) = 2 |^ (n + 1) by NEWTON:6; A4: (1 / 2) * (1 / (2 |^ n)) = 1 / (2 * (2 |^ n)) by XCMPLX_1:102; x / (2 |^ (n + 1)) = ((1 * (2 |^ n)) / (2 |^ (n + 1))) - (j / (2 |^ (n + 1))) .= (1 / 2) - (j / (2 |^ (n + 1))) by A2, A3, XCMPLX_1:91 .= (1 - (j / (2 |^ (n + 1)))) - (1 / 2) ; then A5: (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a) + ((j / (2 |^ (n + 1))) * b) = ((1 / (2 |^ (n + 1))) * (x * a)) + (((1 / (2 |^ (n + 1))) * j) * b) by RLVECT_1:def_7 .= ((1 / (2 |^ (n + 1))) * (x * a)) + ((1 / (2 |^ (n + 1))) * (j * b)) by RLVECT_1:def_7 .= (1 / (2 |^ (n + 1))) * ((x * a) + (j * b)) by RLVECT_1:def_5 .= (1 / 2) * ((1 / (2 |^ n)) * ((x * a) + (j * b))) by A4, A3, RLVECT_1:def_7 ; a + ((j / (2 |^ (n + 1))) * (b - a)) = a + (((j / (2 |^ (n + 1))) * b) - ((j / (2 |^ (n + 1))) * a)) by RLVECT_1:34 .= (a + ((j / (2 |^ (n + 1))) * b)) - ((j / (2 |^ (n + 1))) * a) by RLVECT_1:def_3 .= (a - ((j / (2 |^ (n + 1))) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:def_3 .= ((1 * a) - ((j / (2 |^ (n + 1))) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:def_8 .= ((1 - (j / (2 |^ (n + 1)))) * a) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:35 .= ((((1 - (j / (2 |^ (n + 1)))) * a) + (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a)) - (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a)) + ((j / (2 |^ (n + 1))) * b) by Th4 .= ((((1 - (j / (2 |^ (n + 1)))) * a) - (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a)) + (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:def_3 .= ((((1 - (j / (2 |^ (n + 1)))) - ((1 - (j / (2 |^ (n + 1)))) - (1 / 2))) * a) + (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:35 .= ((1 / 2) * a) + ((((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a) + ((j / (2 |^ (n + 1))) * b)) by RLVECT_1:def_3 .= (1 / 2) * (a + ((1 / (2 |^ n)) * ((x * a) + (j * b)))) by A5, RLVECT_1:def_5 ; hence f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) by A1, Def3; ::_thesis: verum end; Lm10: now__::_thesis:_for_E,_F_being_RealNormSpace for_f_being_Function_of_E,F for_a,_b_being_Point_of_E for_n,_j_being_Nat_st_f_is_midpoints-preserving_&_j_>=_2_|^_n_holds_ ex_x_being_Nat_st_ (_x_=_((2_|^_n)_+_j)_-_(2_|^_(n_+_1))_&_f_._(a_+_((j_/_(2_|^_(n_+_1)))_*_(b_-_a)))_=_(1_/_2)_*_((f_._b)_+_(f_._((1_/_(2_|^_n))_*_((((2_|^_(n_+_1))_-_j)_*_a)_+_(x_*_b)))))_) let E, F be RealNormSpace; ::_thesis: for f being Function of E,F for a, b being Point of E for n, j being Nat st f is midpoints-preserving & j >= 2 |^ n holds ex x being Nat st ( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) ) let f be Function of E,F; ::_thesis: for a, b being Point of E for n, j being Nat st f is midpoints-preserving & j >= 2 |^ n holds ex x being Nat st ( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) ) let a, b be Point of E; ::_thesis: for n, j being Nat st f is midpoints-preserving & j >= 2 |^ n holds ex x being Nat st ( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) ) let n, j be Nat; ::_thesis: ( f is midpoints-preserving & j >= 2 |^ n implies ex x being Nat st ( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) ) ) set m = 2 |^ (n + 1); set k = 2 |^ n; set x = ((2 |^ n) + j) - (2 |^ (n + 1)); assume A1: f is midpoints-preserving ; ::_thesis: ( j >= 2 |^ n implies ex x being Nat st ( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) ) ) A2: 2 * (2 |^ n) = 2 |^ (n + 1) by NEWTON:6; assume j >= 2 |^ n ; ::_thesis: ex x being Nat st ( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) ) then (2 |^ n) + (2 |^ n) <= (2 |^ n) + j by XREAL_1:6; then ((2 |^ n) + j) - (2 |^ (n + 1)) in NAT by A2, INT_1:5; then reconsider x = ((2 |^ n) + j) - (2 |^ (n + 1)) as Nat ; take x = x; ::_thesis: ( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) ) thus x = ((2 |^ n) + j) - (2 |^ (n + 1)) ; ::_thesis: f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) set z = (j / (2 |^ (n + 1))) - (1 / 2); A3: 2 |^ n <> 0 by NEWTON:83; A4: 2 |^ (n + 1) <> 0 by NEWTON:83; A5: (2 |^ (n + 1)) / (2 |^ (n + 1)) = 1 by A4, XCMPLX_1:60; then A6: 1 - (j / (2 |^ (n + 1))) = (1 / (2 |^ (n + 1))) * ((2 |^ (n + 1)) - j) ; A7: (2 |^ n) / (2 |^ (n + 1)) = (1 * (2 |^ n)) / (2 * (2 |^ n)) by NEWTON:6 .= 1 / 2 by A3, XCMPLX_1:91 ; A8: (1 / 2) * (1 / (2 |^ n)) = 1 / (2 * (2 |^ n)) by XCMPLX_1:102; x / (2 |^ (n + 1)) = (((2 |^ n) + j) / (2 |^ (n + 1))) - ((2 |^ (n + 1)) / (2 |^ (n + 1))) .= (j / (2 |^ (n + 1))) - (1 / 2) by A5, A7 ; then A9: (((j / (2 |^ (n + 1))) - (1 / 2)) * b) + ((1 - (j / (2 |^ (n + 1)))) * a) = ((1 / (2 |^ (n + 1))) * (((2 |^ (n + 1)) - j) * a)) + (((1 / (2 |^ (n + 1))) * x) * b) by A6, RLVECT_1:def_7 .= ((1 / (2 |^ (n + 1))) * (((2 |^ (n + 1)) - j) * a)) + ((1 / (2 |^ (n + 1))) * (x * b)) by RLVECT_1:def_7 .= (1 / (2 |^ (n + 1))) * ((((2 |^ (n + 1)) - j) * a) + (x * b)) by RLVECT_1:def_5 .= (1 / 2) * ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))) by A8, A2, RLVECT_1:def_7 ; a + ((j / (2 |^ (n + 1))) * (b - a)) = a + (((j / (2 |^ (n + 1))) * b) - ((j / (2 |^ (n + 1))) * a)) by RLVECT_1:34 .= (a + ((j / (2 |^ (n + 1))) * b)) - ((j / (2 |^ (n + 1))) * a) by RLVECT_1:def_3 .= (a - ((j / (2 |^ (n + 1))) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:def_3 .= ((1 * a) - ((j / (2 |^ (n + 1))) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:def_8 .= ((1 - (j / (2 |^ (n + 1)))) * a) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:35 .= ((((j / (2 |^ (n + 1))) * b) + (((j / (2 |^ (n + 1))) - (1 / 2)) * b)) - (((j / (2 |^ (n + 1))) - (1 / 2)) * b)) + ((1 - (j / (2 |^ (n + 1)))) * a) by Th4 .= ((((j / (2 |^ (n + 1))) * b) - (((j / (2 |^ (n + 1))) - (1 / 2)) * b)) + (((j / (2 |^ (n + 1))) - (1 / 2)) * b)) + ((1 - (j / (2 |^ (n + 1)))) * a) by RLVECT_1:def_3 .= ((((j / (2 |^ (n + 1))) - ((j / (2 |^ (n + 1))) - (1 / 2))) * b) + (((j / (2 |^ (n + 1))) - (1 / 2)) * b)) + ((1 - (j / (2 |^ (n + 1)))) * a) by RLVECT_1:35 .= ((1 / 2) * b) + ((((j / (2 |^ (n + 1))) - (1 / 2)) * b) + ((1 - (j / (2 |^ (n + 1)))) * a)) by RLVECT_1:def_3 .= (1 / 2) * (b + ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b)))) by A9, RLVECT_1:def_5 ; hence f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) by A1, Def3; ::_thesis: verum end; Lm11: now__::_thesis:_for_E,_F_being_RealNormSpace for_f_being_Function_of_E,F for_a,_b_being_Point_of_E for_t_being_Nat_st_f_is_midpoints-preserving_holds_ for_n_being_Nat_st_t_<=_2_|^_n_holds_ f_._(((1_-_(t_/_(2_|^_n)))_*_a)_+_((t_/_(2_|^_n))_*_b))_=_((1_-_(t_/_(2_|^_n)))_*_(f_._a))_+_((t_/_(2_|^_n))_*_(f_._b)) let E, F be RealNormSpace; ::_thesis: for f being Function of E,F for a, b being Point of E for t being Nat st f is midpoints-preserving holds for n being Nat st t <= 2 |^ n holds f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)) let f be Function of E,F; ::_thesis: for a, b being Point of E for t being Nat st f is midpoints-preserving holds for n being Nat st t <= 2 |^ n holds f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)) let a, b be Point of E; ::_thesis: for t being Nat st f is midpoints-preserving holds for n being Nat st t <= 2 |^ n holds f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)) let t be Nat; ::_thesis: ( f is midpoints-preserving implies for n being Nat st t <= 2 |^ n holds f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)) ) assume A1: f is midpoints-preserving ; ::_thesis: for n being Nat st t <= 2 |^ n holds f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)) thus for n being Nat st t <= 2 |^ n holds f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)) ::_thesis: verum proof defpred S1[ Nat] means for w being Nat st w <= 2 |^ $1 holds f . (((1 - (w / (2 |^ $1))) * a) + ((w / (2 |^ $1)) * b)) = ((1 - (w / (2 |^ $1))) * (f . a)) + ((w / (2 |^ $1)) * (f . b)); A2: S1[ 0 ] proof let t be Nat; ::_thesis: ( t <= 2 |^ 0 implies f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b)) ) assume A3: t <= 2 |^ 0 ; ::_thesis: f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b)) A4: 2 |^ 0 = 1 by NEWTON:4; percases ( t = 1 or t = 0 ) by A3, A4, NAT_1:25; supposeA5: t = 1 ; ::_thesis: f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b)) then f . (((1 - t) * a) + (t * b)) = f . ((0. E) + (t * b)) by RLVECT_1:10 .= f . (t * b) by RLVECT_1:4 .= f . b by A5, RLVECT_1:def_8 .= t * (f . b) by A5, RLVECT_1:def_8 .= (0. F) + (t * (f . b)) by RLVECT_1:4 .= ((1 - t) * (f . a)) + (t * (f . b)) by A5, RLVECT_1:10 ; hence f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b)) by A4; ::_thesis: verum end; supposeA6: t = 0 ; ::_thesis: f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b)) then f . (((1 - t) * a) + (t * b)) = f . ((1 * a) + (0. E)) by RLVECT_1:10 .= f . (1 * a) by RLVECT_1:4 .= f . a by RLVECT_1:def_8 .= (1 - t) * (f . a) by A6, RLVECT_1:def_8 .= ((1 - t) * (f . a)) + (0. F) by RLVECT_1:4 .= ((1 - t) * (f . a)) + (t * (f . b)) by A6, RLVECT_1:10 ; hence f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b)) by A4; ::_thesis: verum end; end; end; A7: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) set m = 2 |^ n; set k = 2 |^ (n + 1); assume A8: S1[n] ; ::_thesis: S1[n + 1] let t be Nat; ::_thesis: ( t <= 2 |^ (n + 1) implies f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b)) ) assume A9: t <= 2 |^ (n + 1) ; ::_thesis: f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b)) A10: 2 |^ (n + 1) = (2 |^ n) * 2 by NEWTON:6; A11: 2 |^ n <> 0 by NEWTON:83; A12: (1 / 2) * (t / (2 |^ n)) = (1 * t) / (2 * (2 |^ n)) by XCMPLX_1:76 .= t / (2 |^ (n + 1)) by NEWTON:6 ; percases ( t <= 2 |^ n or t >= 2 |^ n ) ; supposeA13: t <= 2 |^ n ; ::_thesis: f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b)) then consider x being Nat such that A14: x = (2 |^ n) - t and A15: f . (a + ((t / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (t * b))))) by A1, Lm9; A16: x / (2 |^ n) = ((2 |^ n) / (2 |^ n)) - (t / (2 |^ n)) by A14 .= 1 - (t / (2 |^ n)) by A11, XCMPLX_1:60 ; A17: (1 / (2 |^ n)) * ((x * a) + (t * b)) = ((1 / (2 |^ n)) * (x * a)) + ((1 / (2 |^ n)) * (t * b)) by RLVECT_1:def_5 .= ((1 / (2 |^ n)) * (x * a)) + ((t / (2 |^ n)) * b) by RLVECT_1:def_7 .= ((x / (2 |^ n)) * a) + ((t / (2 |^ n)) * b) by RLVECT_1:def_7 ; thus f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = f . (a + ((t / (2 |^ (n + 1))) * (b - a))) by Lm8 .= ((1 / 2) * (f . a)) + ((1 / 2) * (f . ((1 / (2 |^ n)) * ((x * a) + (t * b))))) by A15, RLVECT_1:def_5 .= ((1 / 2) * (f . a)) + ((1 / 2) * (((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)))) by A16, A13, A17, A8 .= ((1 / 2) * (f . a)) + (((1 / 2) * ((1 - (t / (2 |^ n))) * (f . a))) + ((1 / 2) * ((t / (2 |^ n)) * (f . b)))) by RLVECT_1:def_5 .= (((1 / 2) * (f . a)) + ((1 / 2) * ((1 - (t / (2 |^ n))) * (f . a)))) + ((1 / 2) * ((t / (2 |^ n)) * (f . b))) by RLVECT_1:def_3 .= (((1 / 2) * (f . a)) + (((1 / 2) * (1 - (t / (2 |^ n)))) * (f . a))) + ((1 / 2) * ((t / (2 |^ n)) * (f . b))) by RLVECT_1:def_7 .= (((1 / 2) + ((1 / 2) * (1 - (t / (2 |^ n))))) * (f . a)) + ((1 / 2) * ((t / (2 |^ n)) * (f . b))) by RLVECT_1:def_6 .= ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b)) by A12, RLVECT_1:def_7 ; ::_thesis: verum end; suppose t >= 2 |^ n ; ::_thesis: f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b)) then consider x being Nat such that A18: x = ((2 |^ n) + t) - (2 |^ (n + 1)) and A19: f . (a + ((t / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - t) * a) + (x * b))))) by A1, Lm10; set w = t - (2 |^ n); A20: t - (2 |^ n) <= (2 * (2 |^ n)) - (2 |^ n) by A9, A10, XREAL_1:9; A21: (2 |^ n) / (2 |^ n) = 1 by A11, XCMPLX_1:60; A22: (2 |^ (n + 1)) / (2 |^ n) = (2 * (2 |^ n)) / (1 * (2 |^ n)) by NEWTON:6 .= 2 / 1 by A11, XCMPLX_1:91 ; A23: (1 / 2) * (1 - ((t - (2 |^ n)) / (2 |^ n))) = 1 - ((1 / 2) * (t / (2 |^ n))) by A21 .= 1 - ((1 * t) / (2 * (2 |^ n))) by XCMPLX_1:76 .= 1 - (t / (2 |^ (n + 1))) by NEWTON:6 ; thus f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = f . (a + ((t / (2 |^ (n + 1))) * (b - a))) by Lm8 .= ((1 / 2) * (f . b)) + ((1 / 2) * (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - t) * a) + (x * b))))) by A19, RLVECT_1:def_5 .= ((1 / 2) * (f . b)) + ((1 / 2) * (f . (((1 / (2 |^ n)) * (((2 |^ (n + 1)) - t) * a)) + ((1 / (2 |^ n)) * (x * b))))) by RLVECT_1:def_5 .= ((1 / 2) * (f . b)) + ((1 / 2) * (f . ((((1 / (2 |^ n)) * ((2 |^ (n + 1)) - t)) * a) + ((1 / (2 |^ n)) * (x * b))))) by RLVECT_1:def_7 .= ((1 / 2) * (f . b)) + ((1 / 2) * (f . ((((1 / (2 |^ n)) * ((2 |^ (n + 1)) - t)) * a) + (((1 / (2 |^ n)) * x) * b)))) by RLVECT_1:def_7 .= ((1 / 2) * (f . b)) + ((1 / 2) * (((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a)) + (((t - (2 |^ n)) / (2 |^ n)) * (f . b)))) by A20, A21, A22, A18, A10, A8 .= ((1 / 2) * (f . b)) + (((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + ((1 / 2) * (((t - (2 |^ n)) / (2 |^ n)) * (f . b)))) by RLVECT_1:def_5 .= ((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + (((1 / 2) * (f . b)) + ((1 / 2) * (((t - (2 |^ n)) / (2 |^ n)) * (f . b)))) by RLVECT_1:def_3 .= ((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + ((1 / 2) * ((f . b) + (((t - (2 |^ n)) / (2 |^ n)) * (f . b)))) by RLVECT_1:def_5 .= ((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + ((1 / 2) * ((1 * (f . b)) + (((t - (2 |^ n)) / (2 |^ n)) * (f . b)))) by RLVECT_1:def_8 .= ((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + ((1 / 2) * ((1 + ((t - (2 |^ n)) / (2 |^ n))) * (f . b))) by RLVECT_1:def_6 .= ((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + (((1 / 2) * (1 + ((t - (2 |^ n)) / (2 |^ n)))) * (f . b)) by RLVECT_1:def_7 .= ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b)) by A23, RLVECT_1:def_7 ; ::_thesis: verum end; end; end; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A7); hence for n being Nat st t <= 2 |^ n holds f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)) ; ::_thesis: verum end; end; registration let E, F be RealNormSpace; cluster Function-like quasi_total bijective isometric -> midpoints-preserving for Element of K10(K11( the carrier of E, the carrier of F)); coherence for b1 being Function of E,F st b1 is bijective & b1 is isometric holds b1 is midpoints-preserving proofend; end; registration let E, F be RealNormSpace; cluster Function-like quasi_total isometric midpoints-preserving -> Affine for Element of K10(K11( the carrier of E, the carrier of F)); coherence for b1 being Function of E,F st b1 is isometric & b1 is midpoints-preserving holds b1 is Affine proofend; end;