let f be Function of E,F; ( f is bijective & f is isometric implies f is midpoints-preserving )
assume that
A1:
f is bijective
and
A2:
f is isometric
; f is midpoints-preserving
let a, b be Point of E; MAZURULM:def 3 f . ((1 / 2) * (a + b)) = (1 / 2) * ((f . a) + (f . b))
set W = H1(E,a,b);
set l = H2(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 = H2(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 H1(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 = H2(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; verum