---

Step * of Lemma mk-inner-product-space_wf

No Annotations
∀[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 x y) = (ip y x)))
                               ∧ (∀x,y,z:Point(self).  ((ip x + y z) = ((ip x z) + (ip y z))))
                               ∧ (∀a:ℝ. ∀x,y:Point(self).  ((ip a*x y) = (a * (ip x y))))} ]. ∀[pos:∀x:Point(self)
                                                                                                     (x # 0
                                                                                                     ⇐⇒ r0 < (ip x 
                                                                                                               x))].
∀[perp:∀x:Point(self). (x # 0 ⇒ (∃y:Point(self). (y # 0 ∧ ((ip x y) = r0))))].
  (vs=self;
   ip=ip;
   positive=pos;
   perp=perp ∈ InnerProductSpace)
BY
{ (Auto
   THEN (Assert self ∈ RealVectorSpace BY
               Auto)
   THEN Unfolds ``mk-inner-product-space inner-product-space`` 0
   THEN RepeatFor 3 ((RecordPlusTypeCD
                      THENL [ Id; (All (RepUR ``ss-point ss-sep ss-eq rv-0 rv-add rv-mul``) THEN Declaration)]
                     ))
   THEN (D 1 THENA Auto)
   THEN RepUR ``real-vector-space`` 0
   THEN RepeatFor 5 ((RecordPlusTypeCD
                      THENL [ Id; (Reduce 0 THEN All (RepUR ``ss-point ss-sep ss-eq rv-0 rv-add rv-mul``) THEN Trivial)]
                     ))) }

1
1. self : self:SeparationSpace
          "0":Point(self)
          "+":{f:Point(self) ⟶ Point(self) ⟶ Point(self)| 
               (∀x,y,z:Point(self).  f x (f y z) ≡ f (f x y) z) ∧ (∀x,y:Point(self).  f x y ≡ f y x)} 
          "+sep":∀x,x',y,y':Point(self).  (self."+" x y # self."+" x' y' ⇒ (x # x' ∨ y # y'))
          "*":{m:ℝ ⟶ Point(self) ⟶ Point(self)| 
               (∀a:ℝ. ∀x,y:Point(self).  m a (self."+" x y) ≡ self."+" (m a x) (m a y))
               ∧ (∀x:Point(self)
                    (m r1 x ≡ x
                    ∧ m r0 x ≡ self."0"
                    ∧ (∀a,b:ℝ.  m a (m b x) ≡ m (a * b) x)
                    ∧ (∀a,b:ℝ.  m (a + b) x ≡ self."+" (m a x) (m b x))))}  ⋂ x:Atom ⟶ if x =a "*sep"
                                                                                   then ∀a,b:ℝ. ∀x,y:Point(self).
                                                                                          (self."*" a x # self."*" b y
                                                                                          ⇒ (a ≠ b ∨ x # y))
                                                                                   else Top
                                                                                   fi 
2. self ∈ SeparationSpace
3. 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 x y) = (ip y x)))
         ∧ (∀x,y,z:Point(self).  ((ip x + y z) = ((ip x z) + (ip y z))))
         ∧ (∀a:ℝ. ∀x,y:Point(self).  ((ip a*x y) = (a * (ip x y))))} 
4. pos : ∀x:Point(self). (x # 0 ⇐⇒ r0 < (ip x x))
5. perp : ∀x:Point(self). (x # 0 ⇒ (∃y:Point(self). (y # 0 ∧ ((ip x y) = r0))))
6. self ∈ RealVectorSpace
7. self."0" ∈ Point(self)
8. self."+" ∈ {f:Point(self) ⟶ Point(self) ⟶ Point(self)| 
               (∀x,y,z:Point(self).  f x (f y z) ≡ f (f x y) z) ∧ (∀x,y:Point(self).  f x y ≡ f y x)} 
9. self."+sep" ∈ ∀x,x',y,y':Point(self).  (self."+" x y # self."+" x' y' ⇒ (x # x' ∨ y # y'))
10. self."*" ∈ {m:ℝ ⟶ Point(self) ⟶ Point(self)| 
                (∀a:ℝ. ∀x,y:Point(self).  m a (self."+" x y) ≡ self."+" (m a x) (m a y))
                ∧ (∀x:Point(self)
                     (m r1 x ≡ x
                     ∧ m r0 x ≡ self."0"
                     ∧ (∀a,b:ℝ.  m a (m b x) ≡ m (a * b) x)
                     ∧ (∀a,b:ℝ.  m (a + b) x ≡ self."+" (m a x) (m b x))))} 
11. self."*sep" ∈ ∀a,b:ℝ. ∀x,y:Point(self).  (self."*" a x # self."*" b y ⇒ (a ≠ b ∨ x # y))
⊢ self["ip" := ip]["positive" := pos]["perp" := perp] ∈ SeparationSpace

---

Latex:

---

Latex:
No  Annotations
\mforall{}[self:RealVectorSpace].  \mforall{}[ip:\{ip:Point(self)  {}\mrightarrow{}  Point(self)  {}\mrightarrow{}  \mBbbR{}| 
                                                              (\mforall{}x1,x2,y1,y2:Point(self).
                                                                    (x1  \mequiv{}  x2  {}\mRightarrow{}  y1  \mequiv{}  y2  {}\mRightarrow{}  ((ip  x1  y1)  =  (ip  x2  y2))))
                                                              \mwedge{}  (\mforall{}x,y:Point(self).    ((ip  x  y)  =  (ip  y  x)))
                                                              \mwedge{}  (\mforall{}x,y,z:Point(self).    ((ip  x  +  y  z)  =  ((ip  x  z)  +  (ip  y  z))))
                                                              \mwedge{}  (\mforall{}a:\mBbbR{}.  \mforall{}x,y:Point(self).    ((ip  a*x  y)  =  (a  *  (ip  x  y))))\}  ].
\mforall{}[pos:\mforall{}x:Point(self).  (x  \#  0  \mLeftarrow{}{}\mRightarrow{}  r0  <  (ip  x  x))].  \mforall{}[perp:\mforall{}x:Point(self)
                                                                                                                      (x  \#  0
                                                                                                                      {}\mRightarrow{}  (\mexists{}y:Point(self)
                                                                                                                                (y  \#  0  \mwedge{}  ((ip  x  y)  =  r0))))].
    (vs=self;
      ip=ip;
      positive=pos;
      perp=perp  \mmember{}  InnerProductSpace)


By

---

Latex:
(Auto
  THEN  (Assert  self  \mmember{}  RealVectorSpace  BY
                          Auto)
  THEN  Unfolds  ``mk-inner-product-space  inner-product-space``  0
  THEN  RepeatFor  3  ((RecordPlusTypeCD
                                        THENL  [  Id
                                                    ;  (All  (RepUR  ``ss-point  ss-sep  ss-eq  rv-0  rv-add  rv-mul``)
                                                          THEN  Declaration
                                                          )]
                                      ))
  THEN  (D  1  THENA  Auto)
  THEN  RepUR  ``real-vector-space``  0
  THEN  RepeatFor  5  ((RecordPlusTypeCD
                                        THENL  [  Id
                                                    ;  (Reduce  0
                                                          THEN  All  (RepUR  ``ss-point  ss-sep  ss-eq  rv-0  rv-add  rv-mul``)
                                                          THEN  Trivial)]
                                      )))

---

Home Index