---

Step * of Lemma rv-ip-sub-squared

No Annotations
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)].  (x - y^2 = ((x^2 - r(2) * x ⋅ y) + y^2))
BY
{ (Auto THEN (RWW "rv-ip-sub rv-ip-sub2 rv-ip-mul rv-ip-mul2" 0 THENA Auto)) }

1
1. rv : InnerProductSpace
2. x : Point(rv)
3. y : Point(rv)
⊢ (x^2 - x ⋅ y - y ⋅ x - y^2) = ((x^2 - r(2) * x ⋅ y) + y^2)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[rv:InnerProductSpace].  \mforall{}[x,y:Point(rv)].    (x  -  y\^{}2  =  ((x\^{}2  -  r(2)  *  x  \mcdot{}  y)  +  y\^{}2))


By

---

Latex:
(Auto  THEN  (RWW  "rv-ip-sub  rv-ip-sub2  rv-ip-mul  rv-ip-mul2"  0  THENA  Auto))

---

Home Index