---

Step * 1 of Lemma rv-orthogonal-injective


1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. Orthogonal(f)
4. x : Point(rv)
5. y : Point(rv)
6. f x ≡ f y
⊢ x - y^2 = r0
BY
{ (D 3 THEN ExRepD THEN (RWO "3.2" 0 THENA Auto)) }

1
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. ∀x,y:Point(rv).  (f x + y ≡ f x + f y ∧ (x ⋅ y = f x ⋅ f y))
4. ∀x:Point(rv). ∀a:ℝ.  f a*x ≡ a*f x
5. x : Point(rv)
6. y : Point(rv)
7. f x ≡ f y
⊢ f x - y^2 = r0

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  f  :  Point(rv)  {}\mrightarrow{}  Point(rv)
3.  Orthogonal(f)
4.  x  :  Point(rv)
5.  y  :  Point(rv)
6.  f  x  \mequiv{}  f  y
\mvdash{}  x  -  y\^{}2  =  r0


By

---

Latex:
(D  3  THEN  ExRepD  THEN  (RWO  "3.2"  0  THENA  Auto))

---

Home Index