---

Step * of Lemma real-vec-right-angle-lemma

∀[n:ℕ]. ∀[x,z:ℝ^n].  uiff(x⋅z = r0;d(z;x) = d(z;r(-1)*x))
BY
{ (Intros
   THEN (RWO  "real-vec-dist-equal-iff" 0 THENA Auto)
   THEN (RWW "dot-product-linearity1-sub.1  dot-product-linearity1-sub.2" 0⋅ THENA Auto)
   THEN RWW "dot-product-linearity2.1  dot-product-linearity2.2" 0⋅
   THEN Auto) }

1
1. n : ℕ
2. x : ℝ^n
3. z : ℝ^n
4. x⋅z = r0
⊢ (z⋅z - z⋅x - x⋅z - x⋅x) = (z⋅z - r(-1) * z⋅x - (r(-1) * x⋅z) - r(-1) * r(-1) * x⋅x)

2
1. n : ℕ
2. x : ℝ^n
3. z : ℝ^n
4. (z⋅z - z⋅x - x⋅z - x⋅x) = (z⋅z - r(-1) * z⋅x - (r(-1) * x⋅z) - r(-1) * r(-1) * x⋅x)
⊢ x⋅z = r0

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,z:\mBbbR{}\^{}n].    uiff(x\mcdot{}z  =  r0;d(z;x)  =  d(z;r(-1)*x))


By

---

Latex:
(Intros
  THEN  (RWO    "real-vec-dist-equal-iff"  0  THENA  Auto)
  THEN  (RWW  "dot-product-linearity1-sub.1    dot-product-linearity1-sub.2"  0\mcdot{}  THENA  Auto)
  THEN  RWW  "dot-product-linearity2.1    dot-product-linearity2.2"  0\mcdot{}
  THEN  Auto)

---

Home Index