---

Step * of Lemma rv-orthogonal-inverse

∀[rv:InnerProductSpace]. ∀[f,g:Point ⟶ Point].  (Orthogonal(f)) supposing (Orthogonal(g) and (∀x:Point. g (f x) ≡ x))
BY
{ (Auto
   THEN (InstLemma `rv-orthogonal-injective` [⌜rv⌝;⌜g⌝]⋅ THENA Auto)
   THEN All (RWO "rv-orthogonal-iff")
   THEN Auto) }

1
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. g : Point ⟶ Point
4. ∀x:Point. g (f x) ≡ x
5. g 0 ≡ 0
6. Isometry(g)
7. ∀x,y:Point.  (g x ≡ g y ⇒ x ≡ y)
⊢ f 0 ≡ 0

2
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. g : Point ⟶ Point
4. ∀x:Point. g (f x) ≡ x
5. g 0 ≡ 0
6. Isometry(g)
7. ∀x,y:Point.  (g x ≡ g y ⇒ x ≡ y)
8. f 0 ≡ 0
⊢ Isometry(f)

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[f,g:Point  {}\mrightarrow{}  Point].
    (Orthogonal(f))  supposing  (Orthogonal(g)  and  (\mforall{}x:Point.  g  (f  x)  \mequiv{}  x))


By

---

Latex:
(Auto
  THEN  (InstLemma  `rv-orthogonal-injective`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  All  (RWO  "rv-orthogonal-iff")
  THEN  Auto)

---

Home Index