---

Step * of Lemma mk-real-vector-space_wf

No Annotations
∀[self:SeparationSpace]. ∀[z:Point(self)]. ∀[p:{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)} ].
∀[m:{m:ℝ ⟶ Point(self) ⟶ Point(self)| 
     (∀a:ℝ. ∀x,y:Point(self).  m a (p x y) ≡ p (m a x) (m a y))
     ∧ (∀x:Point(self)
          (m r1 x ≡ x
          ∧ m r0 x ≡ z
          ∧ (∀a,b:ℝ.  m a (m b x) ≡ m (a * b) x)
          ∧ (∀a,b:ℝ.  m (a + b) x ≡ p (m a x) (m b x))))} ]. ∀[psep:∀x,x',y,y':Point(self).
                                                                     (p x y # p x' y' ⇒ (x # x' ∨ y # y'))].
∀[msep:∀a,b:ℝ. ∀x,y:Point(self).  (m a x # m b y ⇒ (a ≠ b ∨ x # y))].
  (ss=self;
   0=z;
   +=p;
   *=m;
   +sep=psep;
   *sep=msep ∈ RealVectorSpace)
BY
{ (Auto
   THEN (Assert self ∈ SeparationSpace BY
               Auto)
   THEN (D 1 THENA Auto)
   THEN Unfolds ``mk-real-vector-space real-vector-space`` 0
   THEN RepUR ``ss-point ss-sep`` 0
   THEN RepeatFor 5 ((RecordPlusTypeCD
                      THENL [ Id
                            ; (Reduce 0
                               THEN Try ((RepUR ``ss-eq ss-sep`` 0
                                          THEN Folds ``ss-point ss-sep`` 0
                                          THEN Try (Fold `ss-eq` 0)
                                          THEN Trivial))
                               )]
                     ))
   THEN RepUR ``separation-space`` 0
   THEN RepeatFor 3 ((RecordPlusTypeCD THENL [ Id; (Reduce 0 THEN Trivial)]))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[self:SeparationSpace].  \mforall{}[z:Point(self)].  \mforall{}[p:\{f:Point(self)  {}\mrightarrow{}  Point(self)  {}\mrightarrow{}  Point(self)| 
                                                                                                (\mforall{}x,y,z:Point(self).    f  x  (f  y  z)  \mequiv{}  f  (f  x  y)  z)
                                                                                                \mwedge{}  (\mforall{}x,y:Point(self).    f  x  y  \mequiv{}  f  y  x)\}  ].
\mforall{}[m:\{m:\mBbbR{}  {}\mrightarrow{}  Point(self)  {}\mrightarrow{}  Point(self)| 
          (\mforall{}a:\mBbbR{}.  \mforall{}x,y:Point(self).    m  a  (p  x  y)  \mequiv{}  p  (m  a  x)  (m  a  y))
          \mwedge{}  (\mforall{}x:Point(self)
                    (m  r1  x  \mequiv{}  x
                    \mwedge{}  m  r0  x  \mequiv{}  z
                    \mwedge{}  (\mforall{}a,b:\mBbbR{}.    m  a  (m  b  x)  \mequiv{}  m  (a  *  b)  x)
                    \mwedge{}  (\mforall{}a,b:\mBbbR{}.    m  (a  +  b)  x  \mequiv{}  p  (m  a  x)  (m  b  x))))\}  ].  \mforall{}[psep:\mforall{}x,x',y,y':Point(self).
                                                                                                                                          (p  x  y  \#  p  x'  y'
                                                                                                                                          {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \#  y'))].
\mforall{}[msep:\mforall{}a,b:\mBbbR{}.  \mforall{}x,y:Point(self).    (m  a  x  \#  m  b  y  {}\mRightarrow{}  (a  \mneq{}  b  \mvee{}  x  \#  y))].
    (ss=self;
      0=z;
      +=p;
      *=m;
      +sep=psep;
      *sep=msep  \mmember{}  RealVectorSpace)


By

---

Latex:
(Auto
  THEN  (Assert  self  \mmember{}  SeparationSpace  BY
                          Auto)
  THEN  (D  1  THENA  Auto)
  THEN  Unfolds  ``mk-real-vector-space  real-vector-space``  0
  THEN  RepUR  ``ss-point  ss-sep``  0
  THEN  RepeatFor  5  ((RecordPlusTypeCD
                                        THENL  [  Id
                                                    ;  (Reduce  0
                                                          THEN  Try  ((RepUR  ``ss-eq  ss-sep``  0
                                                                                THEN  Folds  ``ss-point  ss-sep``  0
                                                                                THEN  Try  (Fold  `ss-eq`  0)
                                                                                THEN  Trivial))
                                                          )]
                                      ))
  THEN  RepUR  ``separation-space``  0
  THEN  RepeatFor  3  ((RecordPlusTypeCD  THENL  [  Id;  (Reduce  0  THEN  Trivial)]))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index