---

Step * of Lemma rv-ip-add-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-add rv-ip-add2 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-add  rv-ip-add2  rv-ip-mul  rv-ip-mul2"  0  THENA  Auto))

---

Home Index