---

Step * 1 1 1 of Lemma rv-orthogonal-injective

.....assertion..... 
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 ≡ 0
BY
{ (RepUR ``rv-sub rv-minus`` 0 THEN (RWW  "3.1 4 -1" 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 y + r(-1)*f y ≡ 0

---

Latex:

---

Latex:
.....assertion..... 
1.  rv  :  InnerProductSpace
2.  f  :  Point(rv)  {}\mrightarrow{}  Point(rv)
3.  \mforall{}x,y:Point(rv).    (f  x  +  y  \mequiv{}  f  x  +  f  y  \mwedge{}  (x  \mcdot{}  y  =  f  x  \mcdot{}  f  y))
4.  \mforall{}x:Point(rv).  \mforall{}a:\mBbbR{}.    f  a*x  \mequiv{}  a*f  x
5.  x  :  Point(rv)
6.  y  :  Point(rv)
7.  f  x  \mequiv{}  f  y
\mvdash{}  f  x  -  y  \mequiv{}  0


By

---

Latex:
(RepUR  ``rv-sub  rv-minus``  0  THEN  (RWW    "3.1  4  -1"  0  THENA  Auto))

---

Home Index