---

Step * of Lemma rv-Cauchy-Schwarz-equality

No Annotations
∀rv:InnerProductSpace. ∀a,b:Point(rv).  ((a ⋅ b^2 = (a^2 * b^2)) ⇒ b # 0 ⇒ (∃t:ℝ. a ≡ t*b))
BY
{ (Auto THEN (FLemma `rv-ip-positive` [-1] THENA Auto) THEN Assert ⌜a - (a ⋅ b/b^2)*b ≡ 0⌝⋅) }

1
.....assertion..... 
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. a ⋅ b^2 = (a^2 * b^2)
5. b # 0
6. r0 < b^2
⊢ a - (a ⋅ b/b^2)*b ≡ 0

2
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. a ⋅ b^2 = (a^2 * b^2)
5. b # 0
6. r0 < b^2
7. a - (a ⋅ b/b^2)*b ≡ 0
⊢ ∃t:ℝ. a ≡ t*b

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}a,b:Point(rv).    ((a  \mcdot{}  b\^{}2  =  (a\^{}2  *  b\^{}2))  {}\mRightarrow{}  b  \#  0  {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  a  \mequiv{}  t*b))


By

---

Latex:
(Auto  THEN  (FLemma  `rv-ip-positive`  [-1]  THENA  Auto)  THEN  Assert  \mkleeneopen{}a  -  (a  \mcdot{}  b/b\^{}2)*b  \mequiv{}  0\mkleeneclose{}\mcdot{})

---

Home Index