let f be Function of E,F; :: thesis: ( f is bijective & f is isometric implies f is midpoints-preserving )
assume that
A1: f is bijective and
A2: f is isometric ; :: thesis: f is midpoints-preserving
let a, b be Point of E; :: according to MAZURULM:def 3 :: thesis: f . ((1 / 2) * (a + b)) = (1 / 2) * ((f . a) + (f . b))
set W = H₁(E,a,b);
set l = H₂(E,a,b);
set z = (1 / 2) * (a + b);
set z1 = (1 / 2) * ((f . a) + (f . b));
set R = ((1 / 2) * (a + b)) -reflection ;
set R1 = ((1 / 2) * ((f . a) + (f . b))) -reflection ;
set h = (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f;
then reconsider l = H₂(E,a,b) as real-membered set by MEMBERED:def 3;
A3: rng f = [#] F by A1, FUNCT_2:def 3;
A4: f /" = f " by A1, TOPS_2:def 4;
then A5: f /" is bijective by A1, GROUP_6:63;
(((1 / 2) * (a + b)) -reflection) * (f /") is onto by A5, FUNCT_2:27;
then ((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection) is onto by FUNCT_2:27;
then A6: (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f is onto by A1, FUNCT_2:27;
f /" is isometric by A1, A2, Th12;
then (((1 / 2) * (a + b)) -reflection) * (f /") is isometric by Th11;
then ((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection) is isometric by Th11;
then A7: (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f is isometric by A2, Th11;
A8: 2 * ((1 / 2) * (a + b)) = (2 * (1 / 2)) * (a + b) by RLVECT_1:def 7
.= a + b by RLVECT_1:def 8 ;
then A9: (2 * ((1 / 2) * (a + b))) - a = b by Th4;
A10: (2 * ((1 / 2) * (a + b))) - b = a by A8, Th4;
A11: 2 * ((1 / 2) * ((f . a) + (f . b))) = (2 * (1 / 2)) * ((f . a) + (f . b)) by RLVECT_1:def 7
.= (f . a) + (f . b) by RLVECT_1:def 8 ;
then A12: (2 * ((1 / 2) * ((f . a) + (f . b)))) - (f . a) = f . b by Th4;
A13: (2 * ((1 / 2) * ((f . a) + (f . b)))) - (f . b) = f . a by A11, Th4;
A14: ((((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f) . a = (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) . (f . a) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (f /")) . ((((1 / 2) * ((f . a) + (f . b))) -reflection) . (f . a)) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (f /")) . (f . b) by A12, Def4
.= (((1 / 2) * (a + b)) -reflection) . ((f /") . (f . b)) by FUNCT_2:15
.= (((1 / 2) * (a + b)) -reflection) . b by A4, A1, FUNCT_2:26
.= a by A10, Def4 ;
((((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f) . b = (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) . (f . b) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (f /")) . ((((1 / 2) * ((f . a) + (f . b))) -reflection) . (f . b)) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (f /")) . (f . a) by A13, Def4
.= (((1 / 2) * (a + b)) -reflection) . ((f /") . (f . a)) by FUNCT_2:15
.= (((1 / 2) * (a + b)) -reflection) . a by A4, A1, FUNCT_2:26
.= b by A9, Def4 ;
then A15: (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f in H₁(E,a,b) by A4, A1, A6, A7, A14;
rng (((1 / 2) * (a + b)) -reflection) = [#] E by FUNCT_2:def 3;
then A16: ((((1 / 2) * (a + b)) -reflection) /") * (((1 / 2) * (a + b)) -reflection) = id (dom (((1 / 2) * (a + b)) -reflection)) by TOPS_2:52
.= id E by FUNCT_2:def 1 ;
A17: f * (f /") = id F by A1, A3, TOPS_2:52;
A18: ((((1 / 2) * (a + b)) -reflection) /") * ((((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f) = ((((1 / 2) * (a + b)) -reflection) /") * (((((1 / 2) * (a + b)) -reflection) * (f /")) * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f)) by RELAT_1:36
.= ((((1 / 2) * (a + b)) -reflection) /") * ((((1 / 2) * (a + b)) -reflection) * ((f /") * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f))) by RELAT_1:36
.= (((((1 / 2) * (a + b)) -reflection) /") * (((1 / 2) * (a + b)) -reflection)) * ((f /") * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f)) by RELAT_1:36
.= ((((((1 / 2) * (a + b)) -reflection) /") * (((1 / 2) * (a + b)) -reflection)) * (f /")) * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f) by RELAT_1:36
.= (((((((1 / 2) * (a + b)) -reflection) /") * (((1 / 2) * (a + b)) -reflection)) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f by RELAT_1:36
.= ((f /") * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f by A16, FUNCT_2:17 ;
A19: f * (((f /") * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f) = f * ((f /") * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f)) by RELAT_1:36
.= (f * (f /")) * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f) by RELAT_1:36
.= (((1 / 2) * ((f . a) + (f . b))) -reflection) * f by A17, FUNCT_2:17 ;
l = H₂(E,a,b) ;
then ((((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f) . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) by A15, Lm7;
then (((((1 / 2) * (a + b)) -reflection) /") * ((((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f)) . ((1 / 2) * (a + b)) = ((((1 / 2) * (a + b)) -reflection) /") . ((1 / 2) * (a + b)) by FUNCT_2:15;
then A20: (f * (((f /") * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f)) . ((1 / 2) * (a + b)) = f . (((((1 / 2) * (a + b)) -reflection) /") . ((1 / 2) * (a + b))) by A18, FUNCT_2:15
.= (f * ((((1 / 2) * (a + b)) -reflection) /")) . ((1 / 2) * (a + b)) by FUNCT_2:15 ;
(((1 / 2) * ((f . a) + (f . b))) -reflection) . (f . ((1 / 2) * (a + b))) = ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f) . ((1 / 2) * (a + b)) by FUNCT_2:15
.= (f * (((1 / 2) * (a + b)) -reflection)) . ((1 / 2) * (a + b)) by A20, A19, Th23
.= f . ((((1 / 2) * (a + b)) -reflection) . ((1 / 2) * (a + b))) by FUNCT_2:15
.= f . ((1 / 2) * (a + b)) by Th18 ;
hence f . ((1 / 2) * (a + b)) = (1 / 2) * ((f . a) + (f . b)) by Th18; :: thesis: verum