---

Step * of Lemma rv-mul-sep-iff

∀rv:InnerProductSpace. ∀a,b:ℝ. ∀y:Point.  (a*y # b*y ⇐⇒ a ≠ b ∧ y # 0)
BY
{ (Auto THEN Try ((FLemma `rv-mul-sep1` [-1] THEN Auto))) }

1
1. rv : InnerProductSpace
2. a : ℝ
3. b : ℝ
4. y : Point
5. a*y # b*y
6. a ≠ b
⊢ y # 0

2
1. rv : InnerProductSpace
2. a : ℝ
3. b : ℝ
4. y : Point
5. a ≠ b
6. y # 0
⊢ a*y # b*y

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b:\mBbbR{}.  \mforall{}y:Point.    (a*y  \#  b*y  \mLeftarrow{}{}\mRightarrow{}  a  \mneq{}  b  \mwedge{}  y  \#  0)


By

---

Latex:
(Auto  THEN  Try  ((FLemma  `rv-mul-sep1`  [-1]  THEN  Auto)))

---

Home Index