---

Step * of Lemma rv-ip0

∀[rv:InnerProductSpace]. ∀[x:Point].  (x ⋅ 0 = r0)
BY
{ (Auto
   THEN (Assert x ⋅ 0 = (x ⋅ 0 + x ⋅ 0) BY
               ((Assert 0 + 0 ≡ 0 BY
                       Auto)
                THEN (RW (AddrC [1;3] (RevHypC (-1))) 0 THENA Auto)
                THEN RWO  "rv-ip-add2" 0
                THEN Auto))
   ) }

1
1. rv : InnerProductSpace
2. x : Point
3. x ⋅ 0 = (x ⋅ 0 + x ⋅ 0)
⊢ x ⋅ 0 = r0

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[x:Point].    (x  \mcdot{}  0  =  r0)


By

---

Latex:
(Auto
  THEN  (Assert  x  \mcdot{}  0  =  (x  \mcdot{}  0  +  x  \mcdot{}  0)  BY
                          ((Assert  0  +  0  \mequiv{}  0  BY
                                          Auto)
                            THEN  (RW  (AddrC  [1;3]  (RevHypC  (-1)))  0  THENA  Auto)
                            THEN  RWO    "rv-ip-add2"  0
                            THEN  Auto))
  )

---

Home Index