---

Step * of Lemma rv-orthogonal-iff

No Annotations
∀[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Orthogonal(f) ⇐⇒ f 0 ≡ 0 ∧ Isometry(f))
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. Orthogonal(f)
⊢ f 0 ≡ 0 ∧ Isometry(f)

2
1. rv : InnerProductSpace
2. f : Point(rv) ⟶ Point(rv)
3. f 0 ≡ 0 ∧ Isometry(f)
⊢ Orthogonal(f)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[rv:InnerProductSpace].  \mforall{}f:Point(rv)  {}\mrightarrow{}  Point(rv).  (Orthogonal(f)  \mLeftarrow{}{}\mRightarrow{}  f  0  \mequiv{}  0  \mwedge{}  Isometry(f))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index