---

Step * 1 of Lemma rv-sep-shift2


1. rv : InnerProductSpace
2. a : Point
3. p : Point
4. q : Point
5. p # q
⊢ p + a # q + a
BY
{ ((All (RWO "rv-sep-iff-norm") THENA Auto)
   THEN (Assert p + a - q + a ≡ p - q BY
               (RealVecEqual THEN Auto))
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point
3.  p  :  Point
4.  q  :  Point
5.  p  \#  q
\mvdash{}  p  +  a  \#  q  +  a


By

---

Latex:
((All  (RWO  "rv-sep-iff-norm")  THENA  Auto)
  THEN  (Assert  p  +  a  -  q  +  a  \mequiv{}  p  -  q  BY
                          (RealVecEqual  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index