:: Mazur-Ulam Theorem
::  by Artur Korni{\l}owicz
::
:: Received December 21, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, NORMSP_1, VECTMETR, PRE_TOPC, ARYTM_1, RUSUB_4, XREAL_0,
      CARD_1, XXREAL_0, RELAT_1, ARYTM_3, FUNCT_2, SEQ_2, MEMBERED, ORDINAL2,
      MAZURULM, BINOP_1, VALUED_1, SUPINF_2, COMPLEX1, SUBSET_1, XXREAL_2,
      XBOOLE_0, NUMBERS, MEMBER_1, SUPINF_1, TARSKI, RLVECT_1, CFCONT_1, NAT_1,
      PARTFUN1, REAL_1, NEWTON, TOPMETR, BORSUK_1, TOPS_1, XXREAL_1, URYSOHN1,
      METRIC_1, STRUCT_0, SEQ_1, FUNCOP_1, RCOMP_1, XCMPLX_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_1, XXREAL_3,
      XREAL_0, REAL_1, XXREAL_2, MEMBERED, VALUED_1, SEQ_1, SEQ_2, COMPLEX1,
      MEMBER_1, SUPINF_1, NEWTON, MEASURE6, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2,
      BORSUK_1, METRIC_1, TOPMETR, ALGSTR_0, RLVECT_1, NORMSP_0, NORMSP_1,
      NDIFF_1, NFCONT_1, CONNSP_3, URYSOHN1;
 constructors TOPS_2, REAL_1, SUPINF_2, INTEGRA2, EXTREAL1, BINOP_2, NFCONT_1,
      NEWTON, CONNSP_3, URYSOHN1, TOPS_1, TOPMETR, PCOMPS_1, MEASURE6, NDIFF_1,
      COMSEQ_2;
 registrations RELSET_1, XREAL_0, ORDINAL1, STRUCT_0, MEMBERED, FUNCT_1,
      FUNCT_2, XBOOLE_0, NORMSP_1, FUNCTOR1, NUMBERS, SEQ_4, XXREAL_2,
      MEMBER_1, XXREAL_0, RLVECT_1, TOPS_1, TOPMETR, METRIC_1, XXREAL_1,
      VALUED_1, VALUED_0, FUNCOP_1, BORSUK_1, INT_1, NEWTON, XXREAL_3, SEQ_1,
      SEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

:: Mazur-Ulam Theorem
:: cluster bijective isometric -> Affine Function of E,F;
:: is a consequence of two registrations:
:: cluster bijective isometric -> midpoints-preserving Function of E,F;
:: cluster isometric midpoints-preserving -> Affine Function of E,F;

reserve E,F,G for RealNormSpace;
reserve f for Function of E,F;
reserve g for Function of F,G;
reserve a,b,c for Point of E;
reserve t for Real;

registration
  cluster I[01] -> closed for SubSpace of R^1;
end;

theorem :: MAZURULM:1
  DYADIC is dense Subset of I[01];

theorem :: MAZURULM:2
  Cl DYADIC = [. 0,1 .];

theorem :: MAZURULM:3
  a + a = 2*a;

theorem :: MAZURULM:4
  a + b - b = a;

registration
  let A be bounded_above real-membered set;
  let r be non negative Real;
  cluster r**A -> bounded_above;
end;

registration
  let A be bounded_above real-membered set;
  let r be non positive Real;
  cluster r**A -> bounded_below;
end;

registration
  let A be bounded_below real-membered set;
  let r be non negative Real;
  cluster r**A -> bounded_below;
end;

registration
  let A be bounded_below non empty real-membered set;
  let r be non positive Real;
  cluster r**A -> bounded_above;
end;

theorem :: MAZURULM:5
  for f being Real_Sequence holds f + (NAT --> t) = t + f;

theorem :: MAZURULM:6
  for r being Element of REAL holds lim (NAT --> r) = r;

theorem :: MAZURULM:7
  for f being convergent Real_Sequence holds
  lim (t + f) = t + lim f;

registration
  let f be convergent Real_Sequence;
  let t;
  cluster t + f -> convergent for Real_Sequence;
end;

theorem :: MAZURULM:8
  for f be Real_Sequence holds f (#) (NAT --> a) = f * a;

theorem :: MAZURULM:9
  lim (NAT --> a) = a;

theorem :: MAZURULM:10
  for f being convergent Real_Sequence holds
  lim (f * a) = (lim f) * a;

registration
  let f be convergent Real_Sequence;
  let E,a;
  cluster f * a -> convergent;
end;

definition
  let E,F be non empty NORMSTR, f be Function of E,F;
  attr f is isometric means
:: MAZURULM:def 1
  for a,b being Point of E holds ||. f.a - f.b .|| = ||. a - b .||;
end;

definition
  let E,F be non empty RLSStruct, f be Function of E,F;

  attr f is Affine means
:: MAZURULM:def 2
  for a,b being Point of E, t being Real st 0 <= t & t <= 1 holds
  f.((1-t)*a+t*b) = (1-t)*(f.a) + t*(f.b);

  attr f is midpoints-preserving means
:: MAZURULM:def 3
  for a,b being Point of E holds f.(1/2*(a+b)) = 1/2*(f.a+f.b);
end;

registration
  let E be non empty NORMSTR;
  cluster id E -> isometric;
end;

registration
  let E be non empty RLSStruct;
  cluster id E -> midpoints-preserving Affine;
end;

registration
  let E be non empty NORMSTR;
  cluster bijective isometric midpoints-preserving Affine for UnOp of E;
end;

theorem :: MAZURULM:11
  f is isometric & g is isometric implies g*f is isometric;

registration
  let E; let f,g be isometric UnOp of E;
  cluster g*f -> isometric for UnOp of E;
end;

theorem :: MAZURULM:12
  f is bijective isometric implies f/" is isometric;

registration
  let E; let f be bijective isometric UnOp of E;
  cluster f/" -> isometric;
end;

theorem :: MAZURULM:13
  f is midpoints-preserving & g is midpoints-preserving implies
  g*f is midpoints-preserving;

registration
  let E; let f,g be midpoints-preserving UnOp of E;
  cluster g*f -> midpoints-preserving for UnOp of E;
end;

theorem :: MAZURULM:14
  f is bijective midpoints-preserving implies f/" is midpoints-preserving;

registration
  let E; let f be bijective midpoints-preserving UnOp of E;
  cluster f/" -> midpoints-preserving;
end;

theorem :: MAZURULM:15
  f is Affine & g is Affine implies g*f is Affine;

registration
  let E; let f,g be Affine UnOp of E;
  cluster g*f -> Affine for UnOp of E;
end;

theorem :: MAZURULM:16
  f is bijective Affine implies f/" is Affine;

registration
  let E; let f be bijective Affine UnOp of E;
  cluster f/" -> Affine;
end;

definition
  let E be non empty RLSStruct, a be Point of E;
  func a-reflection -> UnOp of E means
:: MAZURULM:def 4
  for b being Point of E holds it.b = 2*a - b;
end;

theorem :: MAZURULM:17
  (a-reflection) * (a-reflection) = id E;

registration
  let E,a;
  cluster a-reflection -> bijective;
end;

theorem :: MAZURULM:18  :: a is the only fixed point of R
  (a-reflection).a = a & for b st (a-reflection).b = b holds a = b;

theorem :: MAZURULM:19
  (a-reflection).b - a = a - b;

theorem :: MAZURULM:20
  ||. (a-reflection).b - a .|| = ||. b - a .||;

theorem :: MAZURULM:21
  (a-reflection).b - b = 2 * (a - b);

theorem :: MAZURULM:22
  ||. (a-reflection).b - b .|| = 2 * ||. b - a .||;

theorem :: MAZURULM:23
  (a-reflection)/" = a-reflection;

registration
  let E,a;
  cluster a-reflection -> isometric;
end;

theorem :: MAZURULM:24
  f is isometric implies f is_continuous_on dom f;

registration
  let E,F;
  cluster bijective isometric -> midpoints-preserving for Function of E,F;
 end;

registration
  let E,F;
  cluster isometric midpoints-preserving -> Affine for Function of E,F;
end;