---

Step * of Lemma rv-orthogonal-compose

∀[rv:InnerProductSpace]. ∀[f,g:Point ⟶ Point].  (Orthogonal(f o g)) supposing (Orthogonal(g) and Orthogonal(f))
BY
{ (Auto
   THEN (InstLemma `rv-orthogonal-implies-functional` [⌜rv⌝;⌜f⌝]⋅ THEN Auto)
   THEN All (RWO "rv-orthogonal-iff")
   THEN EAuto 1
   THEN RepUR ``compose`` 0) }

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `rv-orthogonal-implies-functional`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  All  (RWO  "rv-orthogonal-iff")
  THEN  EAuto  1
  THEN  RepUR  ``compose``  0)

---

Home Index