The book "Classical Geometries in Modern Contexts", by Walter Benz,
subtitled "Geometry of Real Inner Product Spaces", seems to use mainly
constructive methods.
To make it fully constructive, we introduce the needed separation
primitives into the definition of real inner product space.

So far, we have proved such theorems as
implies-isometry which is Schroeder and Benz's
version of the Benedick Quarles theorem. It is fully constructive.


Definition: real-vector-space
RealVectorSpace ==
  "+":{f:Point(self) ⟶ Point(self) ⟶ Point(self)| 
       (∀x,y,z:Point(self).  (f z) ≡ (f y) z) ∧ (∀x,y:Point(self).  y ≡ x)} 
  "+sep":∀x,x',y,y':Point(self).  (self."+" self."+" x' y'  (x x' ∨ y'))
  "*":{m:ℝ ⟶ Point(self) ⟶ Point(self)| 
       (∀a:ℝ. ∀x,y:Point(self).  (self."+" y) ≡ self."+" (m x) (m y))
       ∧ (∀x:Point(self)
            (m r1 x ≡ x
            ∧ r0 x ≡ self."0"
            ∧ (∀a,b:ℝ.  (m x) ≡ (a b) x)
            ∧ (∀a,b:ℝ.  (a b) x ≡ self."+" (m x) (m x))))} 
  "*sep":∀a,b:ℝ. ∀x,y:Point(self).  (self."*" self."*"  (a ≠ b ∨ y))

Lemma: real-vector-space_wf
RealVectorSpace ∈ 𝕌'

Lemma: real-vector-space_subtype1
RealVectorSpace ⊆SeparationSpace

Definition: mk-real-vector-space
ss=ss;0=z;+=p;*=m;+sep=psep;*sep=msep ==  ss["0" := z]["+" := p]["*" := m]["+sep" := psep]["*sep" := msep]

Lemma: mk-real-vector-space_wf
[self:SeparationSpace]. ∀[z:Point(self)]. ∀[p:{f:Point(self) ⟶ Point(self) ⟶ Point(self)| 
                                                (∀x,y,z:Point(self).  (f z) ≡ (f y) z)
                                                ∧ (∀x,y:Point(self).  y ≡ x)} ].
[m:{m:ℝ ⟶ Point(self) ⟶ Point(self)| 
     (∀a:ℝ. ∀x,y:Point(self).  (p y) ≡ (m x) (m y))
     ∧ (∀x:Point(self)
          (m r1 x ≡ x
          ∧ r0 x ≡ z
          ∧ (∀a,b:ℝ.  (m x) ≡ (a b) x)
          ∧ (∀a,b:ℝ.  (a b) x ≡ (m x) (m x))))} ]. ∀[psep:∀x,x',y,y':Point(self).
                                                                     (p x' y'  (x x' ∨ y'))].
[msep:∀a,b:ℝ. ∀x,y:Point(self).  (m  (a ≠ b ∨ y))].
   *sep=msep ∈ RealVectorSpace)

Definition: rv-0
==  rv."0"

Lemma: rv-0_wf
[rv:RealVectorSpace]. (0 ∈ Point(rv))

Definition: rv-add
==  rv."+" y

Lemma: rv-add_wf
[rv:RealVectorSpace]. ∀[x,y:Point(rv)].  (x y ∈ Point(rv))

Lemma: rv-add-sep
rv:RealVectorSpace. ∀x,x',y,y':Point(rv).  (x x' y'  (x x' ∨ y'))

Lemma: rv-add-sep1
rv:RealVectorSpace. ∀x,x',y:Point(rv).  (x x'  x')

Lemma: rv-add-sep2
rv:RealVectorSpace. ∀x,x',y:Point(rv).  (y x'  x')

Lemma: rv-add_functionality
[rv:RealVectorSpace]. ∀[x,y,x',y':Point(rv)].  (x y ≡ x' y') supposing (y ≡ y' and x ≡ x')

Lemma: rv-add-assoc
[rv:RealVectorSpace]. ∀[x,y,z:Point(rv)].  z ≡ z

Lemma: rv-add-comm
[rv:RealVectorSpace]. ∀[x,y:Point(rv)].  y ≡ x

Lemma: rv-add-swap
[rv:RealVectorSpace]. ∀[x,y,z:Point(rv)].  z ≡ y

Definition: rv-mul
a*x ==  rv."*" x

Lemma: rv-mul_wf
[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x:Point(rv)].  (a*x ∈ Point(rv))

Lemma: rv-mul-sep
rv:RealVectorSpace. ∀a,b:ℝ. ∀x,y:Point(rv).  (a*x b*y  (a ≠ b ∨ y))

Lemma: rv-mul-sep1
rv:RealVectorSpace. ∀a,b:ℝ. ∀y:Point(rv).  (a*y b*y  a ≠ b)

Lemma: rv-mul-sep2
rv:RealVectorSpace. ∀a:ℝ. ∀x,y:Point(rv).  (a*x a*y  y)

Lemma: rv-mul1
[rv:RealVectorSpace]. ∀[x:Point(rv)].  r1*x ≡ x

Lemma: rv-mul0
[rv:RealVectorSpace]. ∀[x:Point(rv)].  r0*x ≡ 0

Lemma: rv-mul_functionality
[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x,x':Point(rv)].  (a*x ≡ b*x') supposing (x ≡ x' and (a b))

Lemma: rv-mul-linear
[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x,y:Point(rv)].  a*x y ≡ a*x a*y

Lemma: rv-mul-mul
[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x:Point(rv)].  a*b*x ≡ b*x

Lemma: rv-mul-add
[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x:Point(rv)].  a*x b*x ≡ b*x

Lemma: rv-mul-add-alt
[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x,u:Point(rv)].  a*x b*x ≡ b*x

Lemma: rv-mul-add-1
[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x:Point(rv)].  a*x x ≡ r1*x

Lemma: rv-mul-add-1-alt
[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x,u:Point(rv)].  a*x x ≡ r1*x

Lemma: rv-mul-1-add
[rv:RealVectorSpace]. ∀[b:ℝ]. ∀[x:Point(rv)].  b*x ≡ r1 b*x

Lemma: rv-mul-1-add-alt
[rv:RealVectorSpace]. ∀[b:ℝ]. ∀[x,u:Point(rv)].  b*x ≡ r1 b*x

Lemma: rv-mul-0
[rv:RealVectorSpace]. ∀[a:ℝ].  a*0 ≡ 0

Definition: rv-minus
-x ==  r(-1)*x

Lemma: rv-minus_wf
[rv:RealVectorSpace]. ∀[x:Point(rv)].  (-x ∈ Point(rv))

Lemma: rv-minus_functionality
[rv:RealVectorSpace]. ∀[x,x':Point(rv)].  -x ≡ -x' supposing x ≡ x'

Lemma: rv-add-minus
[rv:RealVectorSpace]. ∀[x:Point(rv)].  -x x ≡ 0

Lemma: rv-add-minus2
[rv:RealVectorSpace]. ∀[x:Point(rv)].  -x ≡ 0

Lemma: rv-add-0
[rv:RealVectorSpace]. ∀[x:Point(rv)].  x ≡ x

Lemma: rv-0-add
[rv:RealVectorSpace]. ∀[x:Point(rv)].  0 ≡ x

Lemma: rv-add-cancel-left
[rv:RealVectorSpace]. ∀[x,y,z:Point(rv)].  uiff(x y ≡ z;y ≡ z)

Lemma: rv-add-cancel-right
[rv:RealVectorSpace]. ∀[x,y,z:Point(rv)].  uiff(y x ≡ x;y ≡ z)

Lemma: rv-mul-cancel
[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x,y:Point(rv)].  uiff(a*x ≡ a*y;x ≡ y) supposing a ≠ r0

Definition: inner-product-space
InnerProductSpace ==
  "ip":{ip:Point(self) ⟶ Point(self) ⟶ ℝ
        (∀x1,x2,y1,y2:Point(self).  (x1 ≡ x2  y1 ≡ y2  ((ip x1 y1) (ip x2 y2))))
        ∧ (∀x,y:Point(self).  ((ip y) (ip x)))
        ∧ (∀x,y,z:Point(self).  ((ip z) ((ip z) (ip z))))
        ∧ (∀a:ℝ. ∀x,y:Point(self).  ((ip a*x y) (a (ip y))))} 
  "positive":∀x:Point(self). (x ⇐⇒ r0 < (self."ip" x))
  "perp":∀x:Point(self). (x  (∃y:Point(self). (y 0 ∧ ((self."ip" y) r0))))

Lemma: inner-product-space_wf
InnerProductSpace ∈ 𝕌'

Lemma: inner-product-space_subtype
InnerProductSpace ⊆RealVectorSpace

Definition: mk-inner-product-space
vs=vs;ip=ip;positive=pos;perp=perp ==  vs["ip" := ip]["positive" := pos]["perp" := perp]

Lemma: mk-inner-product-space_wf
[self:RealVectorSpace]. ∀[ip:{ip:Point(self) ⟶ Point(self) ⟶ ℝ
                               (∀x1,x2,y1,y2:Point(self).  (x1 ≡ x2  y1 ≡ y2  ((ip x1 y1) (ip x2 y2))))
                               ∧ (∀x,y:Point(self).  ((ip y) (ip x)))
                               ∧ (∀x,y,z:Point(self).  ((ip z) ((ip z) (ip z))))
                               ∧ (∀a:ℝ. ∀x,y:Point(self).  ((ip a*x y) (a (ip y))))} ]. ∀[pos:∀x:Point(self)
                                                                                                     (x 0
                                                                                                     ⇐⇒ r0 < (ip 
[perp:∀x:Point(self). (x  (∃y:Point(self). (y 0 ∧ ((ip y) r0))))].
   perp=perp ∈ InnerProductSpace)

Definition: rn-ss
sepℝ^n ==  Point=ℝ^n #=λx,y. x ≠ cotrans=TERMOF{real-vec-sep-cases-alt:o, 1:l} n

Lemma: rn-ss_wf
[n:ℕ]. (sepℝ^n ∈ SeparationSpace)

Definition: rv-n
vecℝ^n ==
  +=λx,y. y;
  *=λa,y. a*y;
  +sep=TERMOF{real-vec-sep-add:o, 1:l} n;
  *sep=TERMOF{real-vec-sep-mul:o, 1:l} n

Lemma: rv-n_wf
[n:ℕ]. (vecℝ^n ∈ RealVectorSpace)

Definition: rn-ip
ipℝ^n ==  vs=vecℝ^n;ip=λx,y. x⋅y;positive=TERMOF{real-vec-sep-0-iff:o, 1:l} n;perp=TERMOF{real-vec-perp-exists:o, 1:l} n

Lemma: rn-ip_wf
[n:{2...}]. (ipℝ^n ∈ InnerProductSpace)

Definition: rv-ip
x ⋅ ==  rv."ip" y

Lemma: rv-ip_wf
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (x ⋅ y ∈ ℝ)

Lemma: rv-ip_functionality
[rv:InnerProductSpace]. ∀[x1,x2,y1,y2:Point(rv)].  (x1 ⋅ y1 x2 ⋅ y2) supposing (y1 ≡ y2 and x1 ≡ x2)

Lemma: rv-ip-symmetry
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (x ⋅ y ⋅ x)

Lemma: rv-ip-add
[rv:InnerProductSpace]. ∀[x,y,z:Point(rv)].  (x y ⋅ (x ⋅ y ⋅ z))

Lemma: rv-ip-add2
[rv:InnerProductSpace]. ∀[x,y,z:Point(rv)].  (z ⋅ (z ⋅ z ⋅ y))

Lemma: rv-ip-mul
[rv:InnerProductSpace]. ∀[a:ℝ]. ∀[x,y:Point(rv)].  (a*x ⋅ (a x ⋅ y))

Lemma: rv-ip-mul2
[rv:InnerProductSpace]. ∀[a:ℝ]. ∀[x,y:Point(rv)].  (y ⋅ a*x (a y ⋅ x))

Lemma: rv-ip-positive
rv:InnerProductSpace. ∀x:Point(rv).  (x ⇐⇒ r0 < x^2)

Lemma: rv-ip0
[rv:InnerProductSpace]. ∀[x:Point(rv)].  (x ⋅ r0)

Lemma: rv-0ip
[rv:InnerProductSpace]. ∀[x:Point(rv)].  (0 ⋅ r0)

Lemma: rv-ip-nonneg
[rv:InnerProductSpace]. ∀[x:Point(rv)].  (r0 ≤ x^2)

Lemma: rsqrt-1-plus-ip-positive
rv:InnerProductSpace. ∀h:Point(rv).  (r0 < rsqrt(r1 h^2))

Lemma: rv-ip-minus
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (-x ⋅ -(x ⋅ y))

Lemma: rv-ip-minus2
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (x ⋅ -y -(x ⋅ y))

Definition: rv-sub
==  -y

Lemma: rv-sub_wf
[rv:RealVectorSpace]. ∀[x,y:Point(rv)].  (x y ∈ Point(rv))

Lemma: rv-sub_functionality
[rv:RealVectorSpace]. ∀[x,y,x',y':Point(rv)].  (x y ≡ x' y') supposing (y ≡ y' and x ≡ x')

Lemma: rv-sub-is-zero
[rv:RealVectorSpace]. ∀[x,y:Point(rv)].  uiff(x y ≡ 0;x ≡ y)

Lemma: rv-sub0
[rv:RealVectorSpace]. ∀[x:Point(rv)].  0 ≡ x

Lemma: rv-sub-same
[rv:RealVectorSpace]. ∀[x:Point(rv)].  x ≡ 0

Lemma: rv-sub-sep
rv:RealVectorSpace. ∀x,x',y,y':Point(rv).  (x x' y'  (x x' ∨ y'))

Lemma: rv-mul-sub
[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x:Point(rv)].  b*x ≡ a*x b*x

Lemma: rv-mul-rv-sub
[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x,y:Point(rv)].  a*x y ≡ a*x a*y

Lemma: rv-ip-sub
[rv:InnerProductSpace]. ∀[x,y,z:Point(rv)].  (x y ⋅ (x ⋅ y ⋅ z))

Lemma: rv-ip-sub2
[rv:InnerProductSpace]. ∀[x,y,z:Point(rv)].  (z ⋅ (z ⋅ z ⋅ y))

Lemma: rv-sub-add
[rv:InnerProductSpace]. ∀[x,v:Point(rv)].  v ≡ x

Lemma: rv-ip-sub-squared
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (x y^2 ((x^2 r(2) x ⋅ y) y^2))

Lemma: rv-ip-add-squared
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (x y^2 ((x^2 (r(2) x ⋅ y)) y^2))

Lemma: rv-ip-zero-iff
[rv:InnerProductSpace]. ∀[x:Point(rv)].  uiff(x^2 r0;x ≡ 0)

Lemma: rv-sep-iff
rv:InnerProductSpace. ∀x,y:Point(rv).  (x ⇐⇒ 0)

Lemma: rv-sep-iff-ext
rv:InnerProductSpace. ∀x,y:Point(rv).  (x ⇐⇒ 0)

Definition: rv-norm
||x|| ==  rsqrt(x^2)

Lemma: rv-norm_wf
[rv:InnerProductSpace]. ∀[x:Point(rv)].  (||x|| ∈ {r:ℝ(r0 ≤ r) ∧ ((r r) x^2)} )

Lemma: rv-norm_functionality
[rv:InnerProductSpace]. ∀[x1,x2:Point(rv)].  ||x1|| ||x2|| supposing x1 ≡ x2

Lemma: rv-norm0
[rv:InnerProductSpace]. (||0|| r0)

Lemma: rv-norm-nonneg
[rv:InnerProductSpace]. ∀[x:Point(rv)].  (r0 ≤ ||x||)

Lemma: rv-norm-positive
rv:InnerProductSpace. ∀x:Point(rv).  (x  (r0 < ||x||))

Lemma: rv-norm-squared
[rv:InnerProductSpace]. ∀[x:Point(rv)].  (||x||^2 x^2)

Lemma: rv-norm-eq-iff
[rv:InnerProductSpace]. ∀[x:Point(rv)]. ∀[r:ℝ].  uiff(||x|| r;x^2 r^2) supposing r0 ≤ r

Lemma: rv-norm-equal-iff
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  uiff(||x|| ||y||;x^2 y^2)

Lemma: rv-norm-difference-symmetry
[rv:InnerProductSpace]. ∀[a,b:Point(rv)].  (||a b|| ||b a||)

Lemma: rv-norm-is-zero
[rv:InnerProductSpace]. ∀[x:Point(rv)].  uiff(||x|| r0;x ≡ 0)

Lemma: rv-norm-positive-iff
rv:InnerProductSpace. ∀x:Point(rv).  (x ⇐⇒ r0 < ||x||)

Lemma: rv-norm-positive-iff-ext
rv:InnerProductSpace. ∀x:Point(rv).  (x ⇐⇒ r0 < ||x||)

Lemma: rv-sep-iff-norm
rv:InnerProductSpace. ∀x,y:Point(rv).  (x ⇐⇒ r0 < ||x y||)

Lemma: rv-sep-shift
rv:InnerProductSpace. ∀a,p,q:Point(rv).  (p  a)

Lemma: rv-sep-shift2
rv:InnerProductSpace. ∀a,p,q:Point(rv).  (p  a)

Lemma: sq_stable__rv-sep
rv:InnerProductSpace. ∀x,y:Point(rv).  SqStable(x y)

Lemma: sq_stable__rv-sep-ext
rv:InnerProductSpace. ∀x,y:Point(rv).  SqStable(x y)

Lemma: rv-sep-or
rv:InnerProductSpace. ∀a:Point(rv). ∀b:{b:Point(rv)| b} . ∀c:Point(rv).  (a c ∨ c)

Definition: rv-sep-witness
rv-sep-witness(rv;x;y) ==
  case rv."+sep" -y -y 
       case rv."#or" -y -y 
            case rv."#or" -y -y 
                 let _,p rv."positive" 
                 in ((((rlessw(r0^2;||x y||^2) 20) 1) 20) 1)
             of inl(_) =>
             inr(b) =>
             case rv."#or" -y of inl(_) => Ax inr(a) => a
        of inl(_) =>
        inr(b) =>
        case rv."#or" -y -y of inl(_) => Ax inr(a) => a
   of inl(_) =>
   inr(a) =>

Lemma: rv-sep-witness_wf
rv:InnerProductSpace. ∀x:Point(rv). ∀y:{y:Point(rv)| y} .  (rv-sep-witness(rv;x;y) ∈ y)

Lemma: rv-norm-mul
[rv:InnerProductSpace]. ∀[x:Point(rv)]. ∀[a:ℝ].  (||a*x|| (|a| ||x||))

Lemma: rv-norm-sub
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (||x y|| ||y x||)

Lemma: rv-mul-sep-zero
rv:InnerProductSpace. ∀t:ℝ. ∀x:Point(rv).  (t*x ⇐⇒ 0 ∧ (r0 < |t|))

Lemma: rv-mul-sep-iff
rv:InnerProductSpace. ∀a,b:ℝ. ∀y:Point(rv).  (a*y b*y ⇐⇒ a ≠ b ∧ 0)

Lemma: rv-add-sep-iff
rv:InnerProductSpace. ∀a,b,h:Point(rv).  (h ⇐⇒ b)

Definition: rv-unit
rv-unit(rv;x) ==  (r1/||x||)*x

Lemma: rv-unit_wf
[rv:InnerProductSpace]. ∀[x:Point(rv)].  rv-unit(rv;x) ∈ {z:Point(rv)| z^2 r1}  supposing 0

Lemma: rv-unit-squared
[rv:InnerProductSpace]. ∀[x:Point(rv)].  rv-unit(rv;x)^2 r1 supposing 0

Lemma: rv-unit-property
rv:InnerProductSpace. ∀x:Point(rv).  (x  (∃t:ℝ(t ≠ r0 ∧ rv-unit(rv;x) ≡ t*x)))

Lemma: rv-perp-1
rv:InnerProductSpace. ∀x:Point(rv).  (x  (∃y:Point(rv). ((y^2 r1) ∧ (x ⋅ r0))))

Lemma: rv-perp-same-norm
rv:InnerProductSpace. ∀x:Point(rv).  (x  (∃y:Point(rv). ((||y|| ||x||) ∧ (x ⋅ r0))))

Lemma: rv-Cauchy-Schwarz
[rv:InnerProductSpace]. ∀[a,b:Point(rv)].  (a ⋅ b^2 ≤ (a^2 b^2))

Lemma: rv-Cauchy-Schwarz'
[rv:InnerProductSpace]. ∀[a,b:Point(rv)].  (|a ⋅ b| ≤ (||a|| ||b||))

Lemma: rv-ip-rleq
[rv:InnerProductSpace]. ∀[a,b:Point(rv)].  (a ⋅ b ≤ (||a|| ||b||))

Lemma: rv-ip-rneq-0
rv:InnerProductSpace. ∀a,b:Point(rv).  (a ⋅ b ≠ r0  (a 0 ∧ 0))

Lemma: rv-ip-rneq
rv:InnerProductSpace. ∀a1,b1,a2,b2:Point(rv).  (a1 ⋅ b1 ≠ a2 ⋅ b2  (a1 a2 ∨ b1 b2))

Lemma: rv-norm-triangle-inequality
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (||x y|| ≤ (||x|| ||y||))

Lemma: rv-norm-triangle-inequality2
[rv:InnerProductSpace]. ∀[x,y,z:Point(rv)].  (||x z|| ≤ (||x y|| ||y z||))

Lemma: rv-Cauchy-Schwarz-equality
rv:InnerProductSpace. ∀a,b:Point(rv).  ((a ⋅ b^2 (a^2 b^2))   (∃t:ℝa ≡ t*b))

Lemma: rv-Cauchy-Schwarz-equality'
rv:InnerProductSpace. ∀a,b:Point(rv).  ((|a ⋅ b| (||a|| ||b||))   (∃t:ℝa ≡ t*b))

Definition: rv-orthogonal
Orthogonal(f) ==  (∀x,y:Point(rv).  (f y ≡ y ∧ (x ⋅ x ⋅ y))) ∧ (∀x:Point(rv). ∀a:ℝ.  a*x ≡ a*f x)

Lemma: rv-orthogonal_wf
[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Orthogonal(f) ∈ ℙ)

Lemma: sq_stable__rv-orthogonal
[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). SqStable(Orthogonal(f))

Lemma: rv-orthogonal-injective
[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Orthogonal(f)  (∀x,y:Point(rv).  (f x ≡  x ≡ y)))

Lemma: rv-orthogonal-iff-norm-preserving
  ∀f:Point(rv) ⟶ Point(rv)
    ⇐⇒ (∀x,y:Point(rv).  y ≡ y) ∧ (∀x:Point(rv). ((∀a:ℝa*x ≡ a*f x) ∧ (||f x|| ||x||))))

Definition: rv-isometry
Isometry(f) ==  ∀[x,y:Point(rv)].  (||f y|| ||x y||)

Lemma: rv-isometry_wf
[rv:InnerProductSpace]. ∀[f:Point(rv) ⟶ Point(rv)].  (Isometry(f) ∈ ℙ)

Lemma: sq_stble__rv-isometry
[rv:InnerProductSpace]. ∀[f:Point(rv) ⟶ Point(rv)].  SqStable(Isometry(f))

Lemma: rv-orthogonal-isometry
[rv:InnerProductSpace]. ∀[f:Point(rv) ⟶ Point(rv)].  Isometry(f) supposing Orthogonal(f)

Lemma: rv-isometry-implies-extensional
rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv).  ∀x,y:Point(rv).  (f  y) supposing Isometry(f)

Lemma: rv-isometry-injective
[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Isometry(f)  (∀x,y:Point(rv).  (f x ≡  x ≡ y)))

Lemma: rv-orthogonal-implies-extensional
rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv).  ∀x,y:Point(rv).  (f  y) supposing Orthogonal(f)

Lemma: rv-orthogonal-implies-extensional-ext
rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv).  ∀x,y:Point(rv).  (f  y) supposing Orthogonal(f)

Definition: rv-orthog-ext
rv-orthog-ext(rv;f) ==
  λx,y,_. case rv."+sep" -y -y 
               case rv."#or" -y -y 
                    case rv."#or" -y -y 
                         let _,h rv."positive" 
                         in ((((rlessw(r0^2;||x y||^2) 20) 1) 20) 1)
                     of inl(_) =>
                     inr(a) =>
                     case rv."#or" -y of inl(_) => Ax inr(x) => x
                of inl(_) =>
                inr(a) =>
                case rv."#or" -y -y of inl(_) => Ax inr(x) => x
          of inl(_) =>
          inr(x) =>

Lemma: rv-orthog-ext_wf
rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv).
  rv-orthog-ext(rv;f) ∈ ∀x,y:Point(rv).  (f  y) supposing Orthogonal(f)

Lemma: rv-isometry-implies-functional
[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Isometry(f)  (∀x,y:Point(rv).  (x ≡  x ≡ y)))

Lemma: rv-orthogonal-implies-functional
[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Orthogonal(f)  (∀x,y:Point(rv).  (x ≡  x ≡ y)))

Lemma: rv-midpoint-unique
rv:InnerProductSpace. ∀a,b,m:Point(rv).
  ((||m a|| (||b a||/r(2))) ∧ (||m b|| (||b a||/r(2))) ⇐⇒ m ≡ (r1/r(2))*a b)

Lemma: rv-orthogonal-iff
[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Orthogonal(f) ⇐⇒ 0 ≡ 0 ∧ Isometry(f))

Lemma: rv-isometry-compose
[rv:InnerProductSpace]. ∀[f,g:Point(rv) ⟶ Point(rv)].  (Isometry(f g)) supposing (Isometry(g) and Isometry(f))

Lemma: rv-orthogonal-compose
[rv:InnerProductSpace]. ∀[f,g:Point(rv) ⟶ Point(rv)].  (Orthogonal(f g)) supposing (Orthogonal(g) and Orthogonal(f))

Lemma: rv-isometry-inverse
[rv:InnerProductSpace]. ∀[f,g:Point(rv) ⟶ Point(rv)].
  (Isometry(f)) supposing (Isometry(g) and (∀x:Point(rv). (f x) ≡ x))

Lemma: rv-orthogonal-inverse
[rv:InnerProductSpace]. ∀[f,g:Point(rv) ⟶ Point(rv)].
  (Orthogonal(f)) supposing (Orthogonal(g) and (∀x:Point(rv). (f x) ≡ x))

Lemma: rv-isometry-id
[rv:InnerProductSpace]. Isometry(λx.x)

Lemma: rv-orthogonal-id
[rv:InnerProductSpace]. Orthogonal(λx.x)

Definition: rv-permutation-group
Perm(rv) ==  Perm(rv)

Lemma: rv-permutation-group_wf
[rv:InnerProductSpace]. (Perm(rv) ∈ s-Group)

Lemma: rv-perm-point
  (Point(Perm(rv)) {fg:Point(rv) ⟶ Point(rv) × (Point(rv) ⟶ Point(rv))| 
                      let f,g fg 
                      in (∀x:Point(rv). (g x) ≡ x)
                         ∧ (∀x:Point(rv). (f x) ≡ x)
                         ∧ (∀x,y:Point(rv).  (f  y))
                         ∧ (∀x,y:Point(rv).  (g  y))} )

Lemma: rv-perm-id
[rv:Top]. (1 ~ <λx.x, λx.x>)

Lemma: rv-perm-inv
[rv,x:Top].  (x^-1 let f,g in <g, f>)

Lemma: rv-perm-op
[rv,x,y:Top].  ((x y) let f,g in let f',g' in <f', g' g>)

Definition: rv-isometry-group
Isom(rv) ==  mk-s-subgroup(Perm(rv);fg.Isometry(fst(fg)))

Lemma: rv-isometry-group_wf
[rv:InnerProductSpace]. (Isom(rv) ∈ s-Group)

Lemma: subtype-rv-isometry-group
  ({fg:Point(rv) ⟶ Point(rv) × (Point(rv) ⟶ Point(rv))| let f,g fg in (∀x:Point(rv). (g x) ≡ x) ∧ Isometry(f)} 

Definition: orthogonal-group
O(rv) ==  mk-s-subgroup(Perm(rv);fg.Orthogonal(fst(fg)))

Lemma: orthogonal-group_wf
[rv:InnerProductSpace]. (O(rv) ∈ s-Group)

Lemma: subtype-orthogonal-group
  ({fg:Point(rv) ⟶ Point(rv) × (Point(rv) ⟶ Point(rv))| let f,g fg in (∀x:Point(rv). (g x) ≡ x) ∧ Orthogonal(f)} 

Definition: is-isometry
is-isometry(rv;f) ==  ∃g:Point(rv) ⟶ Point(rv). ∃t:Point(rv). (Orthogonal(g) ∧ (∀x:Point(rv). x ≡ t))

Lemma: is-isometry_wf
[rv:InnerProductSpace]. ∀[f:Point(rv) ⟶ Point(rv)].  (is-isometry(rv;f) ∈ ℙ)

Lemma: implies-isometry-lemma1
rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝr0 < r} . ∀N:{2...}.
  ((∀x,y:Point(rv).  (x ≡  x ≡ y))
   (∀x,y:Point(rv).  ((||x y|| r)  (||f y|| ≤ r)))
   (∀x,y:Point(rv).  ((||x y|| (r(N) r))  ((r(N) r) ≤ ||f y||)))
   {∀x,y:Point(rv).  (((||x y|| r) ∨ (||x y|| (r(2) r)))  (||f y|| ||x y||))})

Lemma: implies-isometry-lemma2
rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝr0 < r} .
  ((∀x,y:Point(rv).  (x ≡  x ≡ y))
   (∀x,y:Point(rv).  (((||x y|| r) ∨ (||x y|| (r(2) r)))  (||f y|| ||x y||)))
   (∀x,y:Point(rv).  ((||x y|| r)  (∀j:ℕr(j)*y x ≡ r(j)*f x))))

Comment: geometry primitives in inner product spaces
The primitives of constructive geometry are
 1) separation (of two points)
 2) betweeness (a ternary relation)
 3) congruence (a quaternary relation)
 4) triangle   (a ternary relation that says 
                triangle has strictly positive angles)

If rv is an ⌜InnerProductSpace⌝ then it is a ⌜SeparationSpace⌝ so it has
primitive ⌜y⌝ for separation.

For congrence ab=cd  we use ⌜||a b|| ||c d||⌝.

The proper triangle relation on a, b, is
  ⌜|a b ⋅ b| < (||a b|| ||c b||)⌝
it is saying that the Cauchy-Schwarz inequality is strict.
This turns out to be symmetric relation.

For the betweeness relation B(a,b,c) we say that 
Cauchy-Schwarz gives equality so that (a-b) and (c-b) are linearly dependent
and in addition the inner product is non-positive ⌜b ⋅ b ≤ r0⌝.
That puts between ⌜b⌝ and ⌜b⌝so is between and c.

We can say both parts of the B(a,b,c) relation in one equality realtion:
 ⌜((||a b|| ||c b||) b ⋅ b) r0⌝.

This makes B(a,b,c) and ab=cd stable relations  
(equivalent to their double negation), while ⌜y⌝ and triangle(a,b,c)
have constructive content and are not stable, in general.

Definition: ip-congruent
ab=cd ==  ||a b|| ||c d||

Lemma: ip-congruent_wf
[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)].  (ab=cd ∈ ℙ)

Lemma: stable__ip-congruent
[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)].  Stable{ab=cd}

Lemma: sq_stable__ip-congruent
[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)].  SqStable(ab=cd)

Lemma: ip-congruent-sym
[rv:InnerProductSpace]. ∀[a,b:Point(rv)].  ab=ba

Lemma: ip-congruent-trans
[rv:InnerProductSpace]. ∀[a,b,p,q,r,s:Point(rv)].  (pq=rs) supposing (ab=rs and ab=pq)

Lemma: ip-congruent_functionality
[rv:InnerProductSpace]. ∀[a,b,c,d,a2,b2,c2,d2:Point(rv)].
  ({ab=cd ⇐⇒ a2b2=c2d2}) supposing (d ≡ d2 and c ≡ c2 and b ≡ b2 and a ≡ a2)

Lemma: ip-congruent-same
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  (aa=bc  b ≡ c)

Lemma: ip-congruent-same2
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  (ab=cc  a ≡ b)

Lemma: ip-congruent-sep
rv:InnerProductSpace. ∀a,b,c:Point(rv). ∀d:{d:Point(rv)| ab=cd} .  (a  d)

Definition: ip-between
a_b_c ==  ((||a b|| ||c b||) b ⋅ b) r0

Lemma: ip-between_wf
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  (a_b_c ∈ ℙ)

Lemma: ip-between_functionality
[rv:InnerProductSpace]. ∀[a,b,c,a2,b2,c2:Point(rv)].  (a ≡ a2  b ≡ b2  c ≡ c2  {a_b_c ⇐⇒ a2_b2_c2})

Lemma: ip-between-iff
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a   (a_b_c ⇐⇒ ∃t:ℝ((t ∈ (r0, r1)) ∧ b ≡ t*a r1 t*c)))

Lemma: ip-between-same
[rv:InnerProductSpace]. ∀[a,b:Point(rv)].  (a_b_a  b ≡ a)

Definition: ip-triangle
Δ(a;b;c) ==  |a b ⋅ b| < (||a b|| ||c b||)

Lemma: ip-triangle_wf
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  (a;b;c) ∈ ℙ)

Lemma: sq_stable__ip-triangle
rv:InnerProductSpace. ∀a,b,c:Point(rv).  SqStable(Δ(a;b;c))

Lemma: ip-triangle_functionality
rv:InnerProductSpace. ∀a,b,c,a2,b2,c2:Point(rv).  (a ≡ a2  b ≡ b2  c ≡ c2  (a;b;c) ⇐⇒ Δ(a2;b2;c2)})

Lemma: ip-triangle-symmetry
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a;b;c)  Δ(c;b;a))

Lemma: ip-triangle-permute-lemma
rv:InnerProductSpace. ∀x,y:Point(rv).  ((|x ⋅ y| < (||x|| ||y||))  (|x ⋅ x| < (||x|| ||y x||)))

Lemma: ip-triangle-permute
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a;b;c)  Δ(c;a;b))

Lemma: ip-triangle-linearity
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a;b;c)  (∀t:ℝ((r0 < |t|)  Δ(b t*a b;b;c))))

Lemma: ip-triangle-implies-separated
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a;b;c)  c)

Lemma: ip-triangle-implies-separated2
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a;b;c)  b)

Lemma: not-ip-triangle
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a   (¬Δ(a;b;c))  (∃t:ℝ((r0 < |t|) ∧ c ≡ t*a b)))

Lemma: ip-triangle-shift
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a;b;c)  (∀z:Point(rv). (z  (¬Δ(a;b;z))  Δ(z;b;c))))

Lemma: ip-triangle-not-between
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  ¬a_b_c supposing Δ(a;b;c)

Lemma: ip-triangle-implies
rv:InnerProductSpace. ∀a,b,c:Point(rv).
  (a;b;c)  (c;b;a) ∧ Δ(c;a;b) ∧ c ∧ a_b_c) ∧ (∀z:Point(rv). (z  (¬Δ(a;b;z))  Δ(z;b;c)))))

Lemma: ip-triangle-lemma
rv:InnerProductSpace. ∀x,y:Point(rv).
  ((||x|| ||y||)  (r0 < ||x y||)  (r0 < ||r(-1)*x y||)  (|x ⋅ y| < (||x|| ||y||)))

Lemma: implies-ip-triangle
rv:InnerProductSpace. ∀a,b,c,a':Point(rv).  (a_b_a'  ab=a'b  ab=cb   a'  Δ(a;b;c))

Lemma: ip-between-symmetry
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  (a_b_c  c_b_a)

Lemma: ip-between-trivial
[rv:InnerProductSpace]. ∀[a,b:Point(rv)].  b_b_a

Lemma: ip-between-trivial2
[rv:InnerProductSpace]. ∀[a,b:Point(rv)].  a_b_b

Lemma: stable__ip-between
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  Stable{a_b_c}

Lemma: sq_stable__ip-between
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  SqStable(a_b_c)

Lemma: not-ip-triangle-implies
rv:InnerProductSpace. ∀a,b,c:Point(rv).  ((¬Δ(a;b;c))  ((¬a_b_c) ∧ b_c_a) ∧ c_a_b))))

Lemma: not-ip-triangle-iff
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (¬Δ(a;b;c) ⇐⇒ ¬((¬a_b_c) ∧ b_c_a) ∧ c_a_b)))

Lemma: ip-between-inner-trans
[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)].  (a_b_d  b_c_d  a_b_c)

Lemma: ip-dist-between-1
[rv:InnerProductSpace]. ∀[t:ℝ]. ∀[a,c:Point(rv)].  (||a t*a r1 t*c|| (|r1 t| ||a c||))

Lemma: ip-dist-between-2
[rv:InnerProductSpace]. ∀[t:ℝ]. ∀[a,c:Point(rv)].  (||t*a r1 t*c c|| (|t| ||a c||))

Lemma: ip-dist-between
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  ||a c|| (||a b|| ||b c||) supposing a_b_c

Lemma: ip-between-rleq
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  {(||a b|| ≤ ||a c||) ∧ (||b c|| ≤ ||a c||)} supposing a_b_c

Lemma: ip-between-rless
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a_b_c   (||a b|| < ||a c||))

Lemma: ip-between-sep
rv:InnerProductSpace. ∀a,c:Point(rv).  ∀[b:Point(rv)]. (a c) supposing (a and a_b_c)

Lemma: ip-between-iff2
rv:InnerProductSpace. ∀a,b,c:Point(rv).
  (a_b_c ⇐⇒ (a ≡  b ≡ c) ∧ (a  (∃t:ℝ((t ∈ [r0, r1]) ∧ b ≡ t*a r1 t*c))))

Lemma: rn-ip-between
n:{2...}. ∀a,b,c:ℝ^n.  (a_b_c ⇐⇒ rv-T(n;a;b;c))

Definition: ip-ge
cd ≥ ab ==  ¬¬(∃w:Point(rv). (c_w_d ∧ cw=ab))

Lemma: ip-ge_wf
[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)].  (cd ≥ ab ∈ ℙ)

Definition: ip-gt
cd > ab ==  ↓∃w:Point(rv). (c_w_d ∧ cw=ab ∧ d)

Lemma: ip-gt_wf
[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)].  (cd > ab ∈ ℙ)

Lemma: ip-five-segment-lemma
[rv:InnerProductSpace]. ∀[A,B,C,D:Point(rv)]. ∀[t:ℝ].
  ((t ∈ (r0, r1))
   B ≡ t*A r1 t*C
   let ||D B|| in
      let ||A D|| in
      let ||B C|| in
      let ||A B|| in
      let ||D C|| in
      let (t/t r1) in
      x^2 (c^2 a^2 (s (b^2 d^2 a^2))))

Lemma: ip-five-segment
[rv:InnerProductSpace]. ∀[a,b,c,d,A,B,C,D:Point(rv)].
  (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and b)

Definition: ip-strict-between
a-b-c ==  a_b_c ∧ b ∧ c

Lemma: ip-strict-between_wf
[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)].  (a-b-c ∈ ℙ)

Lemma: ip-strict-between-iff
rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a-b-c ⇐⇒ (∃t:ℝ((t ∈ (r0, r1)) ∧ b ≡ t*a r1 t*c)) ∧ c)

Lemma: ip-inner-Pasch1
rv:InnerProductSpace. ∀a,b,c,p,q:Point(rv).
  (a p
       ∧ b_x_p
       ∧ (a  a)
       ∧ ((a q ∧ c ∧ q)  q)
       ∧ ((b p ∧ q)  b)
       ∧ ((b p ∧ c)  p))))

Lemma: ip-inner-Pasch
rv:InnerProductSpace. ∀a,b,c:Point(rv). ∀p:{p:Point(rv)| a_p_c} . ∀q:{q:Point(rv)| b_q_c} .
  (a p
   (∃x:{x:Point(rv)| a_x_q ∧ b_x_p} 
       ((a  a)
       ∧ ((a q ∧ c ∧ q)  q)
       ∧ ((b p ∧ q)  b)
       ∧ ((b p ∧ c)  p))))

Lemma: ip-inner-Pasch'
rv:InnerProductSpace. ∀a,b:Point(rv). ∀c:{c:Point(rv)| c} . ∀p:{p:Point(rv)| a_p_c ∧ p} .
q:{q:Point(rv)| b_q_c} .
  (∃x:Point(rv) [(a_x_q
                ∧ b_x_p
                ∧ (a  a)
                ∧ ((a q ∧ c ∧ q)  q)
                ∧ ((b p ∧ q)  b)
                ∧ ((b p ∧ c)  p))])

Lemma: ip-line-circle-lemma
rv:InnerProductSpace. ∀r:ℝ. ∀p,q:Point(rv).
  (p q
   (||p|| ≤ r)
   let in
         (r0 ≤ (((r(2) p ⋅ v) r(2) p ⋅ v) r(4) ||v||^2 (||p||^2 r^2)))
         ∧ (||p quadratic1(||v||^2;r(2) p ⋅ v;||p||^2 r^2)*v|| r)
         ∧ (||p quadratic2(||v||^2;r(2) p ⋅ v;||p||^2 r^2)*v|| r))

Lemma: ip-line-circle-1
rv:InnerProductSpace. ∀a,b,p,q:Point(rv).
  (a b
   (||p a|| ≤ ||a b||)
   (||a b|| ≤ ||q a||)
   (∃u:{u:Point(rv)| ab=au ∧ q_u_p} 
       ∃v:{v:Point(rv)| ab=av ∧ q_p_v} ((||a p|| < ||a b||)  (p v ∧ ((||a b|| < ||a q||)  u)))))

Lemma: ip-circle-circle-lemma1
rv:InnerProductSpace. ∀r1,r2:{r:ℝr0 ≤ r} . ∀b:Point(rv).
  ((r0 < ||b||)
        ((b ⋅ b' r0)
         (||b'|| ||b||)
         ((r1^2 r2^2) ||b||^2^2 ≤ (r(4) ||b||^2 r1^2))
         let ((r1^2 r2^2) ||b||^2/r(2)) in
            let (||b||^2 r1^2) c^2 in
              ((x ≡ (r1/||b||^2)*c*b rsqrt(d)*b' ∨ x ≡ (r1/||b||^2)*c*b rsqrt(d)*b')
               ((||x|| r1) ∧ (||x b|| r2))))))

Lemma: ip-circle-circle-lemma2
rv:InnerProductSpace. ∀r1,r2:{r:ℝr0 ≤ r} . ∀b:Point(rv).
  ((r0 < ||b||)
   ((r1^2 r2^2) ||b||^2^2 ≤ (r(4) ||b||^2 r1^2))
       (((||u|| r1) ∧ (||u b|| r2))
       ∧ ((||v|| r1) ∧ (||v b|| r2))
       ∧ (((r1^2 r2^2) ||b||^2^2 < (r(4) ||b||^2 r1^2))  v))))

Lemma: ip-circle-circle-lemma3
rv:InnerProductSpace. ∀a,b:Point(rv). ∀c:{c:Point(rv)| c} . ∀d:Point(rv).
  ∀[p:{p:Point(rv)| ab=ap ∧ (||c p|| ≤ ||c d||)} ]. ∀[q:{q:Point(rv)| cd=cq ∧ (||a q|| ≤ ||a b||)} ].
    ∃u,v:{p:Point(rv)| ab=ap ∧ cd=cp} (((||a q|| < ||a b||) ∧ (||c p|| < ||c d||))  v)

Lemma: ip-extend-lemma
rv:InnerProductSpace. ∀a:Point(rv). ∀b:{b:Point(rv)| b} . ∀dcd:{d:ℝr0 ≤ d} .
  (∃x:Point(rv) [(a_b_x ∧ (||b x|| dcd))])

Lemma: ip-ge-dist
[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)].  ((||a b|| ≤ ||c d||)  (¬¬(∃w:Point(rv). (a_b_w ∧ cd=aw))))

Lemma: ip-gt-iff
rv:InnerProductSpace. ∀a,b,c,d:Point(rv).  uiff(cd > ab;||a b|| < ||c d||)

Lemma: ip-ge-iff
[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)].  uiff(cd ≥ ab;||a b|| ≤ ||c d||)

Lemma: ip-line-circle
rv:InnerProductSpace. ∀a:Point(rv). ∀b:{b:Point(rv)| b} . ∀p:{p:Point(rv)| ab ≥ ap} . ∀q:{q:Point(rv)| 
                                                                                             q ∧ aq ≥ ab} .
  ∃u:{u:Point(rv)| ab=au ∧ q_u_p} (∃v:Point(rv) [(ab=av ∧ q_p_v)])

Lemma: ip-ge-sep
rv:InnerProductSpace. ∀a,c:Point(rv).  ∀[b:Point(rv)]. (a c) supposing (a and ac ≥ ab)

Lemma: ip-circle-circle
rv:InnerProductSpace. ∀a,b:Point(rv). ∀c:{c:Point(rv)| c} . ∀d:Point(rv).
  ∀[p:{p:Point(rv)| ab=ap ∧ cd ≥ cp} ]. ∀[q:{q:Point(rv)| cd=cq ∧ ab ≥ aq} ].
    ∃u:{u:Point(rv)| ab=au ∧ cd=cu} (∃v:Point(rv) [((ab=av ∧ cd=cv) ∧ ((ab > aq ∧ cd > cp)  v))])

Lemma: ip-weak-triangle-inequality
rv:InnerProductSpace. ∀a,b,x,p:Point(rv).  (ax=ab  a_x_p  bp ≥ xp)

Lemma: ip-non-trivial
rv:InnerProductSpace. ∀x:{x:Point(rv)| r0 < ||x||} .  ∃a:Point(rv). (∃b:Point(rv) [a b])

Lemma: ip-extend
rv:InnerProductSpace. ∀a:Point(rv). ∀b:{b:Point(rv)| b} . ∀c,d:Point(rv).  (∃x:Point(rv) [(a_b_x ∧ bx=cd)])

Definition: mkr2
mkr2(a;b) ==  λi.[a; b][i]

Lemma: mkr2_wf
[a,b:ℝ].  (mkr2(a;b) ∈ ℝ^2)

Lemma: implies-isometry-lemma3
rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝr0 < r} .
  ((∀x,y:Point(rv).  (x ≡  x ≡ y))
   (∀x,y:Point(rv).  (((||x y|| r) ∨ (||x y|| (r(2) r)))  (||f y|| ||x y||)))
   (∀n,m:ℕ+. ∀x,y:Point(rv).  ((||x y|| (r(n) r/r(m)))  (||f y|| ||x y||))))

Lemma: implies-isometry-lemma4
rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝr0 < r} .
  ((∀x,y:Point(rv).  (x ≡  x ≡ y))
   (∀x,y:Point(rv).  (((||x y|| r) ∨ (||x y|| (r(2) r)))  (||f y|| ||x y||)))
   (∀n,m:ℕ+. ∀x,y:Point(rv).  ((||x y|| < (r(n) r/r(m)))  (||f y|| ≤ (r(n) r/r(m))))))

Lemma: implies-isometry-lemma5
rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀d:{r:ℝr0 < r} .
  ((∀x,y:Point(rv).  (x ≡  x ≡ y))
   (∀x,y:Point(rv).  (((||x y|| d) ∨ (||x y|| (r(2) d)))  (||f y|| ||x y||)))
        ((∃n,m:ℕ+(s (r(n)/r(m))))
         (∃n,m:ℕ+(r (r(n)/r(m))))
         (∀x,y:Point(rv).  ((||x y|| ∈ (r d, d))  (||f y|| ∈ [r d, d]))))))

Lemma: implies-isometry
rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝr0 < r} . ∀N:{2...}.
  ((∀x,y:Point(rv).  (x ≡  x ≡ y))
   (∀x,y:Point(rv).  ((||x y|| r)  (||f y|| ≤ r)))
   (∀x,y:Point(rv).  ((||x y|| (r(N) r))  ((r(N) r) ≤ ||f y||)))

Lemma: uhg-identity1
  ((((((r1 (t1 t2)) (t3 t4)) (r1 (t3 t4)) (t1 t2))
  (((r1 (t1 t3)) (t2 t4)) (r1 (t2 t4)) (t1 t3)))
  ((r(2) ((t3 t4) t1 t2)) r(2) ((t2 t4) t1 t3)))
  ((((r1 t1 t2) (t3 t4)) (r1 t3 t4) (t1 t2))
    (((r1 t1 t3) (t2 t4)) (r1 t2 t4) (t1 t3))))

Definition: real-proj
^n ==  {b:ℝ^n 1| ∃k:ℕ1. k ≠ r0} 

Lemma: real-proj_wf
[n:ℕ]. (ℙ^n ∈ Type)

Lemma: proj-norm-positive
n:ℕ. ∀a:ℙ^n.  (r0 < ||a||)

Definition: punit
u(a) ==  (r1/||a||)*a

Lemma: punit_wf
[n:ℕ]. ∀[a:ℙ^n].  (u(a) ∈ ℝ^n 1)

Lemma: punit-norm1
[n:ℕ]. ∀[a:ℙ^n].  (||u(a)|| r1)

Definition: proj-sep
a ≠ ==  u(a) ≠ u(b) ∧ u(a) ≠ r(-1)*u(b)

Lemma: proj-sep_wf
[n:ℕ]. ∀[a,b:ℙ^n].  (a ≠ b ∈ ℙ)

Lemma: proj-sep_symmetry
n:ℕ. ∀a,b:ℙ^n.  (a ≠  b ≠ a)

Lemma: proj-sep_antireflexive
[n:ℕ]. ∀[a:ℙ^n].  a ≠ a)

Lemma: sq_stable__proj-sep
n:ℕ. ∀a,b:ℙ^n.  SqStable(a ≠ b)

Lemma: not-proj-sep
n:ℕ. ∀a,b:ℙ^n.  a ≠ ⇐⇒ req-vec(n 1;u(a);u(b)) ∨ req-vec(n 1;u(a);r(-1)*u(b)))

Lemma: proj-sep-or
n:ℕ. ∀a,b,c:ℙ^n.  (a ≠  (a ≠ c ∨ b ≠ c))

Definition: proj-eq
==  ∀i,j:ℕ1.  (((a i) (b j)) ((b i) (a j)))

Lemma: proj-eq_wf
[n:ℕ]. ∀[a,b:ℙ^n].  (a b ∈ ℙ)

Lemma: sq_stable__proj-eq
[n:ℕ]. ∀[a,b:ℙ^n].  SqStable(a b)

Lemma: stable__proj-eq
[n:ℕ]. ∀[a,b:ℙ^n].  Stable{a b}

Lemma: proj-eq-iff
n:ℕ. ∀a,b:ℙ^n.  (a ⇐⇒ ↓∃m:{m:ℝm ≠ r0} req-vec(n 1;a;m*b))

Lemma: proj-eq-equiv
[n:ℕ]. EquivRel(ℙ^n;a,b.a b)

Lemma: proj-eq_inversion
[n:ℕ]. ∀[a,b:ℙ^n].  supposing b

Lemma: proj-eq_transitivity
[n:ℕ]. ∀[a,b,c:ℙ^n].  (a c) supposing (b and b)

Lemma: proj-eq_weakening
[n:ℕ]. ∀[a,b:ℙ^n].  supposing b ∈ ℙ^n

Lemma: proj-eq_functionality
[n:ℕ]. ∀[x1,x2,y1,y2:ℙ^n].  (uiff(x1 y1;x2 y2)) supposing (y1 y2 and x1 x2)

Lemma: not-proj-sep-iff-proj-eq
n:ℕ. ∀a,b:ℙ^n.  a ≠ ⇐⇒ b)

Lemma: proj-sep_functionality
n:ℕ. ∀a1,b1,a2,b2:ℙ^n.  (a1 a2  b1 b2  {a1 ≠ b1 ⇐⇒ a2 ≠ b2})

Lemma: proj-sep-implies
n:ℕ. ∀a,b:ℙ^n.  (a ≠  (∃i,j:ℕ1. (a i) (b j) ≠ (a j) (b i)))

Definition: proj-rev
proj-rev(n;p) ==  λi.if i <then else -(p i) fi 

Lemma: proj-rev_wf
[n:ℕ]. ∀[p:ℙ^n].  (proj-rev(n;p) ∈ ℙ^n)

Lemma: proj-rev_functionality
[n:ℕ]. ∀[p1,p2:ℙ^n].  proj-rev(n;p1) proj-rev(n;p2) supposing p1 p2

Definition: proj-incidence
on ==  v⋅proj-rev(n;p) r0

Lemma: proj-incidence_wf
[n:ℕ]. ∀[p,v:ℙ^n].  (v on p ∈ ℙ)

Lemma: proj-incidence_symmetry
[n:ℕ]. ∀[p,v:ℙ^n].  uiff(v on p;p on v)

Lemma: proj-incidence_functionality
[n:ℕ]. ∀[p1,p2,v1,v2:ℙ^n].  (uiff(v1 on p1;v2 on p2)) supposing (p1 p2 and v1 v2)

Lemma: p2-incidence
[p,v:ℙ^2].  uiff(v on p;((((v 0) (p 0)) ((v 1) (p 1))) (v 2) (p 2)) r0)

Definition: p2J
p2J(a;b) ==
  λi.if (i =z 0) then ((a 1) (b 2)) (b 1) (a 2)
     if (i =z 1) then ((a 2) (b 0)) (b 2) (a 0)
     else ((a 1) (b 0)) (b 1) (a 0)

Lemma: p2J_wf
[a,b:ℙ^2].  p2J(a;b) ∈ ℙ^2 supposing a ≠ b

Lemma: p2J_functionality
[a1,b1,a2,b2:ℙ^2].  (p2J(a1;b1) p2J(a2;b2)) supposing (b1 b2 and a1 a2 and a1 ≠ b1)

Lemma: p2J_on
[a,b:ℙ^2].  p2J(a;b) on supposing a ≠ b

Lemma: p2J_symmetry
[a,b:ℙ^2].  p2J(a;b) p2J(b;a) supposing a ≠ b

Lemma: p2J_on_symm
[a,b:ℙ^2].  p2J(a;b) on supposing a ≠ b

Definition: proj-permute
proj-permute(p;f) ==  f

Lemma: proj-permute_wf
[n:ℕ]. ∀[p:ℙ^n]. ∀[f:ℕ1 ⟶ ℕ1].  proj-permute(p;f) ∈ ℙ^n supposing Surj(ℕ1;ℕ1;f)

Definition: rv-decomp
rv-decomp(rv;x;e) ==  <x ⋅ e*e, x ⋅ e>

Lemma: rv-decomp_wf
[rv:InnerProductSpace]. ∀[e,x:Point(rv)].
  rv-decomp(rv;x;e) ∈ {p:Point(rv) × ℝx ≡ fst(p) snd(p)*e ∧ (fst(p) ⋅ r0)}  supposing e^2 r1

Definition: translation-group-fun
translation-group-fun(rv;e;T) ==
  (∀s,t:ℝ. ∀x,y:Point(rv).  (T  (x y ∨ s ≠ t)))
  ∧ (∀t,s:ℝ. ∀x:Point(rv).  (t s) x ≡ (T x))
  ∧ (∀x:Point(rv). ∀r:ℝ.  ∃t:ℝ(T x ≡ r*e ∧ (∀y:ℝ(y ≠  r*e))))
  ∧ (∀x:Point(rv). ∀t:{t:ℝr0 ≤ t} .  ∃r:{t:ℝr0 ≤ t} x ≡ r*e)

Lemma: translation-group-fun_wf
rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).  (translation-group-fun(rv;e;T) ∈ ℙ)

Definition: trans-apply
T_t(x) ==  x

Lemma: trans-apply_wf
rv:InnerProductSpace. ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv). ∀x:Point(rv).  ∀[t:ℝ]. (T_t(x) ∈ Point(rv))

Lemma: trans-apply_functionality
[rv:InnerProductSpace]. ∀[T:ℝ ⟶ Point(rv) ⟶ Point(rv)].
  ∀[x1,x2:Point(rv)]. ∀[t1,t2:ℝ].  (T_t1(x1) ≡ T_t2(x2)) supposing ((t1 t2) and x1 ≡ x2) 
  supposing ∃e:Point(rv). translation-group-fun(rv;e;T)

Lemma: trans-apply-0
rv:InnerProductSpace. ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
  ∀x:Point(rv). T_r0(x) ≡ supposing ∃e:Point(rv). translation-group-fun(rv;e;T)

Lemma: trans-apply-add
rv:InnerProductSpace. ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv). ∀t,s:ℝ.
  ∀x:Point(rv). T_t s(x) ≡ T_t(T_s(x)) supposing ∃e:Point(rv). translation-group-fun(rv;e;T)

Lemma: trans-apply-sep
rv:InnerProductSpace. ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
  ((∃e:Point(rv). translation-group-fun(rv;e;T))  (∀x:Point(rv). ∀t1,t2:ℝ.  (t1 ≠ t2  T_t2(x) T_t1(x))))

Definition: translation-group
translation-group(rv;e;T) ==  mk-s-subgroup(Perm(rv);fg.∃t:ℝ. ∀x:Point(rv). (fst(fg)) x ≡ x)

Lemma: translation-group_wf
rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
  translation-group(rv;e;T) ∈ s-Group supposing translation-group-fun(rv;e;T)

Lemma: translation-group-point
rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
   Point(translation-group(rv;e;T)) ≡ {fg:Point(rv) ⟶ Point(rv) × (Point(rv) ⟶ Point(rv))| 
                                          ((∀x:Point(rv). (fst(fg)) x ≡ x)
                                          ∧ (∀x:Point(rv). (snd(fg)) x ≡ -(t) x))} )

Definition: trans-kernel
ρ(h;t) ==  T_t(h) ⋅ e

Lemma: trans-kernel_wf
[rv:InnerProductSpace]. ∀[e:Point(rv)]. ∀[T:ℝ ⟶ Point(rv) ⟶ Point(rv)]. ∀[t:ℝ]. ∀[h:{h:Point(rv)| h ⋅ r0} ].
  (h;t) ∈ ℝ)

Lemma: trans-kernel-equation
[rv:InnerProductSpace]. ∀[e:{e:Point(rv)| e^2 r1} ]. ∀[T:ℝ ⟶ Point(rv) ⟶ Point(rv)].
  ∀[t:ℝ]. ∀[h:{h:Point(rv)| h ⋅ r0} ].  T_t(h) ≡ + ρ(h;t)*e supposing translation-group-fun(rv;e;T)

Definition: trans-kernel-fun
trans-kernel-fun(rv;e;f) ==
  (∀h1,h2:{h:Point(rv)| h ⋅ r0} . ∀t1,t2:ℝ.  (f h1 t1 ≠ h2 t2  (h1 h2 ∨ t1 ≠ t2)))
  ∧ (∀h:{h:Point(rv)| h ⋅ r0} ((f r0) r0))
  ∧ (∀h:{h:Point(rv)| h ⋅ r0} . ∀t1,t2:ℝ.  ((t1 < t2)  ((f t1) < (f t2))))
  ∧ (∀h:{h:Point(rv)| h ⋅ r0} . ∀r:ℝ.  ∃t:ℝ((f t) r))

Lemma: trans-kernel-fun_wf
[rv:InnerProductSpace]. ∀[e:Point(rv)]. ∀[f:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ].  (trans-kernel-fun(rv;e;f) ∈ ℙ)

Lemma: trans-kernel-is-kernel-fun
rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
  ((e^2 r1)  translation-group-fun(rv;e;T)  trans-kernel-fun(rv;e;λh,t. ρ(h;t)))

Lemma: trans-kernel_functionality
rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
  ((e^2 r1)
   (∀h1,h2:{h:Point(rv)| h ⋅ r0} . ∀t,s:ℝ.  (h1;t) = ρ(h2;s)) supposing ((t s) and h1 ≡ h2)))

Lemma: trans-kernel-increasing
rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
  ((e^2 r1)
   (∀h:{h:Point(rv)| h ⋅ r0} . ∀t,s:ℝ.  ((t < s)  (h;t) < ρ(h;s)))))

Lemma: trans-kernel-0
rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
  ((e^2 r1)  translation-group-fun(rv;e;T)  (∀h:{h:Point(rv)| h ⋅ r0} (h;r0) r0)))

Lemma: kernel-fun-properties
rv:InnerProductSpace. ∀e:Point(rv). ∀f:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ.
  ((e^2 r1)
   ((∀h1,h2:{h:Point(rv)| h ⋅ r0} . ∀t1,t2:ℝ.  (h1 ≡ h2  (t1 t2)  ((f h1 t1) (f h2 t2))))
     ∧ (∀g:h:{h:Point(rv)| h ⋅ r0}  ⟶ r:ℝ ⟶ ℝ
          ((∀h:{h:Point(rv)| h ⋅ r0} . ∀r:ℝ.  ((f (g r)) r))
           ((∀h1,h2:{h:Point(rv)| h ⋅ r0} . ∀t1,t2:ℝ.  (g h1 t1 ≠ h2 t2  (h1 h2 ∨ t1 ≠ t2)))
             ∧ (∀h1,h2:{h:Point(rv)| h ⋅ r0} . ∀t1,t2:ℝ.  (h1 ≡ h2  (t1 t2)  ((g h1 t1) (g h2 t2)))))))
     ∧ (∃g:h:{h:Point(rv)| h ⋅ r0}  ⟶ r:ℝ ⟶ ℝ. ∀h:{h:Point(rv)| h ⋅ r0} . ∀r:ℝ.  ((f (g r)) r))))

Definition: separable-kernel
separable-kernel(rv;e;f) ==
  ∃phi:ℝ ⟶ ℝ. ∃psi:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ. ∀h:{h:Point(rv)| h ⋅ r0} . ∀t:ℝ.  ((f t) ((phi t) (psi h)\000C))

Lemma: separable-kernel_wf
[rv:InnerProductSpace]. ∀[e:Point(rv)]. ∀[f:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ].  (separable-kernel(rv;e;f) ∈ ℙ)

Lemma: separable-kernel-properties
rv:InnerProductSpace. ∀e:Point(rv). ∀f:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ.
   (∀g:ℝ ⟶ ℝ. ∀k:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ.
        ((∀h:{h:Point(rv)| h ⋅ r0} . ∀t:ℝ.  ((f t) ((g t) (k h))))
         (∃phi:ℝ ⟶ ℝ
             ∃psi:{h:Point(rv)| h ⋅ r0}  ⟶ {r:ℝr0 < r} 
              ((∀h:{h:Point(rv)| h ⋅ r0} . ∀t:ℝ.  ((f t) ((phi t) (psi h))))
              ∧ ((phi r0) r0)
              ∧ ((psi 0) r1)
              ∧ (∀t,s:ℝ.  ((t < s)  ((phi t) < (phi s))))
              ∧ (∀t:ℝ. ∃s:ℝ((phi s) t))
              ∧ (∀h1,h2:{h:Point(rv)| h ⋅ r0} .  (psi h1 ≠ psi h2  h1 h2))
              ∧ (∀t,s:ℝ.  (phi t ≠ phi  t ≠ s)))))))

Lemma: separable-kernel-iff
rv:InnerProductSpace. ∀e:Point(rv). ∀f:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ.
     ⇐⇒ ∃phi:ℝ ⟶ ℝ
          ∃psi:{h:Point(rv)| h ⋅ r0}  ⟶ {r:ℝr0 < r} 
           ((∀h:{h:Point(rv)| h ⋅ r0} . ∀t:ℝ.  ((f t) ((phi t) (psi h))))
           ∧ ((phi r0) r0)
           ∧ ((psi 0) r1)
           ∧ (∀t,s:ℝ.  ((t < s)  ((phi t) < (phi s))))
           ∧ (∀t:ℝ. ∃s:ℝ((phi s) t))
           ∧ (∀h1,h2:{h:Point(rv)| h ⋅ r0} .  (psi h1 ≠ psi h2  h1 h2))
           ∧ (∀t,s:ℝ.  (phi t ≠ phi  t ≠ s)))))

Definition: trans-from-kernel
trans-from-kernel(rv;e;f;g;t;x) ==  let h,z rv-decomp(rv;x;e) in ((g z) t)*e

Lemma: trans-from-kernel_wf
[rv:InnerProductSpace]. ∀[e:{e:Point(rv)| e^2 r1} ]. ∀[f,g:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ]. ∀[t:ℝ].
  (trans-from-kernel(rv;e;f;g;t;x) ∈ Point(rv))

Lemma: trans-from-kernel-sep
rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 r1} . ∀f,g:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ.
   (∀h:{h:Point(rv)| h ⋅ r0} . ∀r:ℝ.  ((f (g r)) r))
   (∀s,t:ℝ. ∀x,y:Point(rv).  (trans-from-kernel(rv;e;f;g;s;x) trans-from-kernel(rv;e;f;g;t;y)  (x y ∨ s ≠ t))))

Lemma: trans-from-kernel_functionality
rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 r1} . ∀f,g:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ.
   (∀h:{h:Point(rv)| h ⋅ r0} . ∀r:ℝ.  ((f (g r)) r))
   (∀s,t:ℝ. ∀x,y:Point(rv).  ((s t)  x ≡  trans-from-kernel(rv;e;f;g;s;x) ≡ trans-from-kernel(rv;e;f;g;t;y))))

Lemma: trans-from-kernel-is-trans
rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 r1} . ∀f,g:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ.
   (∀h:{h:Point(rv)| h ⋅ r0} . ∀r:ℝ.  ((f (g r)) r))
   translation-group-fun(rv;e;λt,x. trans-from-kernel(rv;e;f;g;t;x)))

Lemma: kernel-trans-from-kernel
rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 r1} . ∀f,g:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ.
   (∀h:{h:Point(rv)| h ⋅ r0} . ∀r:ℝ.  ((f (g r)) r))
   (∀h:{h:Point(rv)| h ⋅ r0} . ∀t:ℝ.  (h;t) (f t))))

Lemma: kernel-fun-is-trans-kernel
rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 r1} . ∀f:{h:Point(rv)| h ⋅ r0}  ⟶ ℝ ⟶ ℝ.
   (∃T:ℝ ⟶ Point(rv) ⟶ Point(rv)
       (translation-group-fun(rv;e;T) ∧ (∀h:{h:Point(rv)| h ⋅ r0} . ∀t:ℝ.  (h;t) (f t))))))

Definition: separable-translation-group
separable-translation-group(rv;e;T) ==  translation-group-fun(rv;e;T) ∧ separable-kernel(rv;e;λh,t. ρ(h;t))

Lemma: separable-translation-group_wf
[rv:InnerProductSpace]. ∀[e:Point(rv)]. ∀[T:ℝ ⟶ Point(rv) ⟶ Point(rv)].  (separable-translation-group(rv;e;T) ∈ ℙ)

Lemma: separable-translation-group_iff
rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 r1} . ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
     ⇐⇒ (∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ r0} .  (a ≠ r0  (r0 < ||T_a(h) h||)))
         ∧ (∀a,b:ℝ. ∀h:{h:Point(rv)| h ⋅ r0} .
              (a ≠ r0  b ≠ r0  ((||T_a(h) h||/||T_b(h) h||) (||T_a(0)||/||T_b(0)||))))))

Definition: hyptrans
hyptrans(rv;e;t;x) ==  (x ⋅ (cosh(t) r1)) (rsqrt(r1 x^2) sinh(t))*e

Lemma: hyptrans_wf
[rv:InnerProductSpace]. ∀[e,x:Point(rv)]. ∀[t:ℝ].  (hyptrans(rv;e;t;x) ∈ Point(rv))

Lemma: hyptrans_functionality
[rv:InnerProductSpace]. ∀[e1,x1:Point(rv)]. ∀[t1:ℝ]. ∀[e2,x2:Point(rv)]. ∀[t2:ℝ].
  (hyptrans(rv;e1;t1;x1) ≡ hyptrans(rv;e2;t2;x2)) supposing (x1 ≡ x2 and e1 ≡ e2 and (t1 t2))

Lemma: hyptrans_lemma
[rv:InnerProductSpace]. ∀[e,h:Point(rv)].
  ∀tau,t:ℝ.  hyptrans(rv;e;t;h sinh(tau) rsqrt(r1 h^2)*e) ≡ sinh(tau t) rsqrt(r1 h^2)*e 
  supposing (e^2 r1) ∧ (h ⋅ r0)

Lemma: hyptrans_decomp
rv:InnerProductSpace. ∀e,x:Point(rv).
  ∃h:Point(rv). ∃tau:ℝ((h ⋅ r0) ∧ x ≡ sinh(tau) rsqrt(r1 h^2)*e) supposing e^2 r1

Lemma: hyptrans_add
[rv:InnerProductSpace]. ∀[e,x:Point(rv)]. ∀[t,s:ℝ].
  hyptrans(rv;e;t s;x) ≡ hyptrans(rv;e;t;hyptrans(rv;e;s;x)) supposing e^2 r1

Lemma: hyptrans_ext
rv:InnerProductSpace. ∀e:Point(rv). ∀s,t:ℝ. ∀x,y:Point(rv).
  (hyptrans(rv;e;s;x) hyptrans(rv;e;t;y)  (x y ∨ s ≠ t))

Lemma: hyptrans_0
[rv:InnerProductSpace]. ∀[e,x:Point(rv)].  hyptrans(rv;e;r0;x) ≡ x

Lemma: hyptrans-is-translation-group-fun
rv:InnerProductSpace. ∀e:Point(rv).  ((e^2 r1)  translation-group-fun(rv;e;λt,x. hyptrans(rv;e;t;x)))

Definition: hyptrans-perm
hyptrans-perm(rv;e;t) ==  <λx.hyptrans(rv;e;t;x), λx.hyptrans(rv;e;-(t);x)>

Lemma: hyptrans-perm_wf
[rv:InnerProductSpace]. ∀[e:Point(rv)]. ∀[t:ℝ].
  hyptrans-perm(rv;e;t) ∈ Point(translation-group(rv;e;λt,x. hyptrans(rv;e;t;x))) supposing e^2 r1

Lemma: hyp-distance-lemma1
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (r1 ≤ ((rsqrt(r1 x^2) rsqrt(r1 y^2)) x ⋅ y))

Definition: hyp-dist
hyp (x,y) ==  inv-cosh((rsqrt(r1 x^2) rsqrt(r1 y^2)) x ⋅ y)

Lemma: hyp-dist_wf
[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (hyp (x,y) ∈ ℝ)

Definition: topspace
Space ==  X:Type × E:X ⟶ X ⟶ ℙ × EquivRel(X;x,y.E y)

Lemma: topspace_wf
Space ∈ 𝕌'

Definition: toptype
|X| ==  fst(X)

Lemma: toptype_wf
[X:Space]. (|X| ∈ Type)

Definition: topeq
topeq(X;a;b) ==  (fst(snd(X))) b

Lemma: topeq_wf
[X:Space]. ∀[a,b:|X|].  (topeq(X;a;b) ∈ ℙ)

Lemma: topeq-equiv
X:Space. EquivRel(|X|;a,b.topeq(X;a;b))

Lemma: topeq_weakening
X:Space. ∀a,b:|X|.  ((a b ∈ |X|)  topeq(X;a;b))

Lemma: topeq_inversion
X:Space. ∀a,b:|X|.  (topeq(X;a;b)  topeq(X;b;a))

Lemma: topeq_transitivity
X:Space. ∀a,b,c:|X|.  (topeq(X;a;b)  topeq(X;b;c)  topeq(X;a;c))

Definition: topfun
topfun(X;Y) ==  {f:|X| ⟶ |Y|| ∀a,b:|X|.  (topeq(X;a;b)  topeq(Y;f a;f b))} 

Lemma: topfun_wf
[X,Y:Space].  (topfun(X;Y) ∈ Type)

Definition: topfuneq
topfuneq(X;Y;f;g) ==  ∀x:|X|. topeq(Y;f x;g x)

Lemma: topfuneq_wf
[X,Y:Space]. ∀[f,g:topfun(X;Y)].  (topfuneq(X;Y;f;g) ∈ ℙ)

Lemma: topfuneq-equiv
X,Y:Space.  EquivRel(topfun(X;Y);f,g.topfuneq(X;Y;f;g))

Definition: tfunequiv
tfunequiv(X;Y) ==
  <λa,x. let _,_,refl,_,_ in refl (a x)
  , λa,b,%,x. let _,_,_,sym,_ in sym (a x) (b x) (% x)
  , λa,b,c,%,%2,x. let _,_,_,_,trans in trans (a x) (b x) (c x) (% x) (%2 x)>

Lemma: topfuneq-equiv-ext
X,Y:Space.  EquivRel(topfun(X;Y);f,g.topfuneq(X;Y;f;g))

Lemma: tfunequiv_wf
X,Y:Space.  (tfunequiv(X;Y) ∈ EquivRel(topfun(X;Y);f,g.topfuneq(X;Y;f;g)))

Definition: funspace
funspace(X;Y) ==  <topfun(X;Y), λf,g. topfuneq(X;Y;f;g), tfunequiv(X;Y)>

Lemma: funspace_wf
[X,Y:Space].  (funspace(X;Y) ∈ Space)

Definition: mktopspace
mktopspace(T;E;equiv) ==  <T, E, equiv>

Lemma: mktopspace_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ]. ∀[equiv:EquivRel(T;x,y.E y)].  (mktopspace(T;E;equiv) ∈ Space)

Definition: realspace
realspace() ==  mktopspace(ℝx,y. (x y);TERMOF{req-equiv:o, 1:l})

Lemma: realspace_wf
realspace() ∈ Space

Home Index